Re: [mizar] Re: feature request: include a semantic representaion of the mml in the mizar distribution

[Jesse Alama <alama@stanford.edu>]

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> On Thu, 21 Dec 2006, Jesse Alama wrote:
>
>> Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
>>> When Josef created the semantic representation in its current form,
>>> there came a natural idea of distributing it instead of the old linked
>>> abstract, there were only technical problems because Josef thought it
>>> best for us to store the representation of all MML versions, which is
>>> not possible at the moment on our server.
>
> I guess this is no longer a problem as Grzegorz seems to have enough
> disk space (which is btw. pretty cheap today (0.5$ for 1G?), and the
> html is about 0.5G only) at mmlquery.mizar.org .
>
>> But having at least the
>>> current version of MML rendered in the semantically linked form is
>>> certainly a good idea and we'll try to do so ASAP to help all those
>>> who sometimes prefer/must work off-line.
>>
>> It looks like the current version of the semantic representation of
>> the MML, available at http://mmlquery.mizar.org/mml , is 4.66.942.
>> But the current MML version is 4.75.958.  Would it be possible to
>> build a semantic representation of the current MML?
>
> http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr1.4.75.958.tar.gz
> is the link for abstracts only,
> http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.75.958.tar.gz
> contains also proofs (note that local references in the proofs got
> broken recently as a result of introducing original identifier names -
> still work in progress :-).

Let me just say that I applaud your effort to use the original
identifier names to the semantic representation.  I was going to file
a feature request for this very thing, but now I'll hold off on that
:->

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference