I also have been working on a verifier, which is at https://git.sr.ht/~philipwhite/mmweb, if anyone is interested. The implementation includes a CLI for verifying files, but the main point of the parser/verifier is to power a web UI, which I am currently hosting at https://trailingwhite.space/proofs/ if you want to take a look (it downloads set.mm on page load, which takes several seconds on my connection, but it gets cached by the browser so that future page loads are faster). All the design decisions are aimed at enabling the web UI to be as good as possible.
One reason I starting working on my own verifier instead of contributing to a different one is that I thought it would be a fun project with a limited enough scope that I could finish it pretty quickly. I picked OCaml because that is that language I like best; the goal wasn't to make the version that everyone should use. After I got to the point where the verifier worked well enough, I started thinking about interesting things that I could do with such a library, and the idea of an interesting web UI came up. At this point, I have to answer the question, "why not switch to using a more hardcore and battle-tested library like metamath-knife?" I can think of a lot answers to this: - Using a thing that I wrote and that nobody depends on means that I can change it to fit my needs whenever I want, and without asking anyone else. - It wouldn't at all surprise me if a general-purpose API is difficult to make suitable for web user interfaces, and in particular that type of user interface code that I write. Bonsai, the library I am using, combine both the virtual-dom approach popularized by React, and also a library called incremental, which preserves work from previous frames whenever it can. To make the incremental library happy, it's a good thing to use persistent data structures and make updates in a way that shares as much memory structure as possible, since that will allow the incremental library to short-circuit computations that it has already done. However, this approach seems awful if your goal is to make a verifier that goes as fast as possible over the entire file. - My build can be all in one language, and I don't have to worry about how to link Rust and OCaml together. Maybe it's not that hard to "get it to work", but polyglot systems are always at least a little less convenient; for instance, you only get to support the intersection of the systems that all the languages support. In my case, I think binding OCaml to Rust and making it work in the browser seems like a not fun situation. I admit it would be a shame if lots of people did a bunch of redundant work, and then we end up with a bunch of different verifiers with the same feature-set. However, if what's happening is that if a bunch of people are writing verifiers so that they can then explore some interesting ideas on top of it, that seems like a great situation to me. Haskell was the result of lots of people focusing their efforts together to do research on lazy functional programming (I think). This seems like a big win because decent programming languages take a while to build, so it helps a lot if researchers have an already built language as a starting point. In comparison, metamath verifiers are stupid easy to write. (I don't mean your stupid if you can't make one, but that it's much much easier to make one than to make a programming language compiler). In my estimation, at this point, if everybody exploring interesting ideas were working on the same codebase, it could be rather inefficient. Eventually, once ideas mature, it makes sense to me to think about how to combine them all into one system, but now feels too early. To clarify, what I really mean is that if you like Rust and metamath-knife matches closely enough with a thing your working on, then that's a good project to work with. However, if, like me, you don't really like Rust (it's fine, I just don't really want do low-level programming), or you're building a system that has incompatible goals, then go off and do your own thing (or maybe collaborate with people who are going in the same direction). On Tue, 31 May 2022 07:01:14 -0400 Mario Carneiro <[email protected]> wrote: > 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/20220531175100.0e0700c9%40ithilien.
