Re: wsmiz.xml missing?
Alex Nelson thmprover _AT_ gmail.com <[email protected]> Fri, 12 Sep 2025 18:00:39 -0700
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAA+9CX3bseLzS6Z_VrX-hFKPWD-+eqRGOsYYHO4nyrtyTb30fA@mail.gmail.com> |
--0000000000002ab1aa063ea44db6 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=E2=80=AFAM Alex Nelson <[email protected]> wr= ote: > 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, i= f > 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=E2=80=AFAM adamn _AT_ math.uwb.edu.pl < > [email protected]> wrote: > >> 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 bigges= t >> > "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 >> >> >> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D >> 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/ >> >> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D >> > --0000000000002ab1aa063ea44db6 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr"><div><div><div><div><div><div><div>Hello,<br><br></div>Som= e progress, I have a first draft of the parser (and the 23 files it uses). = I have posted it to github, <a href=3D"https://github.com/pqnelson/literate= -Mizar">https://github.com/pqnelson/literate-Mizar</a><br><br></div>A 606 p= age PDF is posted there, as well.<br><br></div>I openly admit I find the pa= rser a bit involved, and my understanding of the term parsing routines is a= bit limited. (The extSubexpObj.FinishLongTerm's basic structure is cle= ar, but the details elude me.)<br><br></div>I'm finishing up writing an= notations about the Parser.pas file, and then I will review the entire thin= g again.<br><br></div>Feedback is welcome, feel free to either email me or = file an issue on github.<br><br></div>Best,<br></div>Alex</div><br><div cla= ss=3D"gmail_quote gmail_quote_container"><div dir=3D"ltr" class=3D"gmail_at= tr">On Tue, Sep 9, 2025 at 8:21=E2=80=AFAM Alex Nelson <<a href=3D"mailt= o:[email protected]">[email protected]</a>> wrote:<br></div><blockqu= ote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px= solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div><div><div>H= ello,<br><br></div>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= .<br><br></div>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 &= quot;fascicles", then move on to the other components.<br><br></div><d= iv>Best,<br></div><div>Alex</div></div><br><div class=3D"gmail_quote"><div = dir=3D"ltr" class=3D"gmail_attr">On Mon, Sep 8, 2025 at 12:31=E2=80=AFAM ad= amn _AT_ <a href=3D"http://math.uwb.edu.pl" target=3D"_blank">math.uwb.edu.= pl</a> <<a href=3D"mailto:[email protected]" target=3D"= _blank">[email protected]</a>> wrote:<br></div><blockqu= ote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px= solid rgb(204,204,204);padding-left:1ex">Dear Alex,<br> <br> Quoting "Alex Nelson=C2=A0 thmprover _AT_ <a href=3D"http://gmail.com"= rel=3D"noreferrer" target=3D"_blank">gmail.com</a>"=C2=A0 <br> <<a href=3D"mailto:[email protected]" target=3D"_blank"= >[email protected]</a>>:<br> <br> > I have been studying the Mizar system's source code, and I noticed= in<br> > `base/wsmarticle.pas`, there is reference to "wsmiz.xml" in = the constructor<br> > `OutWSMizFileObj .OpenFileWithXSL`...but that XML file is missing in M= izar<br> > installations (and it is not present in the Mizar system's reposit= ory).<br> ><br> > Does anyone have a copy of it? Is this actually needed anywhere? (Just= <br> > grepping through the output produced running Mizar on, e.g., group_24,= I<br> > don't find it appearing in any output file...)<br> <br> I believe that the file never existed and the optional constructor was=C2= =A0 <br> written 'just in case', but as you've noticed it was never used= in the=C2=A0 <br> actual source code base. The grammar of the WSX files was quite=C2=A0 <br> experimental. As it was used only internally by the verifier, noone=C2=A0 <= br> seemed to care to document it properly. In principle, the MSX format=C2=A0 = <br> (and later ESX) was intended to be an extension of WSX, but there may=C2=A0= <br> be some incompatibilities introduced during their development.<br> <br> > I only noticed this because I have been transcribing the Mizar source = code<br> > into a literate program (using Knuth's WEB). So far, that's th= e biggest<br> > "bug" I have encountered (in the 21 files I have looked at),= so that's a<br> > good sign.<br> <br> That's quite surprising, but it's indeed a good sign :-)<br> <br> Please keep up the great work and let us know about the progress with=C2=A0= <br> this project.<br> <br> Adam<br> <br> -- <br> Adam Naumowicz<br> <br> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= <br> Division of Programming and Formal Methods=C2=A0 =C2=A0Fax: +48(85)738-83-3= 3<br> Faculty of Computer Science=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 =C2=A0 Tel: +48(85)738-83-06 (office)<br> University of Bialystok=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 E-mail: <a href=3D"mailto:[email protected]" t= arget=3D"_blank">[email protected]</a><br> Ciolkowskiego 1M, 15-245 Bialystok, Poland=C2=A0 =C2=A0<a href=3D"http://ma= th.uwb.edu.pl/~adamn/" rel=3D"noreferrer" target=3D"_blank">http://math.uwb= .edu.pl/~adamn/</a><br> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= <br> </blockquote></div> </blockquote></div> --0000000000002ab1aa063ea44db6--