search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.26k stars 1.48k forks source link

Build Python distributions targeting wasm #7418

Open Zac-HD opened 4 days ago

Zac-HD commented 4 days ago

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 commented 4 days ago

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 commented 4 days ago

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 commented 16 hours ago

@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 commented 15 hours ago

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.