[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] wsmiz.xml missing?
Dear Alex,
Quoting "Alex Nelson thmprover _AT_ gmail.com"
<owner-mizar-forum@mizar.uwb.edu.pl>:
I have been studying the Mizar system's source code, and I noticed in
`base/wsmarticle.pas`, there is reference to "wsmiz.xml" in the constructor
`OutWSMizFileObj .OpenFileWithXSL`...but that XML file is missing in Mizar
installations (and it is not present in the Mizar system's repository).
Does anyone have a copy of it? Is this actually needed anywhere? (Just
grepping through the output produced running Mizar on, e.g., group_24, I
don't find it appearing in any output file...)
I believe that the file never existed and the optional constructor was
written 'just in case', but as you've noticed it was never used in the
actual source code base. The grammar of the WSX files was quite
experimental. As it was used only internally by the verifier, noone
seemed to care to document it properly. In principle, the MSX format
(and later ESX) was intended to be an extension of WSX, but there may
be some incompatibilities introduced during their development.
I only noticed this because I have been transcribing the Mizar source code
into a literate program (using Knuth's WEB). So far, that's the biggest
"bug" I have encountered (in the 21 files I have looked at), so that's a
good sign.
That's quite surprising, but it's indeed a good sign :-)
Please keep up the great work and let us know about the progress with
this project.
Adam
--
Adam Naumowicz
===========================================================================
Division of Programming and Formal Methods Fax: +48(85)738-83-33
Faculty of Computer Science Tel: +48(85)738-83-06 (office)
University of Bialystok E-mail: adamn@math.uwb.edu.pl
Ciolkowskiego 1M, 15-245 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
===========================================================================