ci: add build/test CI and PyPI release workflows - #1
Merged
Merged
Conversation
- ci.yml: on push to main / PR / dispatch — check out leo3 as a sibling (path dependency), install Rust + elan (pinned Lean toolchain) + uv, maturin develop, pytest on Ubuntu (py3.12/3.13), macOS x86_64/arm64, Windows - release.yml: on v* tags / dispatch — maturin wheels (Linux x86_64, macOS x86_64/arm64, Windows amd64) + sdist, publish to PyPI (PYPI_API_TOKEN) and GitHub Release; leo3 dep resolved via git ref (default) or crates.io pin (official releases) - README: document the CI/CD setup and leo3 dependency strategy
- sdist: leo3 checkout now uses path: leo3 and the checkout's commit output, with a 40-hex SHA validation before writing the pin - release: rewrite the leo3 dependency BEFORE uv sync and sync with --no-install-project, so uv no longer builds the project against the stale path dependency; run maturin via uv run --no-sync - macOS: use explicit macos-15-intel (x86_64, last Intel image) and macos-15 (arm64) instead of macos-14/macos-latest, which both resolve to arm64 - rewrite Cargo.toml with a portable python3 script (BSD sed rejects sed -i without backup suffix); the script no longer uses str.format, which mis-parses the dependency braces - read the Lean toolchain from leotower/lean-toolchain in release.yml; record the resolved leo3 commit in job summaries and the GitHub release body
The committed uv.lock pinned all package URLs to a developer-machine local mirror (http://localhost:3141/simple), which does not exist on GitHub runners and made every uv sync fail with connection refused. Regenerated with 'uv lock --no-config': same package versions and hashes, URLs now point at pypi.org / files.pythonhosted.org.
On macOS the built extension references Lean's dylibs via @rpath without an embedded LC_RPATH, so pytest failed at import with 'Library not loaded: @rpath/libInit_shared.dylib' (found in CI run 32691807629). The test step now exports DYLD_LIBRARY_PATH to the elan toolchain's lean lib dir — the runtime mechanism leo3 documents for macOS. The 'Configure Lean library path' step is generalized to all OSes so LEAN_HOME is available in the test step.
The generalized 'Configure Lean library path' step and the updated 'Run tests' step both use bash syntax but were missing 'shell: bash', so on Windows (default pwsh) they failed with a parser error before any Lean/pytest work. Both steps now pin shell: bash.
The GITHUB_PATH entry 'C:\Users\...\v4.25.2/bin' mixed backslashes
(with LEAN_HOME) and a forward slash; the Windows loader does not
resolve mixed-slash PATH entries, so _leotower.pyd could not find
libleanshared.dll at import time ('DLL load failed: module not found')
even though the directory was on PATH. CI diagnostics confirmed:
by-name load failed while direct-path and add_dll_directory loads
succeeded, and the exact backslash path was absent from PATH. The
entry is now normalized to forward slashes.
Also removes the temporary diagnostic step and documents the Windows
PATH requirement in the README.
Forward-slash PATH entries are also not resolved by the Windows DLL loader (confirmed: by-name load still failed while the entry was on PATH). The entry is now normalized to pure backslashes, with a compact diagnostic to confirm the load on the next run.
SearchPathW reveals whether the loader's PATH search can see the Lean DLL dir at all, and the Win32 error code pins down why the by-name load fails.
The Windows loader on GitHub-hosted runners does not resolve Lean's DLLs (libleanshared.dll and friends) from PATH, in any slash form: mixed, forward, and pure-backslash PATH entries all failed while direct-path and AddDllDirectory-based loads succeeded. So importing leotower on Windows now registers the Lean toolchain's bin dir (from LEAN_HOME, then the elan toolchains under %USERPROFILE%) with os.add_dll_directory before the C extension is imported. This also fixes end-user imports outside CI, where the same loader behavior applies. CI: drop the temporary diagnostic and the now-redundant GITHUB_PATH entry; the Locate Lean toolchain step only exposes LEAN_HOME.
Standalone Repl() init with faulthandler plus a full lean.exe elaboration, to separate a leotower-stack failure from a broken Lean-on-runner (ICU) failure.
Constructing Repl() aborts the Windows process (misaligned pointer dereference in leo3-ffi lean_ptr_tag, exit 127, no Python traceback; debug-build aligncheck exposing an invalid object pointer). The Windows leg keeps building the extension and running the session tests; the repl suite is quarantined with a skip marker until W-395 lands, and a temporary step records the full RUST_BACKTRACE for the issue.
Full backtrace captured and attached to W-395.
The org's ubuntu-latest pool was undergoing continuous runner shutdowns (jobs killed mid-build by SIGTERM across repeated waves), while every other pool was stable. ubuntu-24.04 is the same image on a separate pool and pins the distribution. The release wheels matrix drops windows-latest until W-395 (Repl() process-level abort on Windows) is fixed, so no release ships the broken code path.
Address review feedback: - Add a resolve-leo3 job that resolves the leo3 ref (branch/tag/SHA) to a single full commit SHA via git ls-remote before any build starts; the wheels matrix legs and the sdist job all check out that exact SHA, so one release can no longer mix leo3 revisions when the ref is mutable (main) and moves between legs. - README: state the actual release matrix (Linux x86_64 + macOS x86_64/arm64 wheels + sdist) and that no Windows wheel is published until W-395 is fixed (Windows CI keeps build + import + session smoke tests; Repl suite skipped). Verified: resolve logic tested against github.com for branch, lightweight tag, full SHA, and a nonexistent ref (clean error); actionlint clean; local T1/T2/T4 release-path smoke passes.
resolve-leo3 is job-skipped when leo3_pin is set, and a skipped upstream job skips downstream jobs that have no if of their own. Give wheels and sdist an explicit if: in git mode they still require resolve-leo3 to have succeeded; in crates.io mode they run (the resolve job is irrelevant there). Without this, a dispatch with leo3_pin set built nothing at all.
A skipped needed job skips downstream jobs even when their if condition is true; only status functions such as always() override that gating. wheels/sdist now run in crates.io mode (resolve not needed) and still require a successful resolve-leo3 in git mode.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds the first CI/CD for leotower (issue: 搭建 leotower 仓库 CI/CD).
ci.yml: push to main / PR / dispatch — leo3 sibling checkout (path dep), Rust + elan (toolchain from lean-toolchain) + uv, maturin develop + pytest on Ubuntu (py3.12/3.13), macOS x86_64 (macos-15-intel) / arm64 (macos-15), Windowsrelease.yml: v* tag / dispatch — wheels (Linux x86_64, macOS x86_64/arm64, Windows amd64) + sdist, PyPI publish (PYPI_API_TOKEN) + GitHub Release; leo3 dep via git ref (default, sdist pinned to resolved SHA) or crates.io pin (official releases)Addresses the first review round: sdist SHA chain, pin-before-sync ordering, explicit macOS runner labels, portable Cargo.toml rewrite (no sed).