An attempt to build Metamath for WebAssembly (WASM)

[Antony Bartlett]

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

[Mario Carneiro]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BAUE%3D3qB2PDeDXcqNOg%3DDyT0tBfnTX97XjOKdOV7ukjEw%40mail.gmail.com.

[Antony Bartlett]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs4y59VUgNpxSWgXJSKJXv2m5dzLWz%3D9yGtOTtvxZzk0Q%40mail.gmail.com.

[Antony Bartlett]

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

[Mario Carneiro]

On Sat, Nov 13, 2021 at 12:07 PM Antony Bartlett <a...@akb.me.uk> wrote:

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)

It's a bit slower than native, but not too much. I tried running it and it managed to check set.mm in 18.4 s, compared to 8 or 9 seconds native. Looks like a success!

 

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

 

Yes, WASM is an unusual OS, so it is not that unusual to have to turn some features off via #[cfg(not(target_arch = "wasm32"))] when targeting it. I had to do something similar for MM0, and it wasn't too bad, but obviously no one has looked into this for metamath-knife yet. Probably a PR is in order.

[Mario Carneiro]

I tried testing metamath-knife on wasm32-unknown-unknown target, and it seems to build fine without any changes. The CLI tool probably won't work, but probably you want to be using the library in a different way anyway; the CLI is just a frontend to the library that doesn't make much sense on the web.

[Antony Bartlett]

> I tried testing metamath-knife on wasm32-unknown-unknown target, and it seems to build fine without any changes. The CLI tool probably won't work, but probably you want to be using the library in a different way anyway; the CLI is just a frontend to the library that doesn't make much sense on the web.

You are quite right of course!  Putting the two CLI programs side-by-side was only ever intended to be a bit of fun.

Having the Metamath CLI in browser means a bit more than that, though.  It means people could try it out before installing on their computer - or even never install it if they're on a locked-down computer and can't (pity set.mm is too big to be edited in github.com's web interface, actually, because then one could be completely independent without ever having to leave the browser environment).

> It's a bit slower than native, but not too much. I tried running it and it managed to check set.mm in 18.4 s, compared to 8 or 9 seconds native. Looks like a success!

Thanks!  But no, it was never going to win a race! :-)

    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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStkuNs05_cW4ENxEZ0DV3Afkt2gdmwAqRFEx14HvqgPEA%40mail.gmail.com.