Re: [mizar] XML DTD for Mizar articles?

[Freek Wiedijk <freek@cs.kun.nl>]

Hi Josef,

>Currently, the internal Mizar DB (prel-s) has been ported to
>XML, and Mizar (more precisely, accommodator, exporter and
>tranferer) has expat-based I/O interface to this format. A
>sketch of DTD exists, [...]

It might be interesting to look at this sketch.  Can you post
it to mizar-forum?

>- It is undecided yet, where and for what purposes will XML
>  be used internally in Mizar (even the shortest variant of
>  XML tags makes prel-s five times larger and (thus)
>  accommodator four times slower)

I don't see a good reason to do this.  I'd only use XML for
communication with the outside world.  To put the MML in a
shape that others can use it without having to have a Mizar
parser.

But it might be nice to have all this endless set of files
that Mizar generates (.aco, .ana, .ano, .atr, etc. etc.) be
combined in a single file with some kind of table of contents
at the start.  Those endless lists of files look so messy.
And in a compiler you also have only one .o file, haven't
you.  Something like that would be more interesting to me
than have the files themselves be XML.

Freek