Re: [mizar] A. Asperti's offer

[Andrea Asperti <asperti@CS.UniBO.IT>]

Hallo. Sorry for getting in so late in this discussion
but I was on holiday. 
The idea was to reuse part
of parser code to produce something orthogonal and 
independent from Mizar, with no commitment at all on
your side.
We are not experts of Mizar, but we are not complete
neophyte as well. 
Actually, two years ago, we made a similar attempt to
produce XML starting from the source and the available
grammar specifications, but we got stuck in some 
hundreds grammar conflicts in our yacc parser...
Having a look at your parser, and possibly reusing 
part of its code could probably sensibly simplify 
or work. 

We hope to be able to work in a completely independent
way (unless anynody is interested in some cooperation).

Best Regards.
					-- andrea


On Wed, 7 Aug 2002, Grzegorz Bancerek wrote:

> Piotr Rudnicki wrote:
> > The entire Mizar-XML connection should be discussed before any
> > commitments.  I cannot speak for the current programmers but it is
> > unlikely that Mizar's sources will be adjusted just to serve the XML
> > needs - there are simply more important things to do.  However, I
> > would expect that there is no such need.  I guess that Grzegorz in his
> > MML query has probably developed all the needed tools that the XML
> > people could use without ever looking into Mizar sources.
> 
> My tools concern only exportable part of Mizar article. Nothing
> for proofs yet.  These tools are based on Mizar pascal units.
> So, it means that some work is repeated: reprograming for new
> Mizar features or reprocessing of Mizar articles. I expect that
> XML form of Mizar article can allow to avoid that problem.
> 
> XML solution can also reduce difficulties in the translator
> for Formalized Mathematics. The need of such XML form has been
> discussed through years in developer team.
> 
> Best regards,
> Grzegorz
>