Build Python distributions targeting wasm

[Zac-HD]

Webassembly is now a supported platform for CPython, and can be used via e.g. the Pyodide project to produce in-browser tools. I'd love to get Z3-backed testing working in this demo of hypothesis-crosshair, for example.

Since Z3 already has wasm builds for js, and many Python libraries with native extensions already support wasm (e.g.), I'm confident that this is practical - if also a bit fiddly to set up.

[NikolajBjorner]

I tried integrating wasm two years ago over the course of a couple of weeks.
There was/is a branch for z3 in pyodide for the integration.
I haven't checked how pyodide has evolved since.
There were some significant obstacles just in building z3 nwasm as part of the build process for pyodide. It used (uses?) a mode where all the plugins are built in the main pipeline. Z3 hogged more resources than others for just the build.

Obviously currently, there isn't any python wheel with WASM build. Presumably, this is precisely what pyodide would help with.
If you can get it running, great.

[Zac-HD]

I don't see the branch, but fortunately pyodide does support out-of-tree builds now and I'll try it out when I get some time.

[NikolajBjorner]

@rhelmot - I poked at this a bit. pyodide build seems to require something equivalent to
"python3 -m build --sdist" from the api/python directory.
The error messages suggest the format of setup.py and the toml file have to be updated.

[rhelmot]

Hmm... we should be fully compliant with the appropriate standards. The only thing I can think which might be an issue is it might try to copy the subtree rooted at the setup.py file in isolation, which will make it not possible to copy the proper z3 sources. I'll take a look soon.

[rhelmot]

Finally got around to this. I was able to build the pyodide wheel with minor modifications to setup.py, but running z3test.py yields the following error:

[+] ~/proj/emolabs/z3/src/api/python% python z3test.py                         (.venv-pyodide) audrey@dandelion [10:03:22 PM]
Pyodide has suffered a fatal error. Please report this to the Pyodide maintainers.
The cause of the fatal error was:
CppException is_non_propositional_predicate::found: The exception is an object of type is_non_propositional_predicate::found a
t address 27674504 which does not inherit from std::exception
    at convertCppException (/home/audrey/proj/emolabs/z3/src/api/python/.pyodide-xbuildenv-0.29.0/0.27.0a2/xbuildenv/pyodide-r
oot/dist/pyodide.asm.js:10:47783)
    at API.fatal_error (/home/audrey/proj/emolabs/z3/src/api/python/.pyodide-xbuildenv-0.29.0/0.27.0a2/xbuildenv/pyodide-root/
dist/pyodide.asm.js:10:48076)                                                                                                 
    at main (/home/audrey/proj/emolabs/z3/src/api/python/.pyodide-xbuildenv-0.29.0/0.27.0a2/xbuildenv/pyodide-root/dist/python
:189:17) {
  ty: 'is_non_propositional_predicate::found',
  pyodide_fatal_error: true                                                                                                   
}                                                                                                                             
Stack (most recent call first):          
  File "/home/audrey/proj/emolabs/z3/src/api/python/z3/z3core.py", line 4270 in Z3_solver_check_assumptions
  File "/home/audrey/proj/emolabs/z3/src/api/python/z3/z3.py", line 7181 in check
  File "<doctest z3.z3[6]>", line 1 in <module>
  File "/lib/python312.zip/doctest.py", line 1359 in __run
  File "/lib/python312.zip/doctest.py", line 1523 in run
  File "/lib/python312.zip/doctest.py", line 1996 in testmod
  File "/home/audrey/proj/emolabs/z3/src/api/python/z3test.py", line 11 in <module>
CppException is_non_propositional_predicate::found: The exception is an object of type is_non_propositional_predicate::found a
t address 27674504 which does not inherit from std::exception
    at convertCppException (/home/audrey/proj/emolabs/z3/src/api/python/.pyodide-xbuildenv-0.29.0/0.27.0a2/xbuildenv/pyodide-r
oot/dist/pyodide.asm.js:10:47783)
    at API.fatal_error (/home/audrey/proj/emolabs/z3/src/api/python/.pyodide-xbuildenv-0.29.0/0.27.0a2/xbuildenv/pyodide-root/
dist/pyodide.asm.js:10:48076)
    at main (/home/audrey/proj/emolabs/z3/src/api/python/.pyodide-xbuildenv-0.29.0/0.27.0a2/xbuildenv/pyodide-root/dist/python
:189:17) {                 
  ty: 'is_non_propositional_predicate::found',      
  pyodide_fatal_error: true
}            

Do you know what this is about? Should I submit the PR or is this indicative of some sort of big architectural incompatibility with the platform?

[NikolajBjorner]

Thanks, I have been busy coding on something else.
Probably the saner approach is that I make z3_exception inherit from std::exception and change methods in z3_exception to use the "what" method.

[NikolajBjorner]

9206546

[rhelmot]

still getting the same error after that commit. Do you want me to add pyodide CI so you can test this yourself?

[NikolajBjorner]

Ha, I was just updating this thread essentially asking if you could add a CI so I can fix it on my side?

[NikolajBjorner]

I would have to swap context to set up an actual pyodide build locally, so a CI would be much better. Also it could, if appropriate, be part of WASM action at some point.

I added several more commits after that one to take care of structs that didn't inherit from std::exception

[rhelmot]

I have a preliminary build step for wasm CI on the pyodide-ci branch, but the building seems to run the poor azure pipelines box out of memory during the linking stage. I think if we can turn off LTO it'll work fine, but for something like Z3 that seems important...

see https://dev.azure.com/Z3Public/Z3/_build/results?buildId=7659&view=logs&j=2f68f21a-4f23-5f18-1620-f32fb059cc4b&t=70bb1769-113b-52cf-d677-1cc690cb0a72 for build logs

[NikolajBjorner]

memory issues have been intermittent before.
I will try the build again (a couple of times) to start with.

[NikolajBjorner]

Looks like Azure DevOps is set up to run the pipeline from Master when I select to rerun.
I am adding a github workflow/action to perform this build step.
I already moved out windows builds from the azure-pipelines.yml flow as it was too error prone and the github setup tends to work better.

[NikolajBjorner]

https://github.com/Z3Prover/z3/actions/runs/11849447202/job/33022697026

[NikolajBjorner]

I think there is a typo in your branch:

source ~/emsdk/emsdk_emv -> source ~/emsdk/emsdk_env

After changing this, the Github Action fails further down the line.

Given that Azure pipelines are overloaded and flaky, I wonder if making progress on the GitHub action version is going to be easier. The current break is:

Run source ~/emsdk/emsdk_env.sh && ~/env/bin/pyodide venv ~/env-pyodide
  
Setting up EMSDK environment (suppress these messages with EMSDK_QUIET=1)
Adding directories to PATH:
PATH += /home/runner/emsdk
PATH += /home/runner/emsdk/upstream/emscripten

Setting environment variables:
PATH = /home/runner/emsdk:/home/runner/emsdk/upstream/emscripten:/snap/bin:/home/runner/.local/bin:/opt/pipx_bin:/home/runner/.cargo/bin:/home/runner/.config/composer/vendor/bin:/usr/local/.ghcup/bin:/home/runner/.dotnet/tools:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games
EMSDK = /home/runner/emsdk
EMSDK_NODE = /home/runner/emsdk/node/20.18.0_[6](https://github.com/Z3Prover/z3/actions/runs/11850139005/job/33024542956#step:8:6)4bit/bin/node
Downloading xbuild environment                                                  
Installing xbuild environment                                                   
Creating Pyodide virtualenv at /home/runner/env-pyodide                         
Expected host Python version to be 3.11 but got version 3.[10](https://github.com/Z3Prover/z3/actions/runs/11850139005/job/33024542956#step:8:11)

So python isn't just python.

[NikolajBjorner]

hmm, you are bypassing me now. I was going to try pip install pyodide-cli per friendly AI suggestion/hallucination

[NikolajBjorner]

Looks like we should follow instructions at this point and file with pyodide devs.

https://github.com/Z3Prover/z3/actions/runs/11851278844/job/33027495365

[NikolajBjorner]

pyodide/pyodide#5203

[NikolajBjorner]

I wonder, it could very well be the following:

https://emscripten.org/docs/porting/exceptions.html

It says to pass a compile flag to enable exceptions.