Re: MML and "Building Mizar from Scratch"

--0000000000004f12930629b54353
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Hello,

I am very encouraged by these responses and happy to see (as my Mom would
say) we're all singing from the same hymnal.

(1) Thank you, Roland, for the link; I will look at that in greater detail.

(2) Adam, thank you for summarizing how to create the MML. I will need to
ponder it a bit further, just because I'm slow at digesting things.

(3) I have to agree heartily with Sebastian's observation that some sort of
CI is highly desirable, something I would be willing to work on.

Best,
Alex

On Thu, Dec 19, 2024 at 4:49=E2=80=AFAM Sebastian Koch fly.high.android _AT=
_
gmail.com <[email protected]> wrote:

> Hi there,
>
> I also want to thank Alex for pointing out that there is now a proof
> assistant SE.
>
> On 19.12.24 12:51, adamn _AT_ math.uwb.edu.pl wrote:
> >> Also, could we move the MML to be a github repository? One advantage t=
o
> >> 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 an=
d
> >> 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.
>
> I might add that since PRs need to be approved, we wouldn't loose the
> centralized aspect of the MML. Sure there can be forks, but I think as
> long as PRs are actively attended to, there won't be a derivation
> overtaking the original in popularity :)
>
> What we would need and what I'm also personally interested in is a tool
> (prob. a simple script) that can check the whole MML + changes. That
> added as a github action on top of PRs and we wouldn't need to check out
> a PR to see if the MML is still verifiable. I'm sure the Library
> committee has such a tool already?
>
>
> Best regards and stay healthy
>
> Sebastian Koch
>
>
>

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

<div dir=3D"ltr">Hello,<br><br>I am very encouraged by these responses and =
happy to see (as my Mom would say) we&#39;re all singing from the same hymn=
al.<div><br></div><div>(1) Thank you, Roland, for the link; I will look at =
that in greater detail.</div><div><br></div><div>(2) Adam, thank you for su=
mmarizing how to create the MML. I will need to ponder it a bit further, ju=
st because I&#39;m slow at digesting things.<br><br>(3) I have to agree hea=
rtily with Sebastian&#39;s observation that some sort of CI is highly desir=
able, something I would be willing to work on.</div><div><br></div><div>Bes=
t,<br>Alex</div></div><br><div class=3D"gmail_quote gmail_quote_container">=
<div dir=3D"ltr" class=3D"gmail_attr">On Thu, Dec 19, 2024 at 4:49=E2=80=AF=
AM Sebastian Koch  fly.high.android _AT_ <a href=3D"http://gmail.com">gmail=
.com</a> &lt;<a href=3D"mailto:[email protected]">owner-mi=
[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"gma=
il_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,2=
04,204);padding-left:1ex">Hi there,<br>
<br>
I also want to thank Alex for pointing out that there is now a proof <br>
assistant SE.<br>
<br>
On 19.12.24 12:51, adamn _AT_ <a href=3D"http://math.uwb.edu.pl" rel=3D"nor=
eferrer" target=3D"_blank">math.uwb.edu.pl</a> wrote:<br>
&gt;&gt; Also, could we move the MML to be a github repository? One advanta=
ge to<br>
&gt;&gt; doing so is the ability to file issues on Github with possible min=
or<br>
&gt;&gt; cleanups (e.g., the definition GROUP_1:def 5 is a little too stric=
t and<br>
&gt;&gt; should instead work with any non empty Group-like multMagma, not j=
ust<br>
&gt;&gt; Groups).<br>
&gt;<br>
&gt; Sounds like a good idea to me. Since the founding of MML there&#39;s b=
een <br>
&gt; a policy to allow users build their own libraries, but to keep the <br=
>
&gt; main library development centralized in order to avoid all sorts of <b=
r>
&gt; issues with incompatible versions.<br>
&gt; But I agree that these days the project can benefit much more by <br>
&gt; involving in the work on MML a larger group of people used to <br>
&gt; git-based tools.<br>
<br>
I might add that since PRs need to be approved, we wouldn&#39;t loose the <=
br>
centralized aspect of the MML. Sure there can be forks, but I think as <br>
long as PRs are actively attended to, there won&#39;t be a derivation <br>
overtaking the original in popularity :)<br>
<br>
What we would need and what I&#39;m also personally interested in is a tool=
 <br>
(prob. a simple script) that can check the whole MML + changes. That <br>
added as a github action on top of PRs and we wouldn&#39;t need to check ou=
t <br>
a PR to see if the MML is still verifiable. I&#39;m sure the Library <br>
committee has such a tool already?<br>
<br>
<br>
Best regards and stay healthy<br>
<br>
Sebastian Koch<br>
<br>
<br>
</blockquote></div>

--0000000000004f12930629b54353--