diff --git a/.github/workflows/pyodide-pypi.yml b/.github/workflows/pyodide-pypi.yml new file mode 100644 index 000000000..090145a65 --- /dev/null +++ b/.github/workflows/pyodide-pypi.yml @@ -0,0 +1,57 @@ +name: Pyodide Wheel (PyPI) + +# Builds a PEP 783 `pyemscripten_*_wasm32` wheel for z3-solver using cibuildwheel +# and publishes it to PyPI on tag pushes. Unlike the legacy pyodide.yml (which +# uses `pyodide build` and produces a Pyodide-version-locked emscripten_* wheel +# uploaded only as a CI artifact), this wheel is installable at runtime with +# micropip from PyPI. See src/api/python/pyproject.toml [tool.cibuildwheel]. + +on: + release: + types: [created] + workflow_dispatch: + +permissions: + contents: read + +jobs: + build-pyodide: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v6 + + - name: Build Pyodide wheel + uses: pypa/cibuildwheel@v4.1.0 + with: + # The Python bindings live in a subdirectory of the repo. + package-dir: src/api/python + env: + CIBW_PLATFORM: pyodide + # Exception/longjmp/bigint flags are declared in + # src/api/python/pyproject.toml ([tool.pyodide.build]) and combined + # with Pyodide's -fwasm-exceptions defaults. Don't set CFLAGS/CXXFLAGS + # here — a JS-EH -fexceptions value conflicts with the wasm-EH ABI. + + - name: Store Pyodide wheel + uses: actions/upload-artifact@v7 + with: + name: pyodide-wheel + path: wheelhouse/*.whl + + publish: + name: Publish to PyPI + runs-on: ubuntu-24.04 + if: startsWith(github.ref, 'refs/tags/') + needs: [build-pyodide] + environment: release + permissions: + id-token: write # trusted publishing (OIDC), no API token needed + steps: + - name: Download Pyodide wheel + uses: actions/download-artifact@v8 + with: + name: pyodide-wheel + path: dist/ + + - name: Publish to PyPI + uses: pypa/gh-action-pypi-publish@release/v1 diff --git a/CMakeLists.txt b/CMakeLists.txt index 1ff592e0e..491cb996b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -204,7 +204,12 @@ elseif (EMSCRIPTEN) "-Os" "-s ALLOW_MEMORY_GROWTH=1" "-s ASSERTIONS=0" - "-s DISABLE_EXCEPTION_CATCHING=0" + # Use native wasm exception handling + wasm longjmp to match the ABI of the + # Pyodide / modern-emscripten main module. The legacy JS-based EH (which the + # removed "-s DISABLE_EXCEPTION_CATCHING=0" selected) makes libz3 import + # invoke_* trampolines the Pyodide runtime no longer provides. + "-fwasm-exceptions" + "-s SUPPORT_LONGJMP=wasm" "-s ERROR_ON_UNDEFINED_SYMBOLS=1" ) endif() diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index 380744c87..243a85a94 100644 --- a/src/api/python/pyproject.toml +++ b/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" diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 116b3b570..029b5ea86 100644 --- a/src/api/python/setup.py +++ b/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__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)