Re: [mizar] A. Asperti's offer

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

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