Re: [mizar] wsmiz.xml missing?

Hello,

Some progress, I have a first draft of the parser (and the 23 files it uses). I have posted it to github, https://github.com/pqnelson/literate-Mizar

A 606 page PDF is posted there, as well.

I openly admit I find the parser a bit involved, and my understanding of the term parsing routines is a bit limited. (The extSubexpObj.FinishLongTerm's basic structure is clear, but the details elude me.)

I'm finishing up writing annotations about the Parser.pas file, and then I will review the entire thing again.

Feedback is welcome, feel free to either email me or file an issue on github.

Best,

Alex

On Tue, Sep 9, 2025 at 8:21 AM Alex Nelson <thmprover@gmail.com> wrote:

Hello,

Ah, it's good to know about WSX being an experiment, but I will not worry too much about it then. I'll just make note of it.

It looks like I should have at least the parser transcribed by October, if not sooner. I will probably announce the parser as its own "fascicles", then move on to the other components.

Best,
Alex

On Mon, Sep 8, 2025 at 12:31 AM adamn _AT_ math.uwb.edu.pl <owner-mizar-forum@mizar.uwb.edu.pl> wrote:
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/
===========================================================================