On Sat, Nov 13, 2021 at 12:07 PM Antony Bartlett <[email protected]> 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. -- 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/CAFXXJSsBc6cEs%2BnbfRF4J%3DuPB5Xy1Uqfihv%3DBf7KQw2f8Xck7A%40mail.gmail.com.
