Closed Antony74 closed 2 years ago
weiqingtangx
commented
2 years ago (base) ➜ complex em++ --bind -o fib2.wasm fib2.cc --no-entry -O3 (base) ➜ complex wasmer fib2.wasm error: failed to run `fib2.wasm` ╰─> 1: Error while importing "env"."_embind_register_class": unknown import. Expected Function(FunctionType { params: > [I32, I32, I32, I32, I32, I32, I32, I32, I32, I32, I32, I32, I32], results: [] })
Same Problem
jcaesar
commented
2 years ago In short: You're running into https://github.com/wasmerio/wasmer/issues/1977#issuecomment-754747526.
The specific error message you're seeing is because wasmer checks for _emscripten_memcpy_big or __map_file to be imported when loading to decide whether to run as an emscripten binary or wasi binary. It thinks the compiled module is not an emscripten binary and doesn't provide env.system and the like.
The imports of the module:
# wasmer inspect foo.wasm
…
Imports:
Functions:
"env"."system": [I32] -> [I32]
"env"."__sys_unlink": [I32] -> [I32]
"env"."__sys_rmdir": [I32] -> [I32]
"wasi_snapshot_preview1"."fd_read": [I32, I32, I32, I32] -> [I32]
"wasi_snapshot_preview1"."fd_close": [I32] -> [I32]
"wasi_snapshot_preview1"."fd_seek": [I32, I64, I32, I32] -> [I32]
"env"."__sys_rename": [I32, I32] -> [I32]
"wasi_snapshot_preview1"."fd_write": [I32, I32, I32, I32] -> [I32]
"wasi_snapshot_preview1"."proc_exit": [I32] -> []
"wasi_snapshot_preview1"."args_sizes_get": [I32, I32] -> [I32]
"wasi_snapshot_preview1"."args_get": [I32, I32] -> [I32]
"wasi_snapshot_preview1"."clock_time_get": [I32, I64, I32] -> [I32]
"wasi_snapshot_preview1"."environ_sizes_get": [I32, I32] -> [I32]
"wasi_snapshot_preview1"."environ_get": [I32, I32] -> [I32]Normally, I'd say: "Try wasi-sdk instead, that'll give you pure WASI binaries", but I tried, and there's some problem with longjmp I don't understand. The other option might be to try some old version of emscripten that doesn't yet use wasi. (Older than 1.39.0, I tried that one.)
Antony74
commented
2 years ago The other option might be to try some old version of emscripten that doesn't yet use wasi. (Older than 1.39.0, I tried that one.)
Ah, #1640 suggests 1.38.43 or earlier, but 1.39.0 is as far back as the emscripten/emsdk containers go on dockerhub.
Guess I'll have to find a different container or learn how to install the full development environment myself after all.
Thanks for your help! :-)
jcaesar
commented
2 years ago how to install the full development environment
That should be easy with
git clone https://github.com/emscripten-core/emsdk.git \
&& cd emsdk && ./emsdk install 1.38.43 && ./emsdk activate 1.38.43Hmm, well, that appears to have installed OK, and was a lot easier than I'd been led to expect, but when I run emcc *.c -o metamath.wasm, I'm seeing more output than I should paste here, but the key repeated messages are
shared:WARNING: LLVM version appears incorrect (seeing "12.0", expected "10.0")and
missing function: $stackTraceSame if I try to build a HelloWorld program instead.
Dockerfile
FROM emscripten/emsdk:1.40.1
# Bump Emscripten version back down to 1.38.43 to maximise wasmer compatibility
WORKDIR /work
RUN git clone https://github.com/emscripten-core/emsdk.git
WORKDIR /work/emsdk
RUN ./emsdk install 1.38.43
RUN ./emsdk activate 1.38.43
RUN ln -s /usr/bin/python3 /usr/bin/python
ENV PATH="/work/emsdk:${PATH}"
ENV PATH="/work/emsdk/node/14.15.5_64bit/bin:${PATH}"
ENV PATH="/work/emsdk/fastcomp/emscripten:${PATH}"
WORKDIR /work
# Get wasmer
RUN curl https://get.wasmer.io -sSfL | sh
ENV PATH="/root/.wasmer/bin:${PATH}"
# Get the metamath source code
RUN curl http://us.metamath.org/downloads/metamath.zip -o metamath.zip
RUN unzip metamath.zip -d .
# For convenience also get set.mm
RUN curl https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm -o set.mm
# And when run, launch the shell
WORKDIR /work/metamath
CMD ["sh"]Should probably start FROM something that's not emscripten/emsdk to avoid version confusion.
FROM docker.io/library/debian:bullseye as bin
RUN apt-get update && \
export DEBIAN_FRONTEND=noninteractive && \
apt-get install -yq \
build-essential \
cmake \
curl \
file \
git \
python3 \
python \
sudo \
unzip \
&& \
apt-get clean && rm -rf /var/lib/apt/lists/* && \
useradd frust --user-group --create-home --home-dir /work --shell /bin/bash
USER frust
WORKDIR /work
RUN git clone https://github.com/emscripten-core/emsdk.git
WORKDIR /work/emsdk
RUN ./emsdk install 1.38.43
RUN ./emsdk activate 1.38.43
ENV PATH="/work/emsdk:${PATH}"
ENV PATH="/work/emsdk/node/14.15.5_64bit/bin:${PATH}"
ENV PATH="/work/emsdk/fastcomp/emscripten:${PATH}"
ENV EMSDK_NODE=/work/emsdk/node/14.15.5_64bit/bin/node
ENV EMSDK=/work/emsdk
ENV EM_CONFIG=/work/emsdk/.emscripten
WORKDIR /work
RUN curl http://us.metamath.org/downloads/metamath.zip -o metamath.zip \
&& echo 126fc3eac6699257cfcdbfb2087fb31284fdfe784bb9d6e2ea7c32b8524c3da9 \ metamath.zip | sha256sum -c \
&& unzip metamath.zip -d . \
&& rm metamath.zip
WORKDIR /work/metamath
RUN curl https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm -o set.mm \
&& echo 2a497ca6cbf422e5a58244c7ab064bd62700daa289d9e325d6a9e590ec30d0c4 \ set.mm | sha256sum -c
RUN emcc *.c -o metamath.wasm
# sorry, this isn't a serious docker image for wasmer. Just using another experiment of mine for testing
FROM liftm/wasmer:binfmt-experiment
COPY --from=bin /work/metamath/metamath.wasm /work/metamath/set.mm /
ENTRYPOINT ["/wasmer", "run", "--disable-cache", "metamath.wasm", "--"]This gets me to the metamath prompt, but trying to read set.mm fails for different reasons. Good luck with that. ;P
Antony74
commented
2 years ago That's wonderful, thanks, you were 98% there!
Therefore, very probably the final question to get this working is, how do I increase whatever memory the system is lacking, please?
Metamath - Version 0.198 7-Aug-2021 Type HELP for help, EXIT to exit.
MM> read demo0.mm
Reading source file "demo0.mm"... 1364 bytes
1364 bytes were read into the source buffer.
The source has 19 statements; 7 are $a and 1 are $p.
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
if you want to check them.
MM> verify proof *
0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
..................................................
All proofs in the database were verified in 0.00 s.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
failed to set errno!
failed to set errno!
?Sorry, there was not enough memory to read the file "set.mm".
?Error: file "set.mm" was not found
Reading source file "set.mm"... 0 bytes
?Source was not read due to error(s). Please correct and try again.
MM> exitDockerfile
FROM docker.io/library/debian:bullseye as bin
RUN apt-get update && \
export DEBIAN_FRONTEND=noninteractive && \
apt-get install -yq \
build-essential \
cmake \
curl \
file \
git \
python3 \
python \
sudo \
unzip \
&& \
apt-get clean && rm -rf /var/lib/apt/lists/*
WORKDIR /work
RUN git clone https://github.com/emscripten-core/emsdk.git
WORKDIR /work/emsdk
RUN ./emsdk install 1.38.43
RUN ./emsdk activate 1.38.43
ENV PATH="/work/emsdk:${PATH}"
ENV PATH="/work/emsdk/node/14.15.5_64bit/bin:${PATH}"
ENV PATH="/work/emsdk/fastcomp/emscripten:${PATH}"
ENV EMSDK_NODE=/work/emsdk/node/14.15.5_64bit/bin/node
ENV EMSDK=/work/emsdk
ENV EM_CONFIG=/work/emsdk/.emscripten
WORKDIR /work
RUN curl http://us.metamath.org/downloads/metamath.zip -o metamath.zip \
&& echo 126fc3eac6699257cfcdbfb2087fb31284fdfe784bb9d6e2ea7c32b8524c3da9 \ metamath.zip | sha256sum -c \
&& unzip metamath.zip -d . \
&& rm metamath.zip
WORKDIR /work/metamath
RUN curl https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm -o set.mm \
&& echo 2a497ca6cbf422e5a58244c7ab064bd62700daa289d9e325d6a9e590ec30d0c4 \ set.mm | sha256sum -c
RUN emcc *.c -o metamath.wasm
# sorry, this isn't a serious docker image for wasmer. Just using another experiment of mine for testing
FROM liftm/wasmer:binfmt-experiment
COPY --from=bin /work/metamath/metamath.wasm /work/metamath/set.mm /work/metamath/demo0.mm /
ENTRYPOINT ["/wasmer", "run", "--disable-cache", "metamath.wasm", "--"]That user you created introduced a permissions problem, so I've stripped it out.
Weird, works fine for me.
The next problem is that some part of the system doesn't have enough memory to read in set.mm
Ah, now that you say it, that's what ALLOW_MEMORY_GROWTH is for.
However, it works perfectly with demo0.mm
So does
wapm execute --emscripten metamath "read set.mm" "verify proof *" exit:) (Though of course this means running untrusted unsandboxed binaries on your system, so I'm not sure it's all that terribly useful.)
I sure would have liked it if I could use --embed-file to add set.mm and friends into the wasm binary (they're 40 MB without comments, but it's generally expected that you need to compress wasm before network transfers, as does wapm, so that's ~ok.), but that doesn't seem to work.
Antony74
commented
2 years ago Weird, works fine for me.
Disappointed to hear that, thought containerisation was supposed to have eliminated "it works for me" type problems, but never mind.
that's what ALLOW_MEMORY_GROWTH is for
So now it's working brilliantly in the limited context of your "not serious" Wasmer container, and I'm also impressed to see you've uploaded it to wapm. However, now I'm worried we have been barking up the wrong tree, as the WebAssembly shell is complaining it only supports WASI.
jcaesar
commented
2 years ago <_< I should have asked what you actually want this for.
Do you actually plan on using it on webassembly.sh?
I've tried the same thing for minisat, and had to notice that I don't even know how to put some chars into a file. (I got pissy about that and made pee, if you'll excuse the pun. It's painful to use.)
Then I noticed that minisat for some reason doesn't work on webassembly.sh and gave up. At this point, I consider the utility of webassembly.sh to be rather low...
That being said, with emscripten 2.0.31, there's only a few non-wasi functions that remain, and they're easy to patch out. The only nut I haven't cracked yet is how to get rid of env.emscripten_notify_memory_growth. That being said, no idea whether it'll yield a runnable binary.
Antony74
commented
2 years ago I plan on re-using Metamath for web development. I like the idea of running a virtual shell in the background, to give a clear separation between the two programs, and make it easier to get help if I get some output from Metamath I don't understand, but nothing's essential.
Do you remember the joke about Java, "Write Once, Debug Everywhere" ...it's starting to feel like WASM has multiple build targets too depending on what one intends to do with it, which seems a shame.
jcaesar
commented
2 years ago it's starting to feel like WASM has multiple build targets
It does. In Rust, that's actually plain obvious, as you really specify whether you want wasm32-unknown-unknown for defining your own interface, wasm32-unknown-emscripten for legacy JS things (I say legacy because I think stuff like wasm-pack uses the -unknown target), and wasm32-wasi for running outside the browser. (Ignoring wasm64-unknown-unknown here.)
It's be all fine and good if wasi was complete, but there's still quite some things you just can't do with it. Networking, for example.
The only nut I haven't cracked yet is how to get rid of
env.emscripten_notify_memory_growth.
I wasn't awake yesterday. Just needed to define
void emscripten_notify_memory_growth(size_t blubb) {}That being said, no idea whether it'll yield a runnable binary.
The binary is runnable, but doesn't import path_open. I don't know why, but I'm speculating that emscripten assigns file-descriptors to all embedded files and preopens them. So it can't read files it doesn't know about at compile time.
It's be rather sad if I'm right about this. I might have missed some compiler option.
I'm worried we have been barking up the wrong tree
I guess we have. I didn't think a recent emcc couldn't open files from disk with wasi.
Anyway, I guess this needs retargeting to wasi-sdk/wasi-libc. Maybe some day.
I think this issue has strayed far from being an issue with wasmer. Wanna close it?
jcaesar
commented
2 years ago "Try wasi-sdk instead, that'll give you pure WASI binaries", but I tried, and there's some problem with longjmp I don't understand.
On a second glance, they're just #include <setjmp.h>ing, but not using it. Snip, and it works on webassembly.sh.
Onto the last problem: where do I get a download of set.mm and friends that has a stable url with content that won't change per release. (I'm used to Isabelle releases being wonky. Was hoping others would do better…)
Antony74
commented
2 years ago Sorry, you're way ahead of me! :-)
Yes of course this can be closed, it's not really Wasmer-related, is it.
So you'd like to embed set.mm within metamath.wasm? That takes away some flexibility and falls short of full shell integration, but it does cover the majority of users and uses, and would enable me to focus on web development where I might not be completely out of my depth and should be able to do interesting and useful things.
This was covered on the Metamath mailing list a few years ago - let me see if I can dig that out for you (and while we're there I'd better find my post from last week about WASM for you). set.mm is something of a poster-child for continuous deployment, given how multiple independently developed verifiers are run automatically before anything is accepted into the repo, but I think they may have found a compromise for distributions that require something immutable.
jcaesar
commented
2 years ago So you'd like to embed set.mm within metamath.wasm?
Not necessarily in the wasm itself. wapm has a feature for shipping files (example) together with the binary. You could load them like read "wapm/set.mm", which I guess would make it useless in the sense of a "standard distribution" because you'd have to $[ wapm/set.mm $], but nicer for one-off experiments on webassembly.sh. Not sure if it's really a good idea.
(I'll also have to check how well those included files get compressed, 50 MB is a bit too much, 15 might be bearable...)
Optimally, I'd actually like to leave it as is and tell people to get the files themselves, but neither github.io nor metamath.org set the necessary CORS headers for the webassembly.sh's curl to work. :( (Plus there's no tar or unzip.)
let me see if I can dig that out
Yes please.
Antony74
commented
2 years ago neither github.io nor metamath.org set the necessary CORS headers for the webassembly.sh's curl to work
Hmm. I seem to be able to curl set.mm fine.
jcaesar
commented
2 years ago CORS behavior differences between FF and Chrome. Yay.
Nevermind. I should mind my uMatrix. curl https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm -o set.mm works just fine. I guess I'll slap that into the README and call it a day.
Antony74
commented
2 years ago Then it perhaps doesn't matter that set.mm does seem to be included with metamath.zip etc. such that downloading the latest version isn't strictly necessary. Or that I was actually using Safari.
jcaesar
commented
2 years ago Or that I was actually using Safari.
ooooo.
Metamath downloads: http://us.metamath.org/#mmprog Packaging Metamath for Linux distros Then it perhaps doesn't matter that set.mm does seem to be included with metamath.zip
Yeah, about that... Having stable download URL with stable content would be really nice. For one, because metamath.org doesn't offer https (wat...), and the only way I have to at least somewhat verify the download is by fingerprint. Which I can't do if the downloaded content changes dynamically.
If you'd like to see an (unrelated) place where this is a problem, try building metamath on Arch Linux.
==> Validating source files with md5sums...
metamath.tar.gz ... FAILED(Sorry if I'm preaching to the choir here.)
Which is why I switched to downloading the github releases. I suppose I should have posted the link. https://github.com/jcaesar/wapm-pkg/blob/04560c33e285bfd164f6e9306cffc8834e99525c/metamath/Dockerfile#L28
I wonder though: How much do the versions of metamath and set.mm have to match?
html proof explorer as a Single Page App interest is in drag-and-drop proof assistants
Ah, interesting. I suspect that compiling the metamath executable as is and communicating with it through wasi would be rather painful for that purpose. You might want to build a library on top of the current metamath source. That you can then compile with emscripten and use it's nice facilities for bindings between wasm and js. In turn, you won't need wasi at all.
Question though: Why'd you try running metamath on wasmer, outside of the web, if the web is your target?
Antony74
commented
2 years ago Which is why I switched to downloading the github releases. I suppose I should have posted the link.
Yes, that's impressive work! Well done, and thank you! :-)
Question though: Why'd you try running metamath on wasmer, outside of the web, if the web is your target?
Um, because Metamath is a command line program and wasmer is for command line programs, and I'm spoilt by nodejs, and thus used to command line JavaScript being almost the same as web JavaScript. Wouldn't have been such a terrible idea if the WASI support was complete consistently across the board, would it? Not so smart in hindsight, sorry. Even now I'm not sure I appreciate the finer points in terms of the distinction between wasmer, @wasmer/cli, and @wasmer/wasm-terminal.
Summary
Hi, I'm wondering what I need to know in order to understand and work on a fix to move past this error message please?
Additional details
And here's the containerised build environment I'm currently using (happy to take alternative suggestions for this)
Dockerfile
usage: