Thanks to Github user @jcaesar, Metamath does now run in browser here https://d1mtql0za68dbm.cloudfront.net/
(of the browsers I've tried, Chrome, Firefox, and Edge work fine, Safari does not. Also wont work on the official WebAssembly.sh site. The reason for these limitations relate to Metamath being an interactive program and a JavaScript class called SharedByteArray. Further details here https://github.com/jcaesar/wapm-pkg/issues/1) I've not battle-tested it because to be honest at this point I'm more interested in working on tooling, so while it should be treated with due caution, it can probably do everything running natively can. On 30th Sept, Mario wrote: > I have had success in the past compiling Rust projects to WASM Good, because I've tried to give metamath-knife the same treatment, so you'll probably be interested to know that the "filetime" package used by metamath-knife does not currently support WASM. https://github.com/alexcrichton/filetime/blob/master/src/wasm.rs $ metamath-knife --timing --verify set.mm thread 'main' panicked at 'not implemented', /usr/local/cargo/registry/src/github.com-1ecc6299db9ec823/filetime-0.2.15/src/wasm.rs:23 :5 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace (also multi-threading isn't supported in browser) $ metamath-knife --timing --jobs 4 --split --verify set.mm thread 'main' panicked at 'failed to spawn thread: Error { kind: Unsupported, message: "operation not supported on this platform" }', /rustc/59eed8a2aac0230a8b53e89d4e99d55912ba6b35/library/std/src/thread/mod.rs:628 :29 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace The branch where I've been playing with this can be found here https://github.com/Antony74/metamath-knife/tree/feature/wasm Hope some of that is helpful, Best regards, Antony On Wed, Oct 6, 2021 at 1:28 PM Antony Bartlett <[email protected]> wrote: > Thanks Mario, that's definitely on my radar now! As is learning some > Rust, eventually. > > I tend to see WASM as a way of making use of pre-existing code, and > TypeScript tends to be my preferred language for writing new code (leaving > behind 20 years of C++ after gradually completing the switch), but I know > there's great people doing new work with WASM too. > > Until metamath-knife achieves world domination, I believe there's still > value in both approaches. > > My initial plan for metamath.wasm would be to do a version of the html > proof explorer as a Single Page App. This would make the transition > navigating between proofs almost instantaneous, because a copy of metamath > running in the browser could generate html much faster than it can be > downloaded from an external server. This would provide both a quick-win in > terms of demonstrating value, and a handy proof-picking component to launch > subsequent experiments from. > > After that, my interest is in drag-and-drop proof assistants like QED ( > https://www.math.ucla.edu/~tao/QED/QED.html) and the Incredible Proof > Machine (https://incredible.pm), both of which are just educational toys > compared to the mathematics that has been achieved with Metamath. > > Best regards, > > Antony > > > On Thu, Sep 30, 2021 at 12:30 PM Mario Carneiro <[email protected]> wrote: > >> 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 >> <https://groups.google.com/d/msgid/metamath/CAFXXJSs4y59VUgNpxSWgXJSKJXv2m5dzLWz%3D9yGtOTtvxZzk0Q%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/CAJ48g%2BCchLEkfgCAEFcCi_0BxL_2EXV1atbFQ%2BZ3Mb6TU_HDqg%40mail.gmail.com.
