feat(interval): prove a mixed sine-exp tactic path #11583
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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: | |
| 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 | |
| - run: python3 scripts/check_dag.py | |
| - run: 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 | |
| - run: python3 scripts/check_phase4.py | |
| - name: Lint benches are Mathlib-free (SPEC/benchmarking.md §Mathlib-free benches) | |
| run: | | |
| python3 -m unittest scripts/ci/test_check_benches_mathlib_free.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_hexrcf_proof_sweep.py | |
| python3 -m unittest scripts/oracle/test_rcf_flint_bench.py | |
| python3 scripts/ci/check_benches_mathlib_free.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 | |
| - name: Install Python dependencies (bench comparator + oracles) | |
| run: | | |
| python3 -m pip install --user \ | |
| python-flint cypari2 conway-polynomials sympy matplotlib==3.11.1 | |
| - 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 Lean toolchain (no build) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| auto-config: false | |
| build: false | |
| use-mathlib-cache: false | |
| - 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: | | |
| toolchain="$(sed 's|/|--|; s|:|---|' lean-toolchain)" | |
| echo "LD_LIBRARY_PATH=$HOME/.elan/toolchains/$toolchain/lib/lean:${LD_LIBRARY_PATH:-}" \ | |
| >> "$GITHUB_ENV" | |
| - name: Restore .lake/build (Hex modules only) | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/build/lib/lean/Hex* | |
| .lake/build/ir/Hex* | |
| key: lake-build-${{ github.workflow }}-${{ github.run_id }} | |
| restore-keys: | | |
| lake-build-${{ github.workflow }}- | |
| # --- 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: ${{ env.HEX_CACHE_ENABLED == '1' }} | |
| run: | | |
| lake cache get --service hex-public --repo kim-em/hex-dev \ | |
| || echo "::warning::lake cache miss for this revision; building from source" | |
| 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 HexArith HexPoly HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexGramSchmidt HexLLL HexMatrixMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples" >> "$GITHUB_ENV" | |
| echo "HEX_EXE_TARGETS=hexarith_bench hexpoly_bench hexmvpoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexgramschmidt_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_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} | |
| - name: Build conformance + emit-fixture targets | |
| run: | | |
| lake build \ | |
| HexConformance hexmvpoly_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 \ | |
| hexconway_emit_fixtures \ | |
| hexrowreduce_emit_fixtures hexdeterminant_emit_fixtures \ | |
| hexbareiss_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 | |
| # Publish hex-dev's oleans on a trusted main push so later builds (and any | |
| # consumer) restore them. Skips silently without the upload key. | |
| - 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 | |
| # --- 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 \ | |
| hexarith_bench hexpoly_bench hexmvpoly_bench hexpolyz_bench \ | |
| hexpolyfp_bench hexmodarith_bench \ | |
| hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench \ | |
| hexhensel_bench hexberlekamp_bench hexbz_bench \ | |
| hexconway_bench hexdeterminant_bench hexmatrix_bench \ | |
| hexgramschmidt_bench hexlll_gram_bench \ | |
| hexrealroots_bench hexrcf_bench hexroots_bench \ | |
| hexresultant_bench hexnumberfield_bench \ | |
| hexnumberfieldtower_bench | |
| # The policy-frontier spike is an exact logical-count canary rather | |
| # than a lean-bench timing registration. Build it above and exercise | |
| # all three representation fixtures directly here. | |
| .lake/build/bin/hex_interval_policy_frontier_spike 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 | |
| - name: Upload failure records | |
| if: failure() | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: conformance-failures | |
| path: conformance-failures/*.json | |
| if-no-files-found: ignore |