On Tuesday, May 3, 2022 at 7:23:19 AM UTC+2 Philip White wrote: > Unrelated: my verifier is also in OCaml. I don't expect it to set any > speed records; my ambition is more in the direction of making a web-based > proof visualization tool, and perhaps also a proof assistant UI. >
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). Benoît -- 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/e0beefbb-948d-4f7b-98f5-c9dfa07dec67n%40googlegroups.com.
