Re: [mizar] XML DTD for Mizar articles?

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

Hi Freek,


On Thu, 1 Aug 2002, Freek Wiedijk wrote:

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

http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/XmlForMizar
(You have been warned)

> >- 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.  

But in some following mail, you want to have search tools installed 
locally on your comp, and do not like 1G of Query. I am not quite certain 
about the price of larger prel-s in terms of accommodator speed too, but 
in times when any serious user installs Query of jfmabstrs anyway, why not 
try unifying all this into one reasonable DB, with e.g. possibilities of 
generating additional SQL indeces for users with more space (to have 
faster Query), or online generation of TeX abstracts (which could improve 
their quality), or even some other transformations ( but I still wonder, 
what use for MML will have "articles" in Coq, HOL or Omega produced 
thanks to first-order translation of the Mizar articles).


Josef