Hello,
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).
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?
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).