Re: MML and "Building Mizar from Scratch"

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

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