Hi,the new HTML is browsable at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.76.959/ , and downloadable at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.76.959.tar.gz (unpacks to 1.2GB). The version without proofs is at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.76.959.noproofs.tar.gz (this unpacks to 156MB). Both versions work also locally (clicking on proofs obviously only in the full version), and should be installed in $MIZFILES, and the top directory renamed (or symlinked) to "html". A new version of miz.xsl (http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/*checkout*/xsl4mizar/miz.xsl) links the currently authored article (displayed from Emacs) by default to these locally installed abstracts, and displays original identifiers as well. However both these features will not work, until a new version of the Mizar verifier is distributed (probably next Mizar version). If you want at least the local linking working now, symlinking (or copying for OS-es which suck) the $MIZFILES/html directory inside your "text" working directory should help.
The XSLT(XT) code is at http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/xsl4mizar/MHTML/, and most likely I won't work on it till end of February, so feel free to improve it (it's GPL).
Best, Josef Urban On Sat, 13 Jan 2007, Jesse Alama wrote:
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 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 :-).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