mirror of
https://github.com/Z3Prover/z3
synced 2026-06-20 07:36:31 +00:00
78818f9ae1
z3 already builds under Pyodide, but via `pyodide build` the resulting wheel is tagged `emscripten_<pyodide-version>_wasm32` and only usable as a CI artifact. PEP 783 introduced the portable `pyemscripten_<date>_wasm32` tag that PyPI accepts and micropip can install at runtime. This makes z3 produce that wheel via `cibuildwheel --platform pyodide`. Changes: * setup.py: for the emscripten target, use the wheel platform tag that pyodide-build supplies verbatim via _PYTHON_HOST_PLATFORM (e.g. `pyemscripten_2026_0_wasm32`) instead of reconstructing an `emscripten_*` tag, falling back to the old 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 call fails at runtime with "Dynamic linking error: cannot resolve symbol invoke_vi". * pyproject.toml: add [tool.cibuildwheel] / [tool.pyodide.build] config so `cibuildwheel --platform pyodide` builds and tests the wheel. * add .github/workflows/pyodide-pypi.yml building the wheel with cibuildwheel and publishing it to PyPI (trusted publishing) on tags. The existing pyodide.yml artifact build is left unchanged. Verified with cibuildwheel 4.1.0 / pyodide-build 0.35.0 / emscripten 5.0.3: the resulting z3_solver-4.17.0.0-py3-none-pyemscripten_2026_0_wasm32.whl passes z3test.py in the Pyodide runtime and solves SMT problems both under node and in a browser via micropip. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| shared | ||
| a3-python.lock.yml | ||
| a3-python.md | ||
| academic-citation-tracker.lock.yml | ||
| academic-citation-tracker.md | ||
| agentics-maintenance.yml | ||
| android-build.yml | ||
| api-coherence-checker.lock.yml | ||
| api-coherence-checker.md | ||
| build-warning-fixer.lock.yml | ||
| build-warning-fixer.md | ||
| build-z3-cache.yml | ||
| ci.yml | ||
| code-conventions-analyzer.lock.yml | ||
| code-conventions-analyzer.md | ||
| code-simplifier.lock.yml | ||
| code-simplifier.md | ||
| compare-stats-anomaly-reporter.lock.yml | ||
| compare-stats-anomaly-reporter.md | ||
| copilot-setup-steps.yml | ||
| coverage.yml | ||
| cross-build.yml | ||
| csa-analysis.lock.yml | ||
| csa-analysis.md | ||
| docs.yml | ||
| fstar-master-build.yml | ||
| issue-backlog-processor.lock.yml | ||
| issue-backlog-processor.md | ||
| mark-prs-ready-for-review.yml | ||
| memory-safety-report.lock.yml | ||
| memory-safety-report.md | ||
| memory-safety.yml | ||
| msvc-static-build-clang-cl.yml | ||
| msvc-static-build.yml | ||
| nightly-validation.yml | ||
| nightly.yml | ||
| nuget-build.yml | ||
| ocaml.yaml | ||
| ostrich-benchmark.lock.yml | ||
| ostrich-benchmark.md | ||
| pyodide-pypi.yml | ||
| pyodide.yml | ||
| qf-s-benchmark.lock.yml | ||
| qf-s-benchmark.md | ||
| release-notes-updater.lock.yml | ||
| release-notes-updater.md | ||
| release.yml | ||
| smtlib-benchmark-finder.lock.yml | ||
| smtlib-benchmark-finder.md | ||
| specbot-crash-analyzer.lock.yml | ||
| specbot-crash-analyzer.md | ||
| tactic-to-simplifier.lock.yml | ||
| tactic-to-simplifier.md | ||
| tptp-benchmark.lock.yml | ||
| tptp-benchmark.md | ||
| wasm-release.yml | ||
| wasm.yml | ||
| Windows.yml | ||
| wip.yml | ||
| workflow-suggestion-agent.lock.yml | ||
| workflow-suggestion-agent.md | ||
| zipt-code-reviewer.lock.yml | ||
| zipt-code-reviewer.md | ||