Hi Thierry, Thanks for this summary. I agree with your remarks, I'll try to answer some of your questions in my case, and I'd be glad to hear others' answers too.
I remember I was pretty frustrated myself, a year ago or two, when seeing independent efforts in different directions, while, as a user, I would have prefered everyone to work on mmj2 (the most promising project at the time) to improve it. As for me, I could diffcultly make useful contributions in large programs written in C/C++, Java or Rust, since I'm not proficient enough in these languages, at least of the moment. My in-progress verifier (it does verify proofs, now!) is in OCaml, and one of its goals is also for my own learning (I remember I had mentioned OCaml in the "community verifier" thread, but it didn't catch on, and that's fine). I also recently improved mmverify.py (type annotations, 4x speedup from which every CI run in metamath/set.mm now benefits) in Python (thanks for your reviews!) to try and contribute to the community. All in all, I think it is important to have our most seasoned programmers focus on the most promising tool, which is metamath-knife (and your VSCode extension). So I'm glad to see you and Mario work on it, and I recommend every experienced programmer to join you. When I feel more confident in Rust, I'll try and contribute too. I think that having begun with a smaller verifier in a language I'm more confident with did not waste my time but on the contrary is helping me reach that goal. In the meantime, having smaller projects in other languages can generate new ideas (I'm mostly thinking of frontend ideas here: interfaces and visualization, search tools...). What is important, is that, even if these are independent projects, they are not "competing" and they should share ideas as much as possible, and ideally also share their code. As for me, I hope to be able to put my project soon on Github, and to share ideas with another project in OCaml by Philip White (https://groups.google.com/g/metamath/c/qIHf2h0fxbA), and beyond. Benoît On Tuesday, May 31, 2022 at 7:17:29 AM UTC+2 Thierry Arnoux wrote: > 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/b29a801b-a1b7-480b-b348-7c67ae5ca456n%40googlegroups.com.
