pschanely
Publish a wasm build so Crosshair can be used on the client-side web
Once Z3 has a python-wasm build (https://github.com/Z3Prover/z3/issues/7418), the only thing between me and client-side demos of Hypothesis + Crosshair is a little bit of native code in Crosshair itself. (since it's pure-python, hypothesis-crosshair already works)
Not urgent but it would be very cool to get this demo working 😁
Oooh. That would be fun. Just starting to look at this stuff. cibuildwheel suggests that pyodide is supported in 3.12, but that PyPI doesn't yet support it. So does "publish" essentially just mean the creation of a correct meta.yaml file?
Noting that this won't help much until Z3 goes through the same process, we can either do a pyodide in-tree or out-of-tree build (newer docs). micropip.install(url) works, so I think there's good reason to imitate Numpy and go with out-of-tree.
This is all still pretty experimental still - wasm is a tier two CPython platform though so I do expect things to stabilize eventually.
I'll take a look today! You'd be ok with any publicly-accessible URL for the wheel I presume?
Made progress today. Looks like I'll need to relax my z3 version constraint and try again, but I'm close.
I suppose if all this works, I should re-do https://crosshair-web.org too.
@pschanely were you able to get this working? If so I would love to steal from your approach! I'm currently shimming the z3 wasm bindings in this repo with a python script to build a pure-python pyodide compatible z3 build for the subset of the library required by estimates, but this is quite hacky and I would much rather be using an officially supported version.
@leohentschker I got it sort of working, but never tried to really scale it. But essentially I am:
- building a pyodide wheel as a github artifact with this workflow
- and using this z3 pyodide wheel.
- and then have an html file like this:
<!doctype html>
<html>
<head>
<script src="https://cdn.jsdelivr.net/pyodide/v0.27.7/full/pyodide.js"></script>
</head>
<body>
Pyodide test page <br>
Open your browser console to see Pyodide output
<script type="text/javascript">
async function main(){
let pyodide = await loadPyodide();
await pyodide.loadPackage("micropip");
const micropip = pyodide.pyimport("micropip");
await micropip.install("http://127.0.0.1:8000/z3_solver-4.13.4.0-py3-none-pyodide_2024_0_wasm32.whl");
await micropip.install("http://127.0.0.1:8000/crosshair_tool-0.0.93-cp312-cp312-pyodide_2024_0_wasm32.whl");
console.log(pyodide.runPython(`
import sys
print(sys.version)
from crosshair.core_and_libs import standalone_statespace, proxy_for_type
with standalone_statespace as space:
x = proxy_for_type(int, "x")
space.add(x + 30 == 100)
print("can x be 70?: ", space.is_possible(x == 70))
print("can x be 71?: ", space.is_possible(x == 71))
`));
}
main();
</script>
</body>
</html>
Oh exciting! I misread that thread and assumed there were lingering issues with the wheel. I tested out the release and it's working for my purposes (and I believe will resolve a few issues I introduced in my own shim). Thanks for the help!