diff --git a/.github/workflows/sync-released.yml b/.github/workflows/sync-released.yml index 67ea627ae..b67914f3e 100644 --- a/.github/workflows/sync-released.yml +++ b/.github/workflows/sync-released.yml @@ -8,9 +8,10 @@ name: Sync released repos # to their `main`, and advances the baseline — one dispatch drives it all the way # through. The uncoordinated-commit guard skips any released repo whose `main` has # moved off the baseline, so out-of-band commits are never clobbered. Needs the -# `RELEASED_SYNC_PAT` and `RELEASED_SYNC_PAT_2` secrets (contents:write on the -# released repos; the set is split across two fine-grained tokens because one -# token caps its selected-repository list — the sync routes per repo). +# `RELEASED_SYNC_PAT` and `RELEASED_SYNC_PAT_2` secrets (Contents and Workflows: +# read/write on the released repos; Workflows is required for managed CI files. +# The set is split across two fine-grained tokens because one token caps its +# selected-repository list — the sync routes per repo). on: workflow_dispatch: diff --git a/AGENTS.md b/AGENTS.md index 030e44e46..ca2a03beb 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -44,9 +44,12 @@ near-mechanical copy): - `conformance/HexX/{Conformance,EmitFixtures}.lean` — conformance drivers (shared `conformance/` sub-project). - `conformance-fixtures/HexX/*.jsonl`, `scripts/oracle/_*.py`. +- `.github/workflows/ci.yml` — selected from the complete per-repository + workflows in `scripts/release/released-ci.yml`. The publish mechanism is `scripts/release/released.yml` (the per-repo -managed-path + pin manifest), `scripts/release/sync_released.py` (the +managed-path + pin manifest), `scripts/release/released-ci.yml` (the managed +mirror CI workflows), `scripts/release/sync_released.py` (the driver; supports `--dry-run`), `scripts/release/synced.json` (the per-repo `main` baseline this monorepo corresponds to), and `.github/workflows/sync-released.yml` (manual dispatch, dry by default). diff --git a/PLAN/Releases.md b/PLAN/Releases.md index fe37e45d4..d2b624fec 100644 --- a/PLAN/Releases.md +++ b/PLAN/Releases.md @@ -178,13 +178,20 @@ In this monorepo, all bench and conformance drivers build in the shared root Lake graph. Published mirrors use the corresponding root and sidecar skeletons documented in `scripts/release/BOOTSTRAP.md`; the sync manages source and rewrites every lockfile but deliberately leaves those Lake skeletons intact. +The mirrors' CI workflows are managed centrally in +`scripts/release/released-ci.yml` and published by the same guarded sync. ### The publish mechanism -Four pieces, under `scripts/release/` and `.github/workflows/`: +Five pieces, under `scripts/release/` and `.github/workflows/`: - `released.yml` — a per-repo manifest: which paths to copy, which oracles to ship, and which upstream repos to pin, in dependency order. +- `released-ci.yml` — the complete per-repository mirror workflows. Their + repository-specific build, conformance, oracle, and bench commands remain + explicit while cache setup and policy are uniform. The explicit cache covers + each root/sidecar build plus published Hex dependency builds, while excluding + the separately fetched Mathlib cache. - `sync_released.py` — the driver. For each repo it clones `main`, overwrites the managed paths from this tree, rewrites the cross-repo Lake revisions, and commits to `main`. `--dry-run` prints the planned @@ -212,11 +219,12 @@ routes that repository's clone and push through that token, so a new library goes on whichever token has room. Publishing one takes three steps in this order: -1. create the repository under `leanprover` and give it the un-managed Lake - and CI skeleton (`scripts/release/BOOTSTRAP.md`); the sync clones but never - creates; +1. create the repository under `leanprover`, give it the un-managed Lake + skeleton, and add its managed CI workflow in hex-dev + (`scripts/release/BOOTSTRAP.md`); the sync clones but never creates; 2. add that repository to the selected repositories of a token with room, - with `Contents: Read and write`, and have an organization owner approve + with `Contents: Read and write` and `Workflows: Read and write`, and have an + organization owner approve the request at https://github.com/organizations/leanprover/settings/personal-access-token-requests; find the current tokens under @@ -249,14 +257,13 @@ the push returns `403 Permission to leanprover/.git denied`. before the first push and refuses to start, naming the repositories no token covers. A dry run does not preflight, using no token and pushing nothing. -**What the preflight does not prove.** It checks that each repository is in -some token's selection, and nothing stronger. `GET /repos` needs only -`Metadata: read`, and the `permissions` it returns describe the authenticated -user's role rather than that token's grants, so a token holding only -`Contents: read` on a selected repository still looks fine to it. Nor does it -know whether branch protection or a ruleset on a mirror's `main` would reject -the push. Those failures still surface only at push time; the invariant the -mirrors rely on is that `main` takes direct pushes from the release actor. +**What the preflight does not prove.** Its receive-pack probe verifies that a +token can push ordinary content to the selected repository. GitHub checks the +separate `Workflows: write` permission only when a push changes a workflow, so +that grant still has to be configured on every publishing token. Nor does the +probe know whether branch protection or a ruleset on a mirror's `main` would +reject the push. Those failures still surface only at push time; the invariant +the mirrors rely on is that `main` takes direct pushes from the release actor. ### Baseline and the uncoordinated-commit guard diff --git a/scripts/release/BOOTSTRAP.md b/scripts/release/BOOTSTRAP.md index 96c0f2828..aab940459 100644 --- a/scripts/release/BOOTSTRAP.md +++ b/scripts/release/BOOTSTRAP.md @@ -1,11 +1,11 @@ # Bootstrapping released repositories `scripts/release/released.yml` is the authoritative publication graph for the -35 split repositories and the `leanprover/hex` aggregate. The sync workflow -clones each repository's `main`, overwrites its managed paths from this -monorepo, copies the release toolchain, synchronizes external dependency locks, -rewrites every published Hex revision, and pushes the result. It does not -create repositories or author the remaining Lake and CI skeleton. +split repositories and the `leanprover/hex` aggregate. The sync workflow +clones each repository's `main`, overwrites its managed paths and CI workflow +from this monorepo, copies the release toolchain, synchronizes external +dependency locks, rewrites every published Hex revision, and pushes the result. +It does not create repositories or author the remaining Lake skeleton. The manifest is checked locally by: @@ -60,7 +60,8 @@ on the closest already released package. The initial `main` must contain: manifest, with only direct `require`s and the library's declared build targets; - `lake-manifest.json` generated by Lake, not assembled by hand; -- `LICENSE`, `AGENTS.md`, `.gitignore`, and the standard single-job CI files; +- `LICENSE`, `AGENTS.md`, and `.gitignore`; the first sync publishes the + repository's workflow from `scripts/release/released-ci.yml`; - root and sidecar Lake projects for each enabled `bench` or `conformance` directory; and - a non-public regression-test `lean_lib` containing every module named by the @@ -74,12 +75,15 @@ on the closest already released package. The initial `main` must contain: root module. Publication validates these declarations in the unmanaged Lake skeleton before -copying source. A stale target name therefore stops the sync before it can -partially update that repository. +copying source. It also validates that every `scripts/ci` helper named by the +managed workflow exists in the mirror. A stale target or missing helper +therefore stops the sync before it can partially update that repository. Source, the umbrella module, README, SPEC, benchmarks, conformance drivers, -fixtures, and oracle helpers are managed by the sync when listed in the -manifest. Do not duplicate or hand-edit those files in a released mirror. +fixtures, oracle helpers, and `.github/workflows/ci.yml` are managed by the +sync. Do not duplicate or hand-edit those files in a released mirror. Add a +new repository's complete workflow to `scripts/release/released-ci.yml`; the +manifest checker rejects missing and extra workflow entries. `require`s list direct dependencies only; Lake resolves the rest transitively. The longer `pins` list in `released.yml` is deliberate: the sync rewrites the @@ -112,7 +116,11 @@ Do not add placeholder entries to `scripts/release/synced.json`. An absent baseline is how the first publish is distinguished; any truthy, incorrect SHA causes the uncoordinated-commit guard to skip the repository. -After every skeleton exists on `main`: +After every skeleton exists on `main`, ensure the fine-grained tokens behind +`RELEASED_SYNC_PAT` and +`RELEASED_SYNC_PAT_2` select every target repository and grant both +`Contents: Read and write` and `Workflows: Read and write`; the latter is +required because the sync publishes `.github/workflows/ci.yml`. Then: 1. Run the local manifest check and the complete monorepo build. 2. Dispatch `.github/workflows/sync-released.yml` with `dry_run=true`. diff --git a/scripts/release/check_released_manifest.py b/scripts/release/check_released_manifest.py index 1f5136b5e..37368ec8c 100644 --- a/scripts/release/check_released_manifest.py +++ b/scripts/release/check_released_manifest.py @@ -16,7 +16,12 @@ sys.path.insert(0, str(REPO_ROOT / "scripts")) from libgraph import load_libraries, reachable_dependencies # noqa: E402 -from release.sync_released import MANIFEST, managed_paths, removal_paths # noqa: E402 +from release.sync_released import ( # noqa: E402 + MANIFEST, + managed_paths, + released_ci_workflows, + removal_paths, +) from release import aggregate_readme # noqa: E402 @@ -146,6 +151,147 @@ def release_executables() -> dict[str, str]: return out +def check_ci_workflows(entries: list[dict]) -> None: + """Require one complete, cache-safe managed workflow per released repo.""" + workflows = released_ci_workflows() + expected = {entry["repo"].split("/", 1)[1] for entry in entries} + actual = set(workflows) + if actual != expected: + fail( + "released-ci.yml differs from the release manifest; " + f"missing={sorted(expected - actual)}, extra={sorted(actual - expected)}" + ) + for entry in entries: + short = entry["repo"].split("/", 1)[1] + workflow = workflows[short] + try: + parsed = yaml.load(workflow, Loader=yaml.BaseLoader) + except yaml.YAMLError as exc: + fail(f"{entry['repo']}: managed CI is invalid YAML: {exc}") + triggers = parsed.get("on") if isinstance(parsed, dict) else None + push = triggers.get("push") if isinstance(triggers, dict) else None + if ( + not isinstance(push, dict) + or push.get("branches") != ["main"] + or "pull_request" not in triggers + ): + fail( + f"{entry['repo']}: managed CI must run on main pushes and " + "pull requests" + ) + concurrency = parsed.get("concurrency") if isinstance(parsed, dict) else None + if ( + not isinstance(concurrency, dict) + or concurrency.get("group") != "${{ github.workflow }}-${{ github.ref }}" + or concurrency.get("cancel-in-progress") + != "${{ github.ref != 'refs/heads/main' }}" + ): + fail( + f"{entry['repo']}: managed CI must preserve main runs so their " + "terminal cache save can finish" + ) + jobs = parsed.get("jobs") if isinstance(parsed, dict) else None + if not isinstance(jobs, dict) or not jobs: + fail(f"{entry['repo']}: managed CI must define jobs") + for job_name, job in jobs.items(): + if not isinstance(job, dict) or "strategy" in job: + fail(f"{entry['repo']}: CI job {job_name} must not use a matrix") + steps = job.get("steps") if isinstance(job, dict) else None + if not isinstance(steps, list): + fail(f"{entry['repo']}: CI job {job_name} has no steps") + indexed = { + action: [ + index for index, step in enumerate(steps) + if isinstance(step, dict) and step.get("uses") == action + ] + for action in ( + "leanprover/lean-action@v1", + "actions/cache/restore@v4", + "actions/cache/save@v4", + ) + } + if any(len(indices) != 1 for indices in indexed.values()): + fail( + f"{entry['repo']}: CI job {job_name} must contain one " + "lean-action, cache restore, and cache save" + ) + lean_index = indexed["leanprover/lean-action@v1"][0] + restore_index = indexed["actions/cache/restore@v4"][0] + save_index = indexed["actions/cache/save@v4"][0] + if not (lean_index < restore_index < save_index == len(steps) - 1): + fail( + f"{entry['repo']}: CI job {job_name} must restore after " + "setup and save only after every verification step" + ) + lean_inputs = steps[lean_index].get("with", {}) + if lean_inputs.get("use-github-cache") != "false": + fail(f"{entry['repo']}: lean-action GitHub cache must be disabled") + if lean_inputs.get("use-mathlib-cache") != "false": + fail(f"{entry['repo']}: lean-action Mathlib cache must be disabled") + restore_inputs = steps[restore_index].get("with", {}) + save_inputs = steps[save_index].get("with", {}) + required_paths = { + ".lake/build", + ".lake/packages/Hex*/.lake/build", + ".lake/packages/hex-test-kit/.lake/build", + } + if job_name == "build" and entry.get("bench"): + required_paths |= { + "bench/.lake/build", + "bench/.lake/packages/Hex*/.lake/build", + "bench/.lake/packages/hex-test-kit/.lake/build", + } + if job_name == "build" and entry.get("conformance"): + required_paths |= { + "conformance/.lake/build", + "conformance/.lake/packages/Hex*/.lake/build", + "conformance/.lake/packages/hex-test-kit/.lake/build", + } + cached_paths = { + path.strip() + for path in restore_inputs.get("path", "").splitlines() + if path.strip() + } + saved_paths = { + path.strip() + for path in save_inputs.get("path", "").splitlines() + if path.strip() + } + if cached_paths != required_paths: + fail( + f"{entry['repo']}: CI job {job_name} cache paths differ; " + f"missing={sorted(required_paths - cached_paths)}, " + f"extra={sorted(cached_paths - required_paths)}" + ) + key = restore_inputs.get("key", "") + restore_prefixes = [ + prefix.strip() + for prefix in restore_inputs.get("restore-keys", "").splitlines() + if prefix.strip() + ] + if ( + key != save_inputs.get("key") + or saved_paths != cached_paths + or len(restore_prefixes) != 1 + or key + != restore_prefixes[0] + + "${{ github.run_id }}-${{ github.run_attempt }}" + or "${{ runner.os }}-${{ runner.arch }}" not in key + or "${{ hashFiles(" not in key + ): + fail( + f"{entry['repo']}: CI job {job_name} cache must use a " + "run-unique save key and stable restore prefix" + ) + save_condition = steps[save_index].get("if", "") + if ( + "github.event_name == 'push'" not in save_condition + or "github.ref == 'refs/heads/main'" not in save_condition + ): + fail( + f"{entry['repo']}: CI job {job_name} must save only from main" + ) + def main() -> int: document = yaml.safe_load(MANIFEST.read_text(encoding="utf-8")) entries = document.get("repos") if isinstance(document, dict) else None @@ -296,6 +442,8 @@ def main() -> int: seen_repos.add(short) + check_ci_workflows(entries) + if len(aggregate_entries) != 1: fail(f"released.yml must contain exactly one pins_only aggregate; found {len(aggregate_entries)}") aggregate = aggregate_entries[0] @@ -448,7 +596,7 @@ def main() -> int: print( f"release manifest: {len(entries) - 1} split repositories + " - f"1 aggregate; paths, pins, test targets, and topological constraints valid" + f"1 aggregate; paths, CI, pins, test targets, and topological constraints valid" ) return 0 diff --git a/scripts/release/released-ci.yml b/scripts/release/released-ci.yml new file mode 100644 index 000000000..ea8f34f86 --- /dev/null +++ b/scripts/release/released-ci.yml @@ -0,0 +1,2966 @@ +# Centrally managed released-mirror CI workflows. +# +# Each value is the complete .github/workflows/ci.yml published to the named +# repository by sync_released.py. Keep repository-specific build, conformance, +# oracle, and benchmark commands here; the sync's divergence guard protects this +# artifact exactly like every other managed path. +workflows: + hex-basic: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library + run: lake build + - name: Assert Mathlib-free + run: | + if find . -type d -name mathlib | grep -q .; then + echo "ERROR: a package pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexBasic 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-test-kit: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build + run: lake build + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-arith: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexArith + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexarith_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexarith_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexArith conformance/HexArith bench/HexArith 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-poly: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Install FLINT oracle dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + python3 -m pip install --user python-flint + - name: Build library + run: lake build + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + cd conformance + lake exe hexpoly_emit_fixtures > /tmp/hex-poly-fresh.jsonl + cd .. + diff -u conformance-fixtures/HexPoly/poly.jsonl /tmp/hex-poly-fresh.jsonl + python3 scripts/oracle/poly_flint.py < /tmp/hex-poly-fresh.jsonl + - name: Build + full bench verify + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + HEX_FLINT_BENCH_DRIVER: ${{ github.workspace }}/scripts/oracle/flint_bench_driver.py + HEX_FLINT_BENCH_PYTHON: python3 + run: | + cd bench + lake build hexpoly_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexpoly_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexPoly conformance/HexPoly bench/HexPoly 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-mv-poly: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Install SymPy oracle + run: python3 -m pip install --user sympy + - name: Build library and release regressions + run: lake build HexMvPoly HexMvPolyTests + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + cd conformance + lake exe hexmvpoly_emit_fixtures > /tmp/hex-mv-poly-fresh.jsonl + cd .. + diff -u conformance-fixtures/HexMvPoly/mvpoly.jsonl /tmp/hex-mv-poly-fresh.jsonl + python3 scripts/oracle/mvpoly_sympy.py < /tmp/hex-mv-poly-fresh.jsonl + - name: Build + full bench verify + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexmvpoly_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexmvpoly_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexMvPoly conformance/HexMvPoly bench/HexMvPoly 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-mod-arith: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexModArith + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexmodarith_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexmodarith_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexModArith conformance/HexModArith bench/HexModArith 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-poly-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build bridge (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexPolyMathlib 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-mv-poly-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build bridge (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexMvPolyMathlib 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Fetch Mathlib cache for correspondence conformance + run: | + cd conformance + lake exe cache get + - name: Build correspondence conformance + run: | + cd conformance + set -o pipefail + lake build HexMvPolyMathlibConformance 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-poly-fp: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexPolyFp + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexpolyfp_emit_fixtures) > /tmp/hex-poly-fp-fresh.jsonl + diff -u conformance-fixtures/HexPolyFp/poly.jsonl /tmp/hex-poly-fp-fresh.jsonl + python3 scripts/oracle/polyfp_flint.py < /tmp/hex-poly-fp-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexpolyfp_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexpolyfp_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexPolyFp conformance/HexPolyFp bench/HexPolyFp 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-sparse-poly: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Install SymPy oracle + run: python3 -m pip install --user sympy + - name: Build library and release regressions + run: lake build HexSparsePoly HexSparsePolyTests + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + cd conformance + lake exe hexsparsepoly_emit_fixtures > /tmp/hex-sparse-poly-fresh.jsonl + cd .. + diff -u conformance-fixtures/HexSparsePoly/sparsepoly.jsonl /tmp/hex-sparse-poly-fresh.jsonl + python3 scripts/oracle/sparsepoly_sympy.py /tmp/hex-sparse-poly-fresh.jsonl + - name: Build + full bench verify + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexsparsepoly_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexsparsepoly_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexSparsePoly conformance/HexSparsePoly bench/HexSparsePoly 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-sparse-poly-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build correspondence layer (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexSparsePolyMathlib HexSparsePolyMathlibTests 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Fetch Mathlib cache for correspondence conformance + run: | + cd conformance + lake exe cache get + - name: Build correspondence conformance + run: | + cd conformance + set -o pipefail + lake build HexSparsePolyMathlibConformance 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-poly-z: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexPolyZ + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexpolyz_emit_fixtures) > /tmp/hex-poly-z-fresh.jsonl + diff -u conformance-fixtures/HexPolyZ/polyz.jsonl /tmp/hex-poly-z-fresh.jsonl + python3 scripts/oracle/polyz_flint.py < /tmp/hex-poly-z-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexpolyz_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexpolyz_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexPolyZ conformance/HexPolyZ bench/HexPolyZ 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-mod-arith-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexModArithMathlib + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-poly-fp-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexPolyFpMathlib + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-gfq-ring: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexGFqRing + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexgfqring_emit_fixtures) > /tmp/hex-gfq-ring-fresh.jsonl + diff -u conformance-fixtures/HexGFqRing/gfqring.jsonl /tmp/hex-gfq-ring-fresh.jsonl + python3 scripts/oracle/gfqring_flint.py < /tmp/hex-gfq-ring-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexgfqring_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexgfqring_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexGFqRing conformance/HexGFqRing bench/HexGFqRing 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-hensel: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - name: Install oracle dependencies + run: python3 -m pip install --user cypari2 python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexHensel + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexhensel_emit_fixtures) > /tmp/hex-hensel-fresh.jsonl + diff -u conformance-fixtures/HexHensel/hensel.jsonl /tmp/hex-hensel-fresh.jsonl + python3 scripts/oracle/hensel_pari.py < /tmp/hex-hensel-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexhensel_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexhensel_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexHensel conformance/HexHensel bench/HexHensel 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-poly-z-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexPolyZMathlib + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-hensel-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexHenselMathlib + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-roots: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexRoots + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexroots_emit_fixtures) > /tmp/hexroots-fresh.jsonl + diff -u conformance-fixtures/HexRoots/roots.jsonl /tmp/hexroots-fresh.jsonl + python3 scripts/oracle/roots_flint.py < /tmp/hexroots-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexroots_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexroots_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexRoots conformance/HexRoots bench/HexRoots 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-real-roots: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexRealRoots HexRealRootsTests + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexrealroots_emit_fixtures) > /tmp/hexrealroots-fresh.jsonl + diff -u conformance-fixtures/HexRealRoots/realroots.jsonl /tmp/hexrealroots-fresh.jsonl + python3 scripts/oracle/realroots_flint.py < /tmp/hexrealroots-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexrealroots_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexrealroots_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexRealRoots conformance/HexRealRoots bench/HexRealRoots 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-roots-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexRootsMathlib HexRootsMathlibTests + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-real-roots-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexRealRootsMathlib HexRealRootsMathlibTests + - name: Build conformance sidecar + run: | + cd conformance + lake exe cache get + lake build + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-matrix: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Install FLINT oracle dependencies + run: sudo apt-get update && sudo apt-get install -y libgmp-dev + - name: Install python-flint + run: python3 -m pip install --user python-flint + - name: Build library + run: lake build + - name: Build conformance sidecar + run: | + cd conformance + lake build + cd .. + - name: Conformance oracle (python-flint cross-check) + run: bash scripts/ci/run_oracles.sh + - name: Build + full bench verify (FLINT comparator) + env: + # Hard cap per SPEC/benchmarking.md §CI integration "Time + # budget". The bench verifies the fixed FLINT comparator + # rungs (runFlintBareissDet*), spawning the persistent + # python-flint driver once per run. + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + HEX_FLINT_BENCH_DRIVER: ${{ github.workspace }}/scripts/oracle/flint_bench_driver.py + HEX_FLINT_BENCH_PYTHON: python3 + run: | + cd bench + lake build hexmatrix_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexmatrix_bench + - name: Assert Mathlib-free + run: | + if find . -type d -name mathlib | grep -q .; then + echo "ERROR: a package pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexMatrix conformance bench 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-row-reduce: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Install oracle dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + python3 -m pip install --user python-flint + - name: Build library + run: lake build + - name: Build conformance + run: cd conformance && lake build + - name: FLINT conformance oracle + run: bash scripts/ci/run_oracles.sh + - name: Assert Mathlib-free + run: | + if find . -type d -name mathlib | grep -q .; then + echo "ERROR: a package pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexRowReduce conformance 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-berlekamp: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexBerlekamp HexBerlekampTests + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexberlekamp_emit_fixtures) > /tmp/hex-berlekamp-fresh.jsonl + diff -u conformance-fixtures/HexBerlekamp/berlekamp.jsonl /tmp/hex-berlekamp-fresh.jsonl + python3 scripts/oracle/berlekamp_flint.py < /tmp/hex-berlekamp-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexberlekamp_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexberlekamp_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexBerlekamp conformance/HexBerlekamp bench/HexBerlekamp 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-conway: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + - name: Install oracle dependencies + run: python3 -m pip install --user conway-polynomials + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexConway + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexconway_emit_fixtures) > /tmp/hex-conway-fresh.jsonl + diff -u conformance-fixtures/HexConway/conway.jsonl /tmp/hex-conway-fresh.jsonl + python3 scripts/oracle/conway_luebeck.py --require-conway-polynomials < /tmp/hex-conway-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexconway_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexconway_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexConway conformance/HexConway bench/HexConway 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-gfq-field: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexGFqField + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexgfqfield_emit_fixtures) > /tmp/hex-gfq-field-fresh.jsonl + diff -u conformance-fixtures/HexGFqField/gfqfield.jsonl /tmp/hex-gfq-field-fresh.jsonl + python3 scripts/oracle/gfqfield_flint.py < /tmp/hex-gfq-field-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexgfqfield_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexgfqfield_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexGFqField conformance/HexGFqField bench/HexGFqField 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-gf2: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libntl-dev pkg-config + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + # The Lake target compiles clmul.c with `-O3` only, so an ordinary build + # exercises the portable fallback and never the intrinsic. Compile the + # self-test on both paths before anything else. + - name: Cross-check every compiled clmul path (SPEC/hex-gf2.md) + run: bash scripts/ci/check_clmul_paths.sh + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexGF2 + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexgf2_emit_fixtures) > /tmp/hex-gf2-fresh.jsonl + diff -u conformance-fixtures/HexGF2/gf2.jsonl /tmp/hex-gf2-fresh.jsonl + python3 scripts/oracle/gf2_flint.py < /tmp/hex-gf2-fresh.jsonl + # `HexGF2/Bench.lean` resolves the informational NTL comparator by + # running `scripts/oracle/setup_gf2_ntl_driver.sh` relative to its own + # working directory. The bench sidecar runs from `bench/`, so build the + # driver here from the repository root and pass its path explicitly. + - name: Build the NTL bench comparator driver + run: | + echo "HEX_GF2_NTL_DRIVER=$(bash scripts/oracle/setup_gf2_ntl_driver.sh)" \ + >> "$GITHUB_ENV" + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexgf2_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexgf2_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexGF2 conformance/HexGF2 bench/HexGF2 bench/HexGF2ReleasedBench.lean 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-gf2-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexGF2Mathlib + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-gfq: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexGFq + # `HexGFqConformanceSupport` carries the conformance drivers themselves + # (see the root lakefile); the sub-project carries the emit executable, + # which is the only part needing `hex-test-kit`. + - name: Build conformance sidecar + run: | + lake build HexGFqConformanceSupport + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexgfq_emit_fixtures) > /tmp/hex-gfq-fresh.jsonl + diff -u conformance-fixtures/HexGFq/gfq.jsonl /tmp/hex-gfq-fresh.jsonl + python3 scripts/oracle/gfq_flint.py < /tmp/hex-gfq-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexgfq_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexgfq_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexGFq conformance/HexGFq bench/HexGFq 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-gfq-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexGFqMathlib + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-determinant: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + env: + BENCH_VERIFY_HARD_CAP_SECONDS: 360 + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Install oracle dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + python3 -m pip install --user python-flint + - name: Build library + run: lake build + - name: Build conformance + run: cd conformance && lake build + - name: FLINT conformance oracle + run: bash scripts/ci/run_oracles.sh + - name: Build + verify bench + run: | + cd bench + lake build hexdeterminant_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexdeterminant_bench + - name: Assert Mathlib-free + run: | + if find . -type d -name mathlib | grep -q .; then + echo "ERROR: a package pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexDeterminant conformance bench 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-bareiss: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Install oracle dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + python3 -m pip install --user python-flint + - name: Build library + run: lake build + - name: Build conformance + run: cd conformance && lake build + - name: FLINT conformance oracle + run: bash scripts/ci/run_oracles.sh + - name: Build bench (build-only; the FLINT comparator ladder is heavy) + run: cd bench && lake build hexbareiss_bench + - name: Assert Mathlib-free + run: | + if find . -type d -name mathlib | grep -q .; then + echo "ERROR: a package pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexBareiss conformance bench 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-matrix-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build bridge (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexMatrixMathlib 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-row-reduce-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build bridge (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexRowReduceMathlib 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-determinant-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build bridge (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexDeterminantMathlib 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-bareiss-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build bridge (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexBareissMathlib 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-berlekamp-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexBerlekampMathlib HexBerlekampMathlibTests + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-gram-schmidt: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + env: + BENCH_VERIFY_HARD_CAP_SECONDS: 360 + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Install oracle dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev + python3 -m pip install --user python-flint + - name: Build library + run: lake build + - name: Build conformance + run: | + cd conformance + lake build + cd .. + - name: FLINT conformance oracle + run: bash scripts/ci/run_oracles.sh + - name: Build + verify bench + run: | + cd bench + lake build hexgramschmidt_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexgramschmidt_bench + - name: Assert Mathlib-free + run: | + if find . -type d -name mathlib | grep -q .; then + echo "ERROR: a package pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexGramSchmidt conformance bench 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-gram-schmidt-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build bridge (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexGramSchmidtMathlib 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-lll: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + - name: Install oracle + comparator system dependencies + run: | + sudo apt-get update + sudo apt-get install -y \ + libgmp-dev libfplll-dev fplll-tools libntl-dev libmpfr-dev \ + libc++-dev libc++abi-dev autoconf automake libtool pkg-config curl + - name: Install Python oracle dependencies (fpylll conformance + FLINT HNF) + run: python3 -m pip install --user cysignals fpylll python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library + run: lake build + - name: Configure Lean shared library path + # The fplll-ffi shim (`scripts/oracle/setup_fplll_ffi.sh`) re-links + # against the toolchain's libleanshared and bakes an rpath, but the + # bench process still benefits from the toolchain's lib/lean dir being + # on LD_LIBRARY_PATH so the dlopened shim can resolve libLake_shared.so. + run: | + toolchain="$(sed 's|/|--|; s|:|---|' lean-toolchain)" + echo "LD_LIBRARY_PATH=$HOME/.elan/toolchains/$toolchain/lib/lean:${LD_LIBRARY_PATH:-}" \ + >> "$GITHUB_ENV" + - name: Build external-reduction check + run: lake build hexlll_external_reduction + - name: External reduction (absent + explicit load present) + run: | + .lake/build/bin/hexlll_external_reduction absent + cc -shared -fPIC scripts/ci/hexlll_probe_provider.c -o .lake/build/hexlll_probe_provider.so + .lake/build/bin/hexlll_external_reduction present \ + "$PWD/.lake/build/hexlll_probe_provider.so" + - name: Build conformance + run: | + cd conformance + lake build + - name: Conformance oracle (fpylll cross-check) + run: bash scripts/ci/run_oracles.sh + - name: Build bench executable + run: | + cd bench + lake build hexlll_bench + - name: Bench verify (fpLLL + Isabelle comparators) + env: + # Hard cap per SPEC/benchmarking.md §CI integration "Time budget". + # The hexlll bench's verify path runs the comparator smoke rungs + # (fpLLL via fplll-ffi, verified + certified Isabelle); 360 s leaves + # a variance buffer over those fixed rungs. + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + # verified + certified Isabelle LLL drivers (Zenodo 2636367, patched + # for the persistent stdin protocol). + HEX_LLL_ISABELLE_SVP="$(scripts/oracle/setup_lll_isabelle.sh)" + export HEX_LLL_ISABELLE_SVP + HEX_LLL_ISABELLE_CERTIFIED_SVP="$(scripts/oracle/setup_lll_isabelle.sh certified)" + export HEX_LLL_ISABELLE_CERTIFIED_SVP + # fpLLL comparator: build the fplll-ffi shim and dlopen it at + # hexlll_bench start-up. The shim resolves libLake_shared.so via the + # LD_LIBRARY_PATH configured above. + HEX_FPLLL_FFI_LIB="$(scripts/oracle/setup_fplll_ffi.sh)" + export HEX_FPLLL_FFI_LIB + cd bench + bash ../scripts/ci/check_bench_verify_budget.sh hexlll_bench + - name: Assert Mathlib-free + run: | + # Restrict to source trees; oracle caches (.cache/oracles), pip's + # --user site-packages, and Isabelle/fplll build dirs are not part of + # this repo's Lean dependency graph and must not trip the assertion. + if find HexLLL conformance/HexLLL bench/HexLLL -type d -name mathlib | grep -q .; then + echo "ERROR: a package pulled in Mathlib"; exit 1; fi + if find .lake bench/.lake conformance/.lake -type d -name 'Mathlib' 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexLLL conformance/HexLLL bench/HexLLL 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + # macOS job exists solely for the FFI dyld symbol-resolution cross-check + # (the LLL external-reduction check); per SPEC/CI.md this is the one justified second runner. + build-macos: + runs-on: macos-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build external-reduction check + run: lake build hexlll_external_reduction + - name: External reduction (absent + explicit load present) + run: | + .lake/build/bin/hexlll_external_reduction absent + cc -shared -fPIC scripts/ci/hexlll_probe_provider.c -o .lake/build/hexlll_probe_provider.dylib + .lake/build/bin/hexlll_external_reduction present \ + "$PWD/.lake/build/hexlll_probe_provider.dylib" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-berlekamp-zassenhaus: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y libgmp-dev libpari-dev pari-gp + - name: Install oracle dependencies + run: python3 -m pip install --user python-flint + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Build library and release regressions + run: lake build HexBerlekampZassenhaus HexBerlekampZassenhausModules HexBerlekampZassenhausTests + - name: Build conformance sidecar + run: | + cd conformance + lake build + - name: Conformance oracle + run: | + (cd conformance && lake exe hexbz_emit_fixtures) > /tmp/hex-berlekamp-zassenhaus-fresh.jsonl + diff -u conformance-fixtures/HexBerlekampZassenhaus/bz.jsonl /tmp/hex-berlekamp-zassenhaus-fresh.jsonl + python3 scripts/oracle/bz_flint.py < /tmp/hex-berlekamp-zassenhaus-fresh.jsonl + - name: Build and verify benchmarks + env: + BENCH_VERIFY_HARD_CAP_SECONDS: "360" + run: | + cd bench + lake build hexbz_bench + bash ../scripts/ci/check_bench_verify_budget.sh hexbz_bench + - name: Assert Mathlib-free + run: | + if find .lake bench/.lake conformance/.lake -type d -name Mathlib 2>/dev/null | grep -q .; then + echo "ERROR: a Lake build pulled in Mathlib"; exit 1; fi + if grep -rqE '^import Mathlib' HexBerlekampZassenhaus conformance/HexBerlekampZassenhaus bench/HexBerlekampZassenhaus 2>/dev/null; then + echo "ERROR: a source file imports Mathlib"; exit 1; fi + echo "Mathlib-free OK" + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + bench/.lake/build + bench/.lake/packages/Hex*/.lake/build + bench/.lake/packages/hex-test-kit/.lake/build + conformance/.lake/build + conformance/.lake/packages/Hex*/.lake/build + conformance/.lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-lll-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build bridge (Mathlib must come from cache, never rebuild) + run: | + set -o pipefail + lake build HexLLLMathlib 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex-berlekamp-zassenhaus-mathlib: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build library and release regressions + run: lake build HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibModules HexBerlekampZassenhausMathlibTests + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + hex: | + name: CI + on: + push: + branches: [main] + pull_request: + concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} + jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + auto-config: false + build: false + use-github-cache: false + use-mathlib-cache: false + - name: Restore Lake build outputs + uses: actions/cache/restore@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} + restore-keys: | + lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}- + - name: Fetch Mathlib cache + run: lake exe cache get + - name: Build all released libraries (Mathlib from cache) + run: | + set -o pipefail + lake build 2>&1 | tee build.log + if grep -qE 'Building Mathlib\b' build.log; then + echo "ERROR: Mathlib rebuilt from source (cache miss)"; exit 1; fi + - name: Save Lake build outputs + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && success() + uses: actions/cache/save@v4 + with: + path: | + .lake/build + .lake/packages/Hex*/.lake/build + .lake/packages/hex-test-kit/.lake/build + key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'bench/lean-toolchain', 'bench/lake-manifest.json', 'conformance/lean-toolchain', 'conformance/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }} diff --git a/scripts/release/released.yml b/scripts/release/released.yml index 45ee05fd8..443c07ef3 100644 --- a/scripts/release/released.yml +++ b/scripts/release/released.yml @@ -30,6 +30,10 @@ # conformance// (if conformance) -> conformance// # conformance-fixtures// -> conformance-fixtures// # scripts/oracle/ -> scripts/oracle/ +# scripts/release/released-ci.yml[] -> .github/workflows/ci.yml +# The CI workflow is generated for every entry, including `pins_only`; its +# per-repository build commands remain in released-ci.yml while the driver +# applies the same divergence guard as every other managed path. # `test_modules` lists verification-only modules copied with the source but # intentionally absent from the public umbrella; released CI builds them via a # non-public `lean_lib` target. diff --git a/scripts/release/sync_released.py b/scripts/release/sync_released.py index 10f3dd80c..87c48903b 100755 --- a/scripts/release/sync_released.py +++ b/scripts/release/sync_released.py @@ -3,17 +3,17 @@ For each repo in scripts/release/released.yml (topological order), this: 1. clones the repo's `main`, - 2. overwrites its *managed* paths from this monorepo, + 2. overwrites its *managed* paths and centrally owned CI workflow, 3. for managed-source repos, enables native Verso docstrings, 4. copies the stable Lean toolchain and exact external dependency pins, 5. rewrites cross-repo Hex pins in the repo's Lake files, 6. commits `chore: sync from hex-dev@` and pushes to `main` (unless --dry-run, which prints the planned changes and pin rewrites). -A `pins_only` entry (the `leanprover/hex` aggregate) skips steps 2-3 entirely: it -manages no library source from the monorepo, so the sync only re-pins it (steps -4-5) to the SHAs published this run. Listed last, after its upstreams, so its -pins resolve to the freshly-pushed commits. Its one managed artifact is the +A `pins_only` entry (the `leanprover/hex` aggregate) receives the managed CI +workflow but no library source or Verso rewrite from the monorepo. The sync +re-pins it to the SHAs published this run. Listed last, after its upstreams, its +pins resolve to the freshly-pushed commits. Its other managed artifact is the README, rendered by `aggregate_readme.py` from a template plus the manifest's `component:` labels so the published library table cannot fall behind. @@ -23,7 +23,10 @@ token caps its selected-repository list, so the published set is split across more than one token; for each target repository the preflight probes the tokens in order until one can push to it, and routes that repository's clone and -push through that token. Dry-run clones over public https and never pushes. +push through that token. Because the sync updates `.github/workflows/ci.yml`, +each token also needs Workflows: read and write. The receive-pack preflight can +verify Contents permission but not this separate workflow-file permission. +Dry-run clones over public https and never pushes. Usage: python3 scripts/release/sync_released.py --dry-run @@ -55,6 +58,7 @@ REPO_ROOT = Path(__file__).resolve().parents[2] MANIFEST = REPO_ROOT / "scripts" / "release" / "released.yml" +RELEASED_CI = REPO_ROOT / "scripts" / "release" / "released-ci.yml" BASELINE = REPO_ROOT / "scripts" / "release" / "synced.json" TOOLCHAIN = REPO_ROOT / "lean-toolchain" # The `RELEASED_SYNC_PAT` / `RELEASED_SYNC_PAT_2` secrets hold the @@ -71,7 +75,8 @@ "Follow the per-token reasons above: a repository reported without a\n" "write grant must be added to the selected repositories of one of the\n" "tokens behind the\n" - "RELEASED_SYNC_PAT / RELEASED_SYNC_PAT_2 secrets (Contents: Read and write);\n" + "RELEASED_SYNC_PAT / RELEASED_SYNC_PAT_2 secrets (Contents: Read and write;\n" + "Workflows: Read and write);\n" "a missing repository must be created first; an indeterminate reason (rate\n" "limit, network, credentials) calls for a retry or a token repair, not a\n" "selection change. The tokens are currently `hex-publishing` and\n" @@ -114,14 +119,42 @@ def copy_file(src: Path, dest: Path) -> None: shutil.copy2(src, dest) +def released_ci_workflows(path: Path | None = None) -> dict[str, str]: + """Load the complete managed CI workflow for every released repository.""" + source = path or RELEASED_CI + document = yaml.safe_load(source.read_text(encoding="utf-8")) + workflows = document.get("workflows") if isinstance(document, dict) else None + if not isinstance(workflows, dict) or not workflows: + raise ValueError(f"{source}: workflows must be a non-empty mapping") + for repo, workflow in workflows.items(): + if not isinstance(repo, str) or not isinstance(workflow, str): + raise ValueError(f"{source}: workflow entries must map names to text") + if not workflow.endswith("\n"): + raise ValueError(f"{source}: workflow for {repo} must end in a newline") + return workflows + + +def apply_ci_workflow(entry: dict, clone: Path) -> str: + """Publish the selected central workflow into a released clone.""" + short = entry["repo"].split("/")[-1] + workflows = released_ci_workflows() + if short not in workflows: + raise RuntimeError(f"no managed CI workflow for {entry['repo']}") + destination = clone / ".github" / "workflows" / "ci.yml" + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_text(workflows[short], encoding="utf-8") + return " scripts/release/released-ci.yml -> .github/workflows/ci.yml" + + def managed_paths(entry: dict) -> list[tuple[Path, Path, bool]]: """Yield (src, dest_rel, is_dir) managed mappings for one repo entry. Sources are absolute monorepo paths; dest_rel is relative to the repo root. """ - # Aggregate repos (e.g. leanprover/hex) manage no source from the monorepo: + # Aggregate repos (e.g. leanprover/hex) manage no library source: # their umbrella lakefile, umbrella .lean and README live only in the released - # repo. The sync just rewrites their cross-repo pins + manifest. + # repo. Their centrally owned CI workflow is applied separately by + # apply_ci_workflow; this function only describes library-source mappings. if entry.get("pins_only"): return [] lib = entry["lib"] @@ -195,6 +228,7 @@ def apply_paths(entry: dict, clone: Path) -> list[str]: rendered = aggregate_readme.render(manifest, REPO_ROOT / template) (clone / "README.md").write_text(rendered, encoding="utf-8") notes.append(f" {template} + released.yml -> README.md (generated)") + notes.append(apply_ci_workflow(entry, clone)) if entry.get("pins_only"): return notes lib = entry["lib"] @@ -254,8 +288,10 @@ def _receive_pack_status(repo: str, token: str) -> int: `GET .git/info/refs?service=git-receive-pack` is the handshake `git push` performs before sending anything, so it is authorized exactly like a - push (`Contents: write`) and has no side effects: 200 means this token can - push, 401/403 mean it cannot, 404 means the repository is not there. + content push (`Contents: write`) and has no side effects: 200 means this + token can push ordinary content, 401/403 mean it cannot, 404 means the + repository is not there. GitHub's separate Workflows permission is checked + only when a push changes `.github/workflows`. """ auth = base64.b64encode(f"x-access-token:{token}".encode()).decode() request = urllib.request.Request( @@ -278,7 +314,9 @@ def selection_check(repo: str, token: str) -> str | None: first token even when only a later token holds the write grant, and the failure then surfaces at push time, after earlier repositories were already published (this has actually bitten a first publish). The - receive-pack handshake is authorized exactly like the push itself. + receive-pack handshake is authorized like an ordinary content push. It + cannot preflight the separate Workflows permission needed when this sync + updates `.github/workflows/ci.yml`. A repository that does not exist answers 404; an anonymous metadata probe separates "missing" from anything odder. Any other status is reported as @@ -321,8 +359,9 @@ def route_tokens(entries: list[dict], tokens: list[str]) -> tuple[dict[str, str] it, and every later clone and push uses the token routed here. A library released here but on no token's list would otherwise fail partway through, after earlier - repos were already published. The probe authorizes like the push itself; - see `selection_check`. + repos were already published. The probe authorizes ordinary content pushes; + the separate Workflows grant required by the managed CI update cannot be + preflighted this way. See `selection_check`. """ routed: dict[str, str] = {} blocked: list[str] = [] @@ -451,6 +490,34 @@ def validate_skeleton(entry: dict, clone: Path) -> None: ) +def validate_ci_helpers(entry: dict, clone: Path) -> None: + """Require every centrally managed CI helper to exist in the mirror. + + Release workflows are managed here, while existing ``scripts/ci`` helpers + remain part of each mirror's skeleton. Validate that boundary before any + publication writes so a central workflow cannot point at a missing script. + """ + short = entry["repo"].split("/", 1)[1] + workflow = released_ci_workflows()[short] + parsed = yaml.load(workflow, Loader=yaml.BaseLoader) + jobs = parsed.get("jobs", {}) if isinstance(parsed, dict) else {} + helpers: set[str] = set() + for job in jobs.values(): + if not isinstance(job, dict): + continue + for step in job.get("steps", []): + command = step.get("run") if isinstance(step, dict) else None + if isinstance(command, str): + helpers.update( + re.findall(r"scripts/ci/[A-Za-z0-9_.\-/]+", command) + ) + missing = sorted(path for path in helpers if not (clone / path).is_file()) + if missing: + raise RuntimeError( + f"released repository {entry['repo']} lacks CI helpers {missing}" + ) + + def rewrite_external_pins(clone: Path, pins: dict[str, dict[str, str]]) -> list[str]: """Synchronize direct non-Hex requirements with the monorepo lock. @@ -801,6 +868,7 @@ def sync_repo(entry: dict, source_sha: str, token: str | None, dry_run: bool, return False print(msg + " Overriding (--force).") validate_skeleton(entry, clone) + validate_ci_helpers(entry, clone) for line in apply_paths(entry, clone): print(line) if not entry.get("pins_only"): @@ -823,6 +891,15 @@ def sync_repo(entry: dict, source_sha: str, token: str | None, dry_run: bool, for l in status.splitlines(): print(f" {l}") if dry_run: + workflow_diff = run( + ["git", "diff", "--", ".github/workflows/ci.yml"], + cwd=clone, + capture=True, + ) + if workflow_diff: + print(" managed workflow diff:") + for line in workflow_diff.splitlines(): + print(f" {line}") synced[short] = head # stand-in so downstream pin previews resolve print(" DRY-RUN: not committing or pushing") return False @@ -857,8 +934,9 @@ def main() -> int: ap = argparse.ArgumentParser(description="Publish released split repos from the monorepo.") ap.add_argument("--dry-run", action="store_true", help="print planned changes; do not push") ap.add_argument("--token", action="append", default=None, - help="GitHub token with contents:write on (a subset of) the " - "released repos; repeatable, tried in order per repo. " + help="GitHub token with contents:write and workflows:write " + "on (a subset of) the released repos; repeatable, " + "tried in order per repo. " "Defaults to $RELEASED_SYNC_PAT, $RELEASED_SYNC_PAT_2, ...") ap.add_argument("--only", help="sync only this repo short-name (e.g. hex-matrix)") ap.add_argument("--force", action="store_true", @@ -916,7 +994,8 @@ def main() -> int: f"token {index + 1}: {sum(1 for t in repo_token.values() if t == token)}" for index, token in enumerate(tokens)) print(f"token preflight: all {len(targets)} target repositories are covered " - f"({per_slot}; the probe authorizes like the push itself, see selection_check)") + f"({per_slot}; Contents grants verified; Workflows grants are " + "checked by GitHub when workflow changes are pushed)") failed_repo: str | None = None current_repo = "" diff --git a/scripts/release/test_check_released_manifest.py b/scripts/release/test_check_released_manifest.py index 58d3dabba..bd810f10f 100644 --- a/scripts/release/test_check_released_manifest.py +++ b/scripts/release/test_check_released_manifest.py @@ -8,10 +8,12 @@ import subprocess import tempfile import unittest +from unittest.mock import patch from pathlib import Path from types import SimpleNamespace from scripts.release.check_released_manifest import ( + check_ci_workflows, check_phase_admission, parse_sync_baseline, published_repositories, @@ -93,5 +95,67 @@ def test_malformed_baseline_is_rejected(self) -> None: parse_sync_baseline('{"hex-example": "short"}', "test baseline") +class ReleasedCiTests(unittest.TestCase): + @staticmethod + def workflow() -> str: + from scripts.release.sync_released import released_ci_workflows + + return released_ci_workflows()["hex-basic"] + + def check(self, workflow: str) -> None: + entries = [{"repo": "leanprover/hex-example"}] + with patch( + "scripts.release.check_released_manifest.released_ci_workflows", + return_value={"hex-example": workflow}, + ): + check_ci_workflows(entries) + + def test_workflow_set_must_match_manifest(self) -> None: + entries = [{"repo": "leanprover/hex-example"}] + with ( + patch( + "scripts.release.check_released_manifest.released_ci_workflows", + return_value={"hex-other": "name: CI\n"}, + ), + self.assertRaisesRegex(ValueError, "differs from the release manifest"), + ): + check_ci_workflows(entries) + + def test_complete_workflow_is_accepted(self) -> None: + self.check(self.workflow()) + + def test_restore_and_save_paths_must_match(self) -> None: + workflow = self.workflow() + marker = " .lake/packages/hex-test-kit/.lake/build\n" + head, tail = workflow.rsplit(marker, 1) + with self.assertRaisesRegex(ValueError, "run-unique save key"): + self.check( + head + " .lake/packages/HexOther/.lake/build\n" + tail + ) + + def test_restore_prefix_must_match_unique_key(self) -> None: + workflow = self.workflow().replace( + "restore-keys: |\n lake-build-", + "restore-keys: |\n wrong-build-", + 1, + ) + with self.assertRaisesRegex(ValueError, "run-unique save key"): + self.check(workflow) + + def test_main_run_must_not_be_cancelled(self) -> None: + workflow = self.workflow().replace( + "cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}", + "cancel-in-progress: true", + 1, + ) + with self.assertRaisesRegex(ValueError, "terminal cache save"): + self.check(workflow) + + def test_main_push_trigger_is_required(self) -> None: + workflow = self.workflow().replace("branches: [main]", "branches: [dev]", 1) + with self.assertRaisesRegex(ValueError, "main pushes"): + self.check(workflow) + + if __name__ == "__main__": unittest.main() diff --git a/scripts/release/test_sync_released.py b/scripts/release/test_sync_released.py index 3ecc1e903..7e3d9c4b3 100644 --- a/scripts/release/test_sync_released.py +++ b/scripts/release/test_sync_released.py @@ -48,17 +48,32 @@ def test_apply_paths_removes_obsolete_released_path(self) -> None: stale.mkdir(parents=True) (stale / "Conformance.lean").write_text("stale\n", encoding="utf-8") entry = { + "repo": "leanprover/hex-bridge", "lib": "HexBridge", "readme": False, "umbrella": False, "spec": None, "remove_paths": ["conformance"], } - with patch.object(sync_released, "REPO_ROOT", source): + workflows = self.repo / "released-ci.yml" + workflows.write_text( + "workflows:\n hex-bridge: |\n name: CI\n", encoding="utf-8" + ) + with ( + patch.object(sync_released, "REPO_ROOT", source), + patch.object(sync_released, "RELEASED_CI", workflows), + ): notes = sync_released.apply_paths(entry, clone) self.assertFalse((clone / "conformance").exists()) self.assertIn(" remove conformance", notes) - with patch.object(sync_released, "REPO_ROOT", source): + self.assertEqual( + (clone / ".github" / "workflows" / "ci.yml").read_text(), + "name: CI\n", + ) + with ( + patch.object(sync_released, "REPO_ROOT", source), + patch.object(sync_released, "RELEASED_CI", workflows), + ): notes = sync_released.apply_paths(entry, clone) self.assertNotIn(" remove conformance", notes) @@ -73,14 +88,20 @@ def test_apply_paths_rejects_symlinked_removal_parent(self) -> None: (outside / "kept").write_text("keep\n", encoding="utf-8") (clone / "linked").symlink_to(outside, target_is_directory=True) entry = { + "repo": "leanprover/hex-bridge", "lib": "HexBridge", "readme": False, "umbrella": False, "spec": None, "remove_paths": ["linked/kept"], } + workflows = self.repo / "released-ci.yml" + workflows.write_text( + "workflows:\n hex-bridge: |\n name: CI\n", encoding="utf-8" + ) with ( patch.object(sync_released, "REPO_ROOT", source), + patch.object(sync_released, "RELEASED_CI", workflows), self.assertRaisesRegex( ValueError, "unsafe remove_paths destination escapes clone" ), @@ -95,6 +116,68 @@ def test_removal_paths_rejects_unsafe_destinations(self) -> None: ): sync_released.removal_paths({"remove_paths": [path]}) + def test_released_ci_workflow_requires_complete_text_mapping(self) -> None: + source = self.repo / "released-ci.yml" + source.write_text("workflows:\n hex-example: 42\n", encoding="utf-8") + with self.assertRaisesRegex(ValueError, "map names to text"): + sync_released.released_ci_workflows(source) + + def test_apply_ci_workflow_requires_repository_entry(self) -> None: + source = self.repo / "released-ci.yml" + source.write_text( + "workflows:\n hex-other: |\n name: CI\n", encoding="utf-8" + ) + with ( + patch.object(sync_released, "RELEASED_CI", source), + self.assertRaisesRegex(RuntimeError, "no managed CI workflow"), + ): + sync_released.apply_ci_workflow( + {"repo": "leanprover/hex-example"}, self.repo / "clone" + ) + + def test_pins_only_apply_overwrites_managed_ci(self) -> None: + source = self.repo / "released-ci.yml" + source.write_text( + "workflows:\n hex: |\n name: Managed CI\n", encoding="utf-8" + ) + clone = self.repo / "clone" + workflow = clone / ".github" / "workflows" / "ci.yml" + workflow.parent.mkdir(parents=True) + workflow.write_text("name: Old CI\n", encoding="utf-8") + with patch.object(sync_released, "RELEASED_CI", source): + notes = sync_released.apply_paths( + {"repo": "leanprover/hex", "pins_only": True}, clone + ) + self.assertEqual(workflow.read_text(), "name: Managed CI\n") + self.assertEqual( + notes, + [" scripts/release/released-ci.yml -> .github/workflows/ci.yml"], + ) + + def test_managed_ci_requires_unmanaged_helpers(self) -> None: + source = self.repo / "released-ci.yml" + source.write_text( + "workflows:\n" + " hex-example: |\n" + " name: CI\n" + " jobs:\n" + " build:\n" + " steps:\n" + " - run: bash scripts/ci/check_example.sh\n", + encoding="utf-8", + ) + entry = {"repo": "leanprover/hex-example"} + with ( + patch.object(sync_released, "RELEASED_CI", source), + self.assertRaisesRegex(RuntimeError, "lacks CI helpers"), + ): + sync_released.validate_ci_helpers(entry, self.repo) + helper = self.repo / "scripts" / "ci" / "check_example.sh" + helper.parent.mkdir(parents=True) + helper.write_text("#!/bin/sh\n", encoding="utf-8") + with patch.object(sync_released, "RELEASED_CI", source): + sync_released.validate_ci_helpers(entry, self.repo) + def test_direct_pins_rewrite_toml_and_lean(self) -> None: (self.repo / "lakefile.toml").write_text( '[[require]]\n'