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