Re: MML and "Building Mizar from Scratch"
Josef Urban josef.urban _AT_ gmail.com <[email protected]> Sat, 21 Dec 2024 10:55:08 +0800
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAFP4q17rJmxkx=V0ug1oiQ2qzn+XXhoJ9gBh1c6pCFgcufmApg@mail.gmail.com> |
--000000000000e2fa2c0629bee4d9 Content-Type: text/plain; charset="UTF-8" Long before GitHub CI, there was the git-based wiki for Mizar [1,2,3]. Someone (likely not me) could update/revamp it, it's pretty simple (git hooks). It died long ago because there were no users. I think Mario's Rusty Mizar also has scripts for verifying the whole MML from scratch. Btw., the git-based decentralization revolution followed by the GitHub-based centralization is pretty interesting. Somebody could write the history and study the dynamics of internet-based cycles of decentralized freedom and centralized laziness (invariably followed by major data/privacy sellouts/screwups/etc, leading to the next cycles). Josef [1] http://arxiv.org/abs/1005.4552 [2] https://github.com/JUrban/mwiki [3] http://arxiv.org/abs/1107.3209 On Thu, Dec 19, 2024, 19:55 adamn _AT_ math.uwb.edu.pl < [email protected]> wrote: > Hi Alex, > > Quoting "Alex Nelson thmprover _AT_ gmail.com" > <[email protected]>: > > > There has been some interest in building Mizar from scratch on the proof > > assistant stackexchange (see, e.g., > > https://proofassistants.stackexchange.com/q/4453/14 and > > https://proofassistants.stackexchange.com/q/4441/14). > > Thanks for pointing this out. > > > Right now, it is possible to compile many of the Mizar components using > the > > Free Pascal Compiler, and a Makefile is around somewhere. > > > > But, as best as I can tell, it is not possible to "build the MML from > > scratch" (in the sense that I can't download a copy of the MML, use my > > local Mizar system to verify it, and then update my local Mizar system to > > use it). > > > > Is such a thing possible? If so, could we add instructions on how to do > it? > > In fact all the basic building blocks are available to every Mizar > user, because creating MML from scratch doesn't differ that much from > building a local database. > Essentially one just needs a copy of axiomatic and initial 'prel' > files (hidden.*, tarski_0.*, tarski_a.*, *.dre), vocabularies for MML > and Mizar itself (mml.vct, mizar.dct) and the MML version number file > (mml.ini). All the other database files can be generated by > sequentially calling: accom, exporter and transfer for all the > articles whose names are provided by the MML article order file > (mml.lar). > So just like with compiling the software, the process is fairly > simple, but there are the obvious technical differences if one wants > to do it in various environments (Linux, Windows, MacOs, etc.). > > > Also, could we move the MML to be a github repository? One advantage to > > doing so is the ability to file issues on Github with possible minor > > cleanups (e.g., the definition GROUP_1:def 5 is a little too strict and > > should instead work with any non empty Group-like multMagma, not just > > Groups). > > Sounds like a good idea to me. Since the founding of MML there's been > a policy to allow users build their own libraries, but to keep the > main library development centralized in order to avoid all sorts of > issues with incompatible versions. > But I agree that these days the project can benefit much more by > involving in the work on MML a larger group of people used to > git-based tools. > > Cheers, > > 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/ > =========================================================================== > --000000000000e2fa2c0629bee4d9 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"auto">Long before GitHub CI, there was the git-based wiki for M= izar [1,2,3]. Someone (likely not me) could update/revamp it, it's pret= ty simple (git hooks). It died long ago because there were no users.=C2=A0<= div dir=3D"auto"><br></div><div dir=3D"auto">I think Mario's Rusty Miza= r also has scripts for verifying the whole MML from scratch.<div dir=3D"aut= o"><br></div><div dir=3D"auto">Btw., the git-based decentralization revolut= ion followed by the GitHub-based centralization is pretty interesting. Some= body could write the history and study the dynamics of internet-based cycle= s of decentralized freedom and centralized laziness (invariably followed by= major data/privacy sellouts/screwups/etc, leading to the next cycles).</di= v><div dir=3D"auto"><br></div><div dir=3D"auto">Josef=C2=A0</div><div dir= =3D"auto"><br></div><div dir=3D"auto">[1]=C2=A0<a href=3D"http://arxiv.org/= abs/1005.4552">http://arxiv.org/abs/1005.4552</a></div><div dir=3D"auto">[2= ] <a href=3D"https://github.com/JUrban/mwiki">https://github.com/JUrban/mwi= ki</a></div><div dir=3D"auto">[3] <a href=3D"http://arxiv.org/abs/1107.3209= ">http://arxiv.org/abs/1107.3209</a></div><div dir=3D"auto"><br></div></div= ></div><br><div class=3D"gmail_quote gmail_quote_container"><div dir=3D"ltr= " class=3D"gmail_attr">On Thu, Dec 19, 2024, 19:55 adamn _AT_ <a href=3D"ht= tp://math.uwb.edu.pl">math.uwb.edu.pl</a> <<a href=3D"mailto:owner-mizar= [email protected]">[email protected]</a>> wrote:<= br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8e= x;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Alex,<br> <br> Quoting "Alex Nelson=C2=A0 thmprover _AT_ <a href=3D"http://gmail.com"= rel=3D"noreferrer noreferrer" target=3D"_blank">gmail.com</a>"=C2=A0 = <br> <<a href=3D"mailto:[email protected]" target=3D"_blank"= rel=3D"noreferrer">[email protected]</a>>:<br> <br> > There has been some interest in building Mizar from scratch on the pro= of<br> > assistant stackexchange (see, e.g.,<br> > <a href=3D"https://proofassistants.stackexchange.com/q/4453/14" rel=3D= "noreferrer noreferrer" target=3D"_blank">https://proofassistants.stackexch= ange.com/q/4453/14</a> and<br> > <a href=3D"https://proofassistants.stackexchange.com/q/4441/14" rel=3D= "noreferrer noreferrer" target=3D"_blank">https://proofassistants.stackexch= ange.com/q/4441/14</a>).<br> <br> Thanks for pointing this out.<br> <br> > Right now, it is possible to compile many of the Mizar components usin= g the<br> > Free Pascal Compiler, and a Makefile is around somewhere.<br> ><br> > But, as best as I can tell, it is not possible to "build the MML = from<br> > scratch" (in the sense that I can't download a copy of the MM= L, use my<br> > local Mizar system to verify it, and then update my local Mizar system= to<br> > use it).<br> ><br> > Is such a thing possible? If so, could we add instructions on how to d= o it?<br> <br> In fact all the basic building blocks are available to every Mizar=C2=A0 <b= r> user, because creating MML from scratch doesn't differ that much from= =C2=A0 <br> building a local database.<br> Essentially one just needs a copy of axiomatic and initial 'prel'= =C2=A0 <br> files (hidden.*, tarski_0.*, tarski_a.*, *.dre), vocabularies for MML=C2=A0= <br> and Mizar itself (mml.vct, mizar.dct) and the MML version number file=C2=A0= <br> (mml.ini). All the other database files can be generated by=C2=A0 <br> sequentially calling: accom, exporter and transfer for all the=C2=A0 <br> articles whose names are provided by the MML article order file=C2=A0 <br> (mml.lar).<br> So just like with compiling the software, the process is fairly=C2=A0 <br> simple, but there are the obvious technical differences if one wants=C2=A0 = <br> to do it in various environments (Linux, Windows, MacOs, etc.).<br> <br> > Also, could we move the MML to be a github repository? One advantage t= o<br> > doing so is the ability to file issues on Github with possible minor<b= r> > cleanups (e.g., the definition GROUP_1:def 5 is a little too strict an= d<br> > should instead work with any non empty Group-like multMagma, not just<= br> > Groups).<br> <br> Sounds like a good idea to me. Since the founding of MML there's been= =C2=A0 <br> a policy to allow users build their own libraries, but to keep the=C2=A0 <b= r> main library development centralized in order to avoid all sorts of=C2=A0 <= br> issues with incompatible versions.<br> But I agree that these days the project can benefit much more by=C2=A0 <br> involving in the work on MML a larger group of people used to=C2=A0 <br> git-based tools.<br> <br> Cheers,<br> <br> Adam<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" rel=3D"noreferrer">[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 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> --000000000000e2fa2c0629bee4d9--