Some info on the Mizar XML implementation

Kernel-related stuff, more important

• Syntactic XML parts are described right in the Pascal files (mostly iocorrel.pas) using the ##RNC embedded comments. These comments are written in the very simple Compact Relax NG specification language by James Clark, see the file xml/Mizar.rnc for examples, or http://www.relaxng.org/compact-tutorial-20030326.html for more.
• All XML elements and atributes used in Mizar have to be listed in the enumerated types in xmldict.pas, otherwise an XML error is reported.
• The mapping from strings to the Pascal names should be obvious: elements look like elDefinitionBlock in Pascal, and translate to the XML element 'DefinitionBlock', while attributes look like atRightSymbolNr in Pascal, and they are down-cased in XML - 'rightsymbolnr'.
• The following Perl one-liner collects all the ##RNC definitions into the file Mizar.rnc:

 
cat *.pas | perl -e 'local $/;$_=<>; while(m/#[#]RNC:((.|[\n])*?)[*]\)/g) { print $1}' > Mizar.rnc

Then the following one-liner prints all XML element tags defined (and if you change there 'el' to 'at', it will do attributes instead. It is probably the best way how to automatically update xmldict.pas after larger syntactic changes.

 
perl -e 'local $/;$_=<>; while(m/\b(el[A-Z]\w*)/g) {$h{$1}=()}; foreach $k (sort keys %h) {print "$k,\n"}' Mizar.rnc

• a better way how to produce Mizar.rnc is to go to the xml directory of the Pascal sources, and call

 
make Mizar.rnc 

Documentation and validation stuff, less important

These steps are optional, and you can leave it to me. They require to have some XML tools installed. On the other hand, validation is useful for finding errors in the RNC specification, and may therefore lead to changes in the Pascal files.

• The trang tool by James Clark is used for creating other XML specification formats (RNG, XSD). RNG (the XML version of RNC) is probably needed for validation by tools like xmllint. You can test it by running

 
make Mizar.rng

in the xml directory. If it fails on syntactic error, it means that you have to fix some ##RNC specification in the Pascal sources, and call this make target again.

• For specifying syntax of various Mizar XML files their starting element needs to be specified, and Mizar.rnc included. See the examples (e.g. article.rnc) in the xml directory, they are very simple:

 
include "Mizar.rnc"
start = Article

• For validating you need xmllint. Iniprels can be then validated by the schemata by calling

 
make check-iniprel

Look into the xml/Makefile iof you wish to validate something else.

• The html documentation is also created just by calling make, but more tools need to be installed (the docbook stylesheets and the rng-doc.xsl stylesheet). You will also need a XSLT processor for that (I use xsltproc). See xml/doc/Makefile .

XSLT processing, very optional

Unless you are interested in XSLT programming, leave this to me.

• If you want to change the HTML presentation created from the Mizar XML, you need to change the xml/xsl/miz.xsl stylesheet. You can do it directly - this I strongly discourage, XSLT in its raw form is extremely verbose and hard-to-read language.
• Or you can use the XSLTXT (https://xsltxt.dev.java.net/) language, which is a nice compact syntax equivalent to XSL, and serious stuff can be written (and read) in it. You will need Java and the xsltxt.jar program to transform miz.xsltxt to miz.xsl like this:

 
java -jar xsltxt.jar toXSL miz.xsltxt >miz.xsl

• Test your new miz.xsl either by opening the Mizar XML files directly in a good browser (e.g. Firefox), or (this is faster), by explicitly running a good xslt processor (e.g. xsltproc) like this:

 
xsltproc miz.xsl modelc_1.xml > modelc_1.html

-- JosefUrban - 02 May 2006