I think metamath-knife has shown itself to be pretty good for metamath-related data exploration, it is a lot easier to use as a library than anything else right now (usually you would have to take a verifier and modify it if you wanted to get information out). metamath-exe has probably historically been the way to do data exploration but all such exploration has been done purely through expanding the code itself and almost exclusively by Norm.
If you would prefer to do your data exploration in another language, I think we should try to set up bindings for mm-knife to OCaml et al. From what I can tell it's technically not too difficult, it just needs a place to live and a bit of maintenance. It would also be good to start collecting ideas for what kind of data exploration is interesting and make it easier to do those things in rust as well. On Tue, May 31, 2022 at 6:52 AM Benoit <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/b29a801b-a1b7-480b-b348-7c67ae5ca456n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsv5yRXwAgTKh4SaJcSD_-j-s3zhF3tiicAwD3zToQX4w%40mail.gmail.com.
