mirror of
https://github.com/Z3Prover/z3
synced 2026-06-23 00:50:29 +00:00
3bf4d2b53d
## Summary z3 already builds under Pyodide (there is a `pyodide.yml` workflow and an `IS_PYODIDE` path in `setup.py`), but that path uses `pyodide build` and produces a wheel tagged `emscripten_<pyodide-version>_wasm32`, which is pinned to a single Pyodide release and rejected by PyPI — so today it's only usable as a CI artifact. [PEP 783](https://peps.python.org/pep-0783/) introduced the portable `pyemscripten_<date>_wasm32` platform tag that **PyPI accepts** and `micropip` can install at runtime. This makes `z3-solver` build that wheel via `cibuildwheel --platform pyodide`. ## Changes - **`setup.py`** — for the emscripten target, use the wheel platform tag that pyodide-build provides verbatim via `_PYTHON_HOST_PLATFORM` (e.g. `pyemscripten_2026_0_wasm32`) instead of reconstructing an `emscripten_*` tag. Falls back to the previous behaviour when that env var is absent. - **`setup.py` / `CMakeLists.txt` / `pyproject.toml`** — switch the Pyodide build from JS-based exceptions (`-fexceptions`, `-sDISABLE_EXCEPTION_CATCHING=0`) to **native wasm exception handling** (`-fwasm-exceptions -sSUPPORT_LONGJMP=wasm`), matching the ABI of the Pyodide 314 / emscripten 5 main module. With the old flags `libz3.so` imports `invoke_*` trampolines the runtime no longer provides, so the wheel builds but the first `Z3_mk_config` call fails at runtime with `Dynamic linking error: cannot resolve symbol invoke_vi`. - **`pyproject.toml`** — add `[tool.cibuildwheel]` / `[tool.pyodide.build]` so `cibuildwheel --platform pyodide` builds and tests the wheel (`cp314`). - **`.github/workflows/pyodide-pypi.yml`** (new) — build with cibuildwheel and publish to PyPI (trusted publishing) on tags. Existing `pyodide.yml` unchanged. ## Verification Built with `cibuildwheel 4.1.0` / `pyodide-build 0.35.0` / `emscripten 5.0.3`, CPython 3.14 / Pyodide 314: - Produces `z3_solver-4.17.0.0-py3-none-pyemscripten_2026_0_wasm32.whl`. - `z3test.py` passes in the Pyodide runtime (node + wasm32). - Installed via `micropip` and solves SMT problems both under node and in a browser (`sat` with a model, `unsat` for a contradiction). 🤖 Generated with [Claude Code](https://claude.com/claude-code) 🕵️♂️ Reviewed by [Alcides Fonseca](https://wiki.alcidesfonseca.com) Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| c++ | ||
| dll | ||
| dotnet | ||
| go | ||
| java | ||
| js | ||
| julia | ||
| mcp | ||
| ml | ||
| python | ||
| api_algebraic.cpp | ||
| api_arith.cpp | ||
| api_array.cpp | ||
| api_ast.cpp | ||
| api_ast_map.cpp | ||
| api_ast_map.h | ||
| api_ast_vector.cpp | ||
| api_ast_vector.h | ||
| api_bv.cpp | ||
| api_config_params.cpp | ||
| api_context.cpp | ||
| api_context.h | ||
| api_datalog.cpp | ||
| api_datalog.h | ||
| api_datatype.cpp | ||
| api_finite_set.cpp | ||
| api_fpa.cpp | ||
| api_goal.cpp | ||
| api_goal.h | ||
| api_log.cpp | ||
| api_model.cpp | ||
| api_model.h | ||
| api_numeral.cpp | ||
| api_opt.cpp | ||
| api_params.cpp | ||
| api_parsers.cpp | ||
| api_pb.cpp | ||
| api_polynomial.cpp | ||
| api_polynomial.h | ||
| api_qe.cpp | ||
| api_quant.cpp | ||
| api_rcf.cpp | ||
| api_seq.cpp | ||
| api_solver.cpp | ||
| api_solver.h | ||
| api_special_relations.cpp | ||
| api_stats.cpp | ||
| api_stats.h | ||
| api_tactic.cpp | ||
| api_tactic.h | ||
| api_util.h | ||
| CMakeLists.txt | ||
| z3.h | ||
| z3_algebraic.h | ||
| z3_api.h | ||
| z3_ast_containers.h | ||
| z3_fixedpoint.h | ||
| z3_fpa.h | ||
| z3_logger.h | ||
| z3_macros.h | ||
| z3_optimization.h | ||
| z3_polynomial.h | ||
| z3_private.h | ||
| z3_rcf.h | ||
| z3_replayer.cpp | ||
| z3_replayer.h | ||
| z3_spacer.h | ||
| z3_v1.h | ||