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