[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] MML and "Building Mizar from Scratch"
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/
===========================================================================