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 thecurrent 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 :-).
Josef