Re: wsmiz.xml missing?
Alex Nelson thmprover _AT_ gmail.com <[email protected]> Tue, 9 Sep 2025 08:21:29 -0700
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAA+9CX1drvsis+_x6hRkWR1b9T+7QFzRobY4ieJy2v9gSB56qA@mail.gmail.com> |
--0000000000006913b8063e5fdc2f Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=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 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 > > =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 (offic= e) > University of Bialystok E-mail: [email protected]= l > 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 > --0000000000006913b8063e5fdc2f Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr"><div><div><div>Hello,<br><br></div>Ah, it's good to kn= ow about WSX being an experiment, but I will not worry too much about it th= en. 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 "fascicles", then move on to the = other components.<br><br></div><div>Best,<br></div><div>Alex</div></div><br= ><div class=3D"gmail_quote gmail_quote_container"><div dir=3D"ltr" class=3D= "gmail_attr">On Mon, Sep 8, 2025 at 12:31=E2=80=AFAM adamn _AT_ <a href=3D"= http://math.uwb.edu.pl">math.uwb.edu.pl</a> <<a href=3D"mailto:owner-miz= [email protected]">[email protected]</a>> wrote= :<br></div><blockquote 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> --0000000000006913b8063e5fdc2f--