Hi all, I notice there are several independent Metamath parser/verifiers in the making these days:
* Anthony Barlett recently announced his Typescript verifier `checkmm-ts`, * Glauco is writing a Typescript program / VsCode extension, * Benoît is writing a lexer/parser, * Mario and I have been working for a while on `metamath-knife`, and I'm working on a VsCode extension for Metamath. * There are laudable efforts to maintain and extend `metamath-exe` (Wolf) and `mmverify.py` (Benoît) On one hand that's a sign of a vibrant community and that's very good. On the other hand these are fragmented efforts (to paraphrase Mario) and we might achieve more if we were all working on a single project. There is of course a cost for team work, as we need to agree on a direction and design choices, and coordinate efforts. This also means sometimes making concessions, which is never easy. GitHub is a wonderful tool which can help a lot here. Personally I know the time I can spend on Metamath is limited, so I want to make it count - and like everyone I also want to have fun! My questions to the community are: * Does anyone else wish to join forces and work more together on a common project rather on "competing" ones? * What would the right direction be for that? Which steps shall we take? * I followed Mario's call to work in Rust, I think technically it's a good choice. That language is growing in popularity, however it is still not as popular as e.g. Python, JS/TS, C++ or java, which pretty much every programmer touched. Did that choice exclude too many? * What was the rationale for you guys to start a new project rather than join an existing one? Are those existing project not well-documented enough? Is it too daunting to learn about the existing code base? Are you missing some clear "good first task" as GitHub calls them? Are the working environment of other projects not welcoming enough? Do you think they are not going to the right direction? Are there no other projects advanced enough to have a critical mass worth joining? Or is simply the challenge to do things alone stronger and more appealing? As far as the project I've chosen to work on, the goal with `metamath-knife` and the Metamath VsCode Extension would be to provide a feature-rich proof assistant in VsCode just like Lean or MMJ2, or at least provide in VsCode the functionalities I had in my Eclipse plugin (I made a video about that). I've learned Rust as it was the programming language suggested by Mario and because `metamath-knife` was seen as a "new community verifier". All work-in-progress is in GitHub and external contributions are of course welcome, though only Mario and I are contributing. I'd love to learn more about other projects (Benoît, Glauco) even though we discussed a bit directly: what are your goals/aspirations? Would you welcome external contributions? BR, _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8bd47a1f-ca46-5e8d-c159-75877d3eea5d%40gmx.net.
