search

pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
1.03k stars 49 forks source link

Publish a wasm build so Crosshair can be used on the client-side web #314

Open Zac-HD opened 1 month ago

Zac-HD commented 1 month ago

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 😁

pschanely commented 1 month ago

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?

Zac-HD commented 1 month ago

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.

Zac-HD commented 6 days ago

Z3 now has a wasm wheel (🎊), which I think puts this back in your hands!

pschanely commented 5 days ago

I'll take a look today! You'd be ok with any publicly-accessible URL for the wheel I presume?

pschanely commented 4 days ago

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.