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.

[NikolajBjorner]

Once adding -fexceptions the error changed to be related to threads. After adding some of the flags used by the wasm build it gets further. It now fails somewhere else with a memory bounds bug.

https://github.com/Z3Prover/z3/actions/runs/11866498035/job/33073294477

I have closed the issue on pyodide even though the error message always says to contact maintainers of pyodide.
The trick appears to be to use the appropriate compilation flags. The WASM build already mixes an exquisitely
sublime cocktail of build flags. https://github.com/Z3Prover/z3/blob/master/src/api/js/scripts/build-wasm.ts

[NikolajBjorner]

It gets much further if building Z3_SINGLED_THREADED. This is consistent with how wasm is built.
I don't recall why exactly single threaded is needed, but I can see that -pthread compile options don't work directly.
It complains that std::atomic isn't supported (old C++?), add -latomic, it complains that LTO fails.
Right now it fails the doc-test with ParOr and ParThen. They would need to be disabled or changed if z3 is single threaded,
either by exposing information that z3 is single threaded over the API or some other way by selecting doc tests.

[NikolajBjorner]

ended up redefining par or/and tactics in single threaded mode to sequential
750dd68

What are the next steps, what is the distribution story?

[rhelmot]

The .whl file is the ultimate distribution artifact here. If you upload it, people can download and install it. I don't think there's any place you can upload pyodide wheels right now to make them automatically available.

[NikolajBjorner]

This?

- name: Create build artifact
  run: |
     mkdir -p ~/build-artifacts
     cp ~/env-pyodide/lib/python*/site-packages/*.whl ~/build-artifacts/

[rhelmot]

I would go for src/api/python/dist/*.whl

[NikolajBjorner]

copilot suggestion looks shady for some more reasons too.

[NikolajBjorner]

It is live.
Next step seems to be to register with micropip.

<!DOCTYPE html>
<html>
<head>
  <meta charset="UTF-8">
  <meta name="viewport" content="width=device-width, initial-scale=1.0">
  <title>Pyodide Example</title>
</head>
<body>
  <div id="output"></div>
  <script type="text/javascript" src="https://cdn.jsdelivr.net/pyodide/v0.26.2/full/pyodide.js"></script>
<script type="text/javascript">
  async function main() {
    let pyodide = await loadPyodide();
    await pyodide.loadPackage("micropip");
    const micropip = pyodide.pyimport("micropip");
      await micropip.install("./z3_solver-4.13.4.0-py3-none-pyodide_2024_0_wasm32.whl");


      pyodide.runPython(`
        from z3 import *
        # Your Python code here
        x, y = Ints('x y')
        result = f"{(simplify(2 + x >= 2))}"
        from js import document
        document.getElementById("output").innerText = result
      `);
    }
    main();
  </script>
</body>
</html>
    

[NikolajBjorner]

pypi will not host it from what you say and what I can see.

I put it here:

https://microsoft.github.io/z3guide/z3_solver-4.13.4.0-py3-none-pyodide_2024_0_wasm32.whl

The sample above works with loading from that location instead of localhost.

The better solution is to upload it as a release artifact and have it accessible from z3prover releases. I am not sure the slicker way? Add to release.yaml?

Since there now is a pyodide package, which is the original objective of this issue. I am closing it even as there is more fiddling. Use it or lose it.

[pschanely]

The is very neat stuff. I noticed when trying out pyodide+CrossHair that I'm seeing immediate unsats with a reason of "unclassified exception" when attempting to apply a TryFor tactic; here is a snippet to reproduce using your html template above:

from js import document
import z3

tactic = z3.Tactic("smt")
tactic = z3.TryFor(tactic, 100_000)  # commenting this line will make the check satisfiable
solver = tactic.solver()

x = z3.Int("x")
solver.add(x > 10)

# This will display "unknown - unclassified exception":
document.getElementById("output").innerText = f"{solver.check()} - {solver.reason_unknown()}"

Possibly this would be intended based on the cocktail of compile flags we're using, but @NikolajBjorner, maybe you would know?

[NikolajBjorner]

I am observing this too.
It passed the basic doc tests, but when I try calling the solver it throws an internal exception. To start with I am trying to track the exception with more descriptive information: 5168a13
A clue may be inferred based on build flags for js not yet used for pyodide and build warnings for the pyodide build.

[NikolajBjorner]

Status:
It throws an exception when it attempts to create a thread in the "scoped_timer" class.
Z3 uses threads to manage timeouts. The timeout lives on a stand-alone thread.

Thus, we are hitting issues related to pyodide/pyodide#237

For the JS bindings, there were some related issues. They were addressed, but I am not sure exactly what all the relevant ingredients are at this point. The SharedArrayBuffer was introduced at some point. Other functions are declared as async so presumably it is legal to spawn a thread within an async but not on the main browser thread or something.

Some more context on what precisely works will be required for emscripten+pyodide beyond build flags will be required.

[NikolajBjorner]

Status: the timeout event doesn't use threads in the pyodide build.
Basic functionality that previously wasn't working now functions correctly.
I still get exceptions, such as

https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#solvers

(hit Run twice since we have yet to deal with that we don't pre-cache the pyodide runs and therefore show a spurious error message)

F12 provides a stack deep inside of pyodide with a call to contact maintainers.