> 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
On Sun, Nov 14, 2021 at 12:21 AM Mario Carneiro <[email protected]> wrote:
> 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
> <https://groups.google.com/d/msgid/metamath/CAFXXJStkuNs05_cW4ENxEZ0DV3Afkt2gdmwAqRFEx14HvqgPEA%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%2BApuHB8EJSxHP0t2bpS9t6bFxg%2BHwOc0aDhTTks4RF4Ug%40mail.gmail.com.
