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.
On Sat, Nov 13, 2021 at 6:12 PM Mario Carneiro <[email protected]> wrote: > > > 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/CAFXXJStkuNs05_cW4ENxEZ0DV3Afkt2gdmwAqRFEx14HvqgPEA%40mail.gmail.com.
