Re: wsmiz.xml missing?

Dear Alex,

Quoting "Alex Nelson  thmprover _AT_ gmail.com"  
<[email protected]>:

> 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: [email protected]
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================