Re: [mizar] MML and "Building Mizar from Scratch"

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 <owner-mizar-forum@mizar.uwb.edu.pl> wrote:

Hi Alex,

Quoting "Alex Nelson thmprover _AT_ gmail.com"
<owner-mizar-forum@mizar.uwb.edu.pl>:

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