Running in the browser is one of the goals for the (budding) metamath-knife community verifier / proof assistant: https://github.com/david-a-wheeler/metamath-knife/ . It's written in Rust, and I have had success in the past compiling Rust projects to WASM, but the web frontend for metamath-knife has not yet been written. IIRC there was a prototype of smm3 in the browser, which can probably be lightly adapted to get mm-knife working too. If you are interested in pursuing this, I would encourage you to redirect your efforts to mm-knife instead. It also has a permissive license (MIT/Apache instead of GPL v2+ for metamath.exe), which was brought up on the reddit thread.
Mario On Thu, Sep 30, 2021 at 7:05 AM Antony Bartlett <[email protected]> wrote: > Hi, > > I don't know if anyone else has tried this, but I think it may be of > interest to a few people here that I'm making an (ongoing) effort to build > Metamath for the WebAssembly (WASM) platform. > > The goal is to be able to use Metamath's functionality in dynamic > JavaScript web-pages. Obviously proof validation is readily available for > most major programming languages, and it's not *that* hard to write one's > own prover, but some Metamath's richer functionality can't be found > anywhere else (except maybe mmj2), at least until there is a community > verifier, as has also been mooted here. I've particularly got my eye on > html generation, and the unification algorithm. > > Usually I'd prefer to report only my successes, but, well, as you'll see > from the following two posts linked below, I have been asking for help: > > > https://www.reddit.com/r/WebAssembly/comments/pvye5u/porting_command_line_program_to_wasm_and/ > > https://github.com/wasmerio/wasmer/issues/2589 > > (and my own posts have started appearing in my Google search queries, so > it's not like I could keep this a secret even if I wanted to anyway ;-) > > Best regards, > > Antony > > -- > 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/CAJ48g%2BAUE%3D3qB2PDeDXcqNOg%3DDyT0tBfnTX97XjOKdOV7ukjEw%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAJ48g%2BAUE%3D3qB2PDeDXcqNOg%3DDyT0tBfnTX97XjOKdOV7ukjEw%40mail.gmail.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/CAFXXJSs4y59VUgNpxSWgXJSKJXv2m5dzLWz%3D9yGtOTtvxZzk0Q%40mail.gmail.com.
