ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:
  # workflow_dispatch is useful for ad-hoc conformance/oracle runs; the
  # conformance work now lives in this single job (see below), so keep it.
  workflow_dispatch:

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  # Cancel superseded PR runs, but let main runs finish: the publish
  # step only runs at the end, and main merges arrive faster than a cold
  # build, so cancelling main would mean the Lake cache never publishes.
  cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}

# One ubuntu job (SPEC/CI.md § Job-count budget). The build graph is
# elaborated once here; the two independent verification tails (bench
# verify and the conformance/oracle suite) then run concurrently as
# in-job `background:` steps, so a single runner does the work that used
# to duplicate the whole hex build across two workflows.
jobs:
  build:
    runs-on: ubuntu-latest
    # Force `shell: bash` on every run step so they all run under
    # `bash --noprofile --norc -eo pipefail` (an unspecified Linux run step is
    # only `bash -e`, without `pipefail`). The fail-closed sentinel logic below
    # relies on a failed command in a pipeline aborting the step before the
    # success `touch`.
    defaults:
      run:
        shell: bash
    steps:
      - uses: actions/checkout@v4
        with:
          # The release-manifest admission check reads release-sync-baseline.
          fetch-depth: 0
      # --- Structural + source lints ---
      - run: python3 scripts/check_copyright_headers.py
      - name: Lint Lean file line counts (SPEC/CI.md §Source-file lints)
        run: python3 scripts/check_file_line_counts.py
      - name: Check dependency DAG and trusted-internals imports
        run: |
          python3 -m unittest scripts/test_check_dag.py
          python3 scripts/check_dag.py
      - name: Check the released manifest and Phase-7 admission state
        run: |
          python3 -m unittest scripts/release/test_check_released_manifest.py
          python3 scripts/release/check_released_manifest.py
      - name: Check the manual's released/unreleased split matches released.yml
        run: python3 scripts/release/check_manual_split.py
      - run: python3 -m unittest scripts/release/test_sync_released.py
      - run: python3 scripts/release/check_trust_surface.py
      - name: Cross-check every compiled clmul path (HexGF2/SPEC/hex-gf2.md)
        run: bash scripts/ci/check_clmul_paths.sh
      - run: python3 scripts/check_phase4.py
      - name: Check Phase 7 chapters and anchored tutorials (PLAN/Phase7.md)
        run: |
          python3 -m unittest scripts/test_check_phase7.py
          python3 scripts/check_phase7.py
      - name: Run bench source lints (SPEC/benchmarking.md)
        run: |
          python3 -m unittest scripts/ci/test_check_benches_mathlib_free.py
          python3 -m unittest scripts/ci/test_check_persistent_flint_warmup.py
          python3 -m unittest scripts/bench/test_fresh_module_sweep.py
          python3 -m unittest scripts/bench/test_real_roots_mathlib_sweep.py
          python3 -m unittest scripts/bench/test_bz_mathlib_sweep.py
          python3 -m unittest scripts/bench/test_berlekamp_mathlib_sweep.py
          python3 -m unittest scripts/bench/test_hexrcf_proof_sweep.py
          python3 -m unittest scripts/bench/test_primality_policy_sweeps.py
          python3 -m unittest scripts/bench/test_primality_negative_sweep.py
          python3 -m unittest scripts/bench/test_primality_mathlib_proof_sweep.py
          python3 -m unittest scripts/oracle/test_flint_mpoly_bench.py
          python3 -m unittest scripts/oracle/test_flint_fmpq_bench.py
          python3 -m unittest scripts/oracle/test_singular_mpoly_bench.py
          python3 -m unittest scripts/oracle/test_rcf_flint_bench.py
          python3 scripts/ci/check_benches_mathlib_free.py
          python3 scripts/ci/check_persistent_flint_warmup.py
      - name: Verify conformance matrix invariant
        run: python3 scripts/conformance_targets.py --check
      - name: Validate committed PNT+ inventory (offline)
        run: |
          python3 -m unittest scripts/maintenance/test_pnt_inventory.py
          python3 scripts/maintenance/pnt_inventory.py --check
      # --- System + Python deps (union of the bench comparator and the oracles) ---
      - name: Install system dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y libgmp-dev libntl-dev pkg-config libpari-dev pari-gp singular
      - name: Install Python dependencies (bench comparator + oracles)
        run: |
          python3 -m pip install --user \
            python-flint gmpy2 cypari2 conway-polynomials sympy matplotlib==3.11.1
          python3 -m unittest scripts/oracle/test_hermite_bench_drivers.py
      - name: Verify factorization measurements and figures are current
        run: |
          python3 scripts/bench/check_factor_sweep_freshness.py
          python3 scripts/plots/hexbz-cactus.py --check
      - name: Set up pinned Lean toolchain (no build)
        run: bash scripts/ci/setup_lean_toolchain.sh
      - name: Fetch Mathlib cache
        run: lake exe cache get
      - name: Verify Mathlib cache populated (hard fail on miss)
        run: bash scripts/ci/check_no_mathlib_rebuild.sh
      - name: Configure Lean shared library path
        run: |
          lean_prefix="$(lean --print-prefix)"
          test -d "$lean_prefix/lib/lean"
          echo "LD_LIBRARY_PATH=$lean_prefix/lib/lean:${LD_LIBRARY_PATH:-}" \
            >> "$GITHUB_ENV"
      - name: Restore .lake/build (Hex modules only)
        id: hex-build-cache
        uses: actions/cache/restore@v4
        with:
          path: |
            .lake/build/lib/lean/Hex*
            .lake/build/ir/Hex*
          key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
          restore-keys: |
            lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-
      # --- Lake artifact cache (dormant unless the LAKE_CACHE_*_PUBLIC repo
      # variables are set). A rev-precise, cross-runner fallback to the
      # actions/cache restore above: when that misses (eviction, a new branch),
      # this restores hex-dev's oleans by Git revision so the build below
      # recompiles only changed modules. Mathlib still comes from `lake exe
      # cache get`. ---
      - name: Configure Lake artifact cache (no-op unless endpoints set)
        env:
          PUBLIC_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ARTIFACT_ENDPOINT_PUBLIC }}
          PUBLIC_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_REVISION_ENDPOINT_PUBLIC }}
        run: |
          if [ -n "$PUBLIC_ARTIFACT_ENDPOINT" ] && [ -n "$PUBLIC_REVISION_ENDPOINT" ]; then
            CFG="$RUNNER_TEMP/lake-cache.toml"
            {
              echo 'cache.defaultService = "hex-public"'
              echo '[[cache.service]]'
              echo 'name = "hex-public"'
              echo 'kind = "s3"'
              echo "artifactEndpoint = \"$PUBLIC_ARTIFACT_ENDPOINT\""
              echo "revisionEndpoint = \"$PUBLIC_REVISION_ENDPOINT\""
            } > "$CFG"
            {
              echo "LAKE_CONFIG=$CFG"
              echo "LAKE_CACHE_DIR=$PWD/.lake/cache"
              echo "LAKE_ARTIFACT_CACHE=true"
              echo "LAKE_RESTORE_ARTIFACTS=true"
              echo "HEX_CACHE_ENABLED=1"
            } >> "$GITHUB_ENV"
            echo "::notice::Lake artifact cache enabled (service hex-public)"
          else
            echo "::notice::Lake artifact cache not configured (set the LAKE_CACHE_*_PUBLIC repo variables to enable)"
          fi
      - name: Restore hex-dev oleans from the Lake cache (anonymous; non-fatal)
        if: ${{ steps.hex-build-cache.outputs.cache-matched-key == '' && env.HEX_CACHE_ENABLED == '1' }}
        run: |
          lake cache get --max-revs=20 --service hex-public --repo kim-em/hex-dev \
            || echo "::warning::lake cache miss for this revision; building from source"
      - name: Disable implicit Lake cache restores during build
        run: echo "LAKE_NO_CACHE=true" >> "$GITHUB_ENV"
      # With the cache env now active, assert the entire Mathlib graph is already
      # up to date. `--no-build` reports stale targets and exits non-zero instead
      # of building them, so this fails loudly (never silently rebuilds) if the
      # cache wiring ever invalidates the prebuilt Mathlib oleans.
      - name: Assert Mathlib will not rebuild (lake build --no-build)
        run: lake build --no-build Mathlib
      # Two target sets. HEX_LIB_TARGETS are the libraries we cache: their oleans
      # are the expensive elaboration and they restore cleanly. Executables are
      # deliberately NOT cached -- the artifact cache restores an exe's module
      # outputs but not its linked `bin/` binary, so a restored exe looks
      # up-to-date yet cannot run. By never publishing them, exes always link
      # fresh against the restored libs, which is cheap.
      - name: Define the hex-dev cache + build target sets
        run: |
          echo "HEX_LIB_TARGETS=HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexPrimalityElabProbe HexPrimalityMathlibProofProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
          echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexprimality_policy_probe hexprimality_fuel_probe hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexrowreduce_bench hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV"
      # Shared build. The libraries, bench exes, conformance #guard drivers, and
      # emit-fixture exes are all elaborated here so the two verification tails
      # below only *run* things, never rebuild them -- which is what lets the
      # previously-separate conformance workflow reuse this job's build instead
      # of recompiling the whole graph a second time. Kept as three sequential
      # `lake build` invocations rather than one: a single invocation lets Lake
      # parallelize the Mathlib-heavy library compiles, the exe links, the
      # conformance/fixture builds, and the Verso manual all at once, whose
      # combined memory peak exhausts the runner. Sequential invocations share
      # `.lake/build` (no recompilation) but cap the peak at whichever single
      # invocation is largest, each of which is known to fit.
      - name: Build hex libraries + bench exes
        run: lake build ${HEX_LIB_TARGETS} ${HEX_EXE_TARGETS} HexTruncatedSeriesTests
      - name: Verify deterministic HexPrimality table regeneration
        run: python3 scripts/bench/check_prime_table.py
      - name: Build conformance + emit-fixture targets
        run: |
          lake build \
            HexConformance hextruncatedseries_emit_fixtures \
            hexmvpoly_emit_fixtures hexsparsepoly_emit_fixtures \
            hexmodular_emit_fixtures hexpolyzgcd_emit_fixtures \
            hexpolysmith_emit_fixtures \
            hexpoly_emit_fixtures hexpolyfp_emit_fixtures \
            hexberlekamp_emit_fixtures \
            hexbz_emit_fixtures hexpolyz_emit_fixtures \
            hexgf2_emit_fixtures hexgfq_emit_fixtures \
            hexgfqring_emit_fixtures hexgfqfield_emit_fixtures \
            hexhensel_emit_fixtures hexprimality_emit_fixtures \
            hexintfactor_emit_fixtures \
            hexconway_emit_fixtures \
            hexrowreduce_emit_fixtures hexdeterminant_emit_fixtures \
            hexbareiss_emit_fixtures hexhermite_emit_fixtures \
            hexsmith_emit_fixtures hexcharpoly_emit_fixtures \
            hexminpoly_emit_fixtures \
            hexgramschmidt_emit_fixtures \
            hexlll_emit_fixtures hexrealroots_emit_fixtures \
            hexrcf_emit_fixtures \
            hexroots_emit_fixtures hexresultant_emit_fixtures \
            hexnumberfield_emit_fixtures \
            hexnumberfieldtower_emit_fixtures
      - name: Build HexManual
        run: lake build HexManual
      # --- Parallel verification tails (single job, in-job parallel steps) ---
      # Both tails only read the already-built .lake/build; they write to
      # disjoint outputs, so they are safe to run concurrently. Each touches a
      # sentinel file as its final action *only* on success (the runner shell is
      # `bash -eo pipefail`, so any earlier failure exits before the touch). The
      # gate step after `wait-all:` then fails the job unless BOTH sentinels
      # exist -- a fail-closed backstop on top of `wait-all:`'s own failure
      # propagation, so gating never depends on background-step exit codes.
      # (`shell: bash` is set job-wide, so these run under `-eo pipefail`.)
      - name: Bench verify (smoke gate per SPEC/benchmarking.md §CI integration)
        id: bench
        background: true
        env:
          # Hard cap per SPEC/benchmarking.md §CI integration "Time budget".
          BENCH_VERIFY_HARD_CAP_SECONDS: "360"
        run: |
          bash scripts/ci/check_bench_verify_budget.sh \
            hextruncatedseries_bench \
            hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench \
            hexmvpoly_bench hexmvgcd_bench \
            hexpolyz_bench \
            hexpolyzgcd_bench hexsparsepoly_bench hexpolyfp_bench \
            hexmodarith_bench \
            hexmodular_bench \
            hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench \
            hexhensel_bench hexprimality_bench hexintfactor_bench \
            hexberlekamp_bench hexbz_bench \
            hexconway_bench hexdeterminant_bench hexmatrix_bench hexrowreduce_bench \
            hexhermite_bench hexsmith_bench \
            hexcharpoly_bench hexminpoly_bench \
            hexgramschmidt_bench hexlll_gram_bench \
            hexrealroots_bench hexrcf_bench hexroots_bench \
            hexresultant_bench hexnumberfield_bench \
            hexnumberfieldtower_bench hexinterval_decision_bench
          # These two interval scheduler spikes are exact logical-count
          # canaries rather than lean-bench timing registrations. Build them
          # above and exercise their fixtures directly here.
          .lake/build/bin/hex_interval_scheduler_spike canary
          .lake/build/bin/hex_interval_policy_frontier_spike canary
          # The decision target has fixed timing registrations above plus a
          # separate canonical logical policy-comparison canary.
          .lake/build/bin/hexinterval_decision_bench canary
          touch "$RUNNER_TEMP/bench.ok"
      - name: Conformance oracles + BZ gates
        id: conformance
        background: true
        env:
          # Missing comparator packages are release failures, not green skips.
          HEX_REQUIRE_ORACLES: "1"
        run: |
          bash scripts/ci/run_oracles.sh
          # Deterministic anti-regression gate: a recombination blow-up,
          # unexpected method downgrade, or unexpected decline/fallback fails the
          # merge even though it would still factor correctly.
          python3 scripts/oracle/bz_trace_gate.py
          # Catastrophic (order-of-magnitude) slow-downs trip this generous cap.
          timeout 180 lake exe hexbz_emit_fixtures > /dev/null
          touch "$RUNNER_TEMP/conformance.ok"
      - wait-all:
      - name: Gate on parallel verification results (fail-closed)
        run: |
          rc=0
          [ -f "$RUNNER_TEMP/bench.ok" ] || { echo "::error::Bench verify did not complete successfully"; rc=1; }
          [ -f "$RUNNER_TEMP/conformance.ok" ] || { echo "::error::Conformance/oracles did not complete successfully"; rc=1; }
          exit $rc
      # Save only a fully verified main snapshot. Pull-request caches are scoped
      # to their merge ref and cannot help another PR, so saving one per PR would
      # churn the repository's cache quota without providing shared reuse.
      - name: Save .lake/build (Hex modules only; main only)
        if: ${{ github.ref == 'refs/heads/main' && github.event_name == 'push' && steps.hex-build-cache.outputs.cache-hit != 'true' }}
        uses: actions/cache/save@v4
        with:
          path: |
            .lake/build/lib/lean/Hex*
            .lake/build/ir/Hex*
          key: lake-build-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
      # Publish only after every verification gate passes. R2 remains a
      # cross-runner fallback for a GitHub cache miss and for external consumers.
      - name: Publish hex-dev oleans to the Lake cache (main only)
        if: ${{ github.ref == 'refs/heads/main' && github.event_name == 'push' && env.HEX_CACHE_ENABLED == '1' }}
        env:
          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
          S3_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ARTIFACT_ENDPOINT }}
          S3_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_REVISION_ENDPOINT }}
        run: |
          if [ -z "$LAKE_CACHE_KEY" ] || [ -z "$S3_ARTIFACT_ENDPOINT" ] || [ -z "$S3_REVISION_ENDPOINT" ]; then
            echo "::notice::upload not configured (LAKE_CACHE_KEY / endpoints); skipping publish"; exit 0
          fi
          CFG="$RUNNER_TEMP/lake-cache-upload.toml"
          {
            echo 'cache.defaultUploadService = "hex-r2"'
            echo '[[cache.service]]'
            echo 'name = "hex-r2"'
            echo 'kind = "s3"'
            echo "artifactEndpoint = \"$S3_ARTIFACT_ENDPOINT\""
            echo "revisionEndpoint = \"$S3_REVISION_ENDPOINT\""
          } > "$CFG"
          export LAKE_CONFIG="$CFG"
          # HexManual is built in its own memory-bounded phase above, so append
          # it only while collecting the outputs to publish.
          lake build --no-build -o .lake/outputs.jsonl ${HEX_LIB_TARGETS} HexManual
          echo "mapping entries: $(wc -l < .lake/outputs.jsonl)"
          lake cache put .lake/outputs.jsonl --service hex-r2 --repo kim-em/hex-dev
      - name: Upload failure records
        if: failure()
        uses: actions/upload-artifact@v4
        with:
          name: conformance-failures
          path: conformance-failures/*.json
          if-no-files-found: ignore