> Nice ! I think a web-based program would be a nice addition, and I > was thinking of using js_of_ocaml for that. I suggested OCaml for > the community verifier in > https://groups.google.com/g/metamath/c/6fQ_GxnPAWI/m/54sFV7AOAAAJ but > unfortunately it didn't catch on. For the moment, I have a "minimum > viable product" which builds an AST from a .mm file, displays > statements and verifies proofs, with a minimal CLI. I'd like to > round this up, and after that I'd be happy to collaborate if you want > (there are many different blocks we can work on).
Yeah, js_of_ocaml is also what I was planning to use. More specifically, I was going to use https://github.com/janestreet/bonsai to make the UI bits. It's a strange and rather difficult to comprehend library [1], but I've found that it makes building composable components rather easy. I'd be interested in collaborating, and I would be happy to explain how Bonsai works if we end up using it for a UI. One aspect of this UI that I would like to make polished is a visualization/debugger of how the proof progresses. My current vision is that the user gets to see the formulas on the stack and the formulas in the "heap" (to borrow Mario's analogy for how Z works). You can step forward through the proof, which will animate through all the unification and substitution steps involved in using an assertion. In my mind, good animations would be a big win over the static html pages that comprise the current proof explorer. Also, being able to step forward and backward through proof steps seems to match much better with how verification actually works. [1] Bonsai is difficult and strange in sort of the same way that Monads are difficult and strange. Now that I am familiar and well practiced in using Bonsai, I find it really easy and natural to do pretty much anything I want to. -- 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/20220503185812.2f5e3569%40ithilien.
