[Date Prev][Date Next] [Chronological] [Thread] [Top]

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




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