MML and "Building Mizar from Scratch"

--000000000000c21af50629693821
Content-Type: text/plain; charset="UTF-8"

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).

Best,
Alex

--000000000000c21af50629693821
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>Hello,<br><br>There has been some interest in buildin=
g Mizar from scratch on the proof assistant stackexchange (see, e.g.,=C2=A0=
<a href=3D"https://proofassistants.stackexchange.com/q/4453/14">https://pro=
ofassistants.stackexchange.com/q/4453/14</a> and=C2=A0<a href=3D"https://pr=
oofassistants.stackexchange.com/q/4441/14">https://proofassistants.stackexc=
hange.com/q/4441/14</a>).<br><br>Right now, it is possible to compile many =
of the Mizar components using the Free Pascal Compiler, and a Makefile is a=
round somewhere.<br><br>But, as best as I can tell, it is not possible to &=
quot;build the MML from scratch&quot; (in the sense that I can&#39;t downlo=
ad a copy of the MML, use my local Mizar system to verify it, and then upda=
te my local Mizar system to use it).<br><br>Is such a thing possible? If so=
, could we add instructions on how to do it?<br><br>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 G=
ROUP_1:def 5 is a little too strict and should instead work with any non em=
pty Group-like multMagma, not just Groups).<br><br></div><div>Best,<br>Alex=
</div>
</div>

--000000000000c21af50629693821--