Re: MML and "Building Mizar from Scratch"

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/
===========================================================================