Re: [mizar] XML DTD for Mizar articles?

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

> Has someone already defined a proper XML DTD for Mizar
> articles?  

Probably not. 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, and is 
probably quite near (1 day?) from a real validation-usable DTD for the XML 
prel-s, but it's rather about storage of the internal Mizar 
datastructures.
However, all of this is unofficial yet, because
- XML formats for other parts of Mizar (e.g. articles after various stages 
  of processing) have to be devised yet and integrated together
- 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)
- It still requires some C/Pascal object-file hacking to link in Windows, 
  so the CVS version compiles without problems only in Linux 

Regards,
Josef