python: build a PyPI-publishable Pyodide (PEP 783) wheel (#9891)

## 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>

src/api/python/pyproject.toml

@@ -1,3 +1,29 @@
 [build-system]
 requires = ["setuptools>=70"]
 build-backend = "setuptools.build_meta"
+
+# --- Pyodide / WebAssembly (PEP 783) build configuration ---------------------
+# Consumed by pyodide-build (invoked directly or via `cibuildwheel --platform
+# pyodide`). These flags are forwarded to the emscripten toolchain that compiles
+# libz3 to wasm32. setup.py's IS_PYODIDE branch appends the same -fexceptions
+# flags defensively, but declaring them here is what cibuildwheel relies on.
+# Pyodide 314 / emscripten 5 builds its main module with *native wasm*
+# exception handling and wasm longjmp (see Pyodide's Makefile.envs). Side
+# modules like libz3.so MUST match that ABI: building with the legacy
+# `-fexceptions` (JS-based EH) makes libz3 import `invoke_*` trampolines that the
+# Pyodide runtime no longer provides -> "cannot resolve symbol invoke_vi" at the
+# first Z3 call. WASM_BIGINT is required because the Z3 C API passes 64-bit ints
+# across the ctypes/JS boundary.
+[tool.pyodide.build]
+cflags = "-fwasm-exceptions -sSUPPORT_LONGJMP=wasm"
+cxxflags = "-fwasm-exceptions -sSUPPORT_LONGJMP=wasm"
+ldflags = "-fwasm-exceptions -sSUPPORT_LONGJMP=wasm -sWASM_BIGINT"
+
+# --- cibuildwheel: produce a PyPI-publishable pyemscripten wheel -------------
+[tool.cibuildwheel]
+# Pyodide 314 ships CPython 3.14; match the single ABI it targets.
+build = "cp314-*"
+
+[tool.cibuildwheel.pyodide]
+# z3test.py is the upstream smoke test; run it inside the Pyodide test venv.
+test-command = "python {project}/z3test.py z3"

src/api/python/setup.py

@@ -42,9 +42,16 @@ if RELEASE_DIR is None:
         BUILD_PLATFORM = "emscripten"
         BUILD_ARCH = "wasm32"
         BUILD_OS_VERSION = os.environ['_PYTHON_HOST_PLATFORM'].split('_')[1:-1]
-        build_env['CFLAGS'] = build_env.get('CFLAGS', '') + " -fexceptions"
-        build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + " -fexceptions"
-        build_env['LDFLAGS'] = build_env.get('LDFLAGS', '') + " -fexceptions"
+        # Match Pyodide's native-wasm exception/longjmp ABI (see Makefile.envs in
+        # Pyodide). The legacy JS-based "-fexceptions" makes libz3.so import
+        # invoke_* trampolines that the modern Pyodide runtime does not export,
+        # which surfaces as "cannot resolve symbol invoke_vi" on the first Z3
+        # call. These mirror [tool.pyodide.build] in pyproject.toml so direct
+        # `pyodide build` invocations stay consistent with cibuildwheel.
+        _wasm_eh = " -fwasm-exceptions -sSUPPORT_LONGJMP=wasm"
+        build_env['CFLAGS'] = build_env.get('CFLAGS', '') + _wasm_eh
+        build_env['CXXFLAGS'] = build_env.get('CXXFLAGS', '') + _wasm_eh
+        build_env['LDFLAGS'] = build_env.get('LDFLAGS', '') + _wasm_eh + " -sWASM_BIGINT"
         IS_SINGLE_THREADED = True
         ENABLE_LTO = False
         # build with pthread doesn't work. The WASM bindings are also single threaded.
@@ -305,6 +312,21 @@ class bdist_wheel(_bdist_wheel):
             
             
     def finalize_options(self):
+        if BUILD_PLATFORM == "emscripten":
+            # Under pyodide-build / `cibuildwheel --platform pyodide`, the
+            # authoritative wheel platform tag is handed to us verbatim via
+            # _PYTHON_HOST_PLATFORM. For PEP 783 (Pyodide >= 0.28 / "314") this
+            # is e.g. "pyemscripten_2026_0_wasm32" -- a tag PyPI accepts. The
+            # reconstruction below instead produced "emscripten_<ver>_wasm32",
+            # which is locked to a Pyodide release and rejected by PyPI, so we
+            # defer to pyodide-build's tag when it is available.
+            host_platform = os.environ.get('_PYTHON_HOST_PLATFORM')
+            if host_platform:
+                self.plat_name = host_platform
+            else:
+                os_version_tag = '_'.join(BUILD_OS_VERSION) if BUILD_OS_VERSION else 'xxxxxx'
+                self.plat_name = f"emscripten_{os_version_tag}_wasm32"
+            return super().finalize_options()
         if BUILD_ARCH is not None and BUILD_PLATFORM is not None:
             os_version_tag = '_'.join(BUILD_OS_VERSION) if BUILD_OS_VERSION is not None else 'xxxxxx'
             os_version_tag = self.remove_build_machine_os_version(BUILD_PLATFORM, os_version_tag)