diff --git a/.github/actions/lean-axiom/action.yml b/.github/actions/lean-axiom/action.yml new file mode 100644 index 0000000000..c1fe58808e --- /dev/null +++ b/.github/actions/lean-axiom/action.yml @@ -0,0 +1,360 @@ +name: 'Lean axiom check' +description: > + Composite-action twin of .github/workflows/lean-axiom.yml (reusable), for + callers routed to the specialised self-hosted Lean pool (#14337 tranche 2a, + arbitrage (B) composite action, ai-01 DM msg-20260904T132737-02hnpi). Same + per-declaration #print-axioms audit, same forbidden-axiom policy, same + honesty knobs (fail-on-sorry, include-i18n-siblings). The reusable stays + the caller of record for the 25 unrouted lakes until 2b. + +inputs: + project-path: + description: 'Repo-relative path to the lake project root' + required: true + display-name: + description: 'Human-readable project name (for job labels)' + required: true + target-modules: + description: "Comma-separated dotted module names to check, or '*' to derive the list at runtime from what lake compiles" + required: true + include-i18n-siblings: + description: 'When target-modules is "*", whether the runtime derivation keeps `_en` i18n siblings. Default false (FR-only measurement).' + required: false + default: 'false' + allow-axioms: + description: 'Comma-separated additional axioms to whitelist beyond the defaults (propext, funext, Classical.choice, Quot.lift, Quot.mk, Quot.sound).' + required: false + default: '' + fail-on-sorry: + description: 'Whether a transitive sorryAx fails the run. false = report has_sorry without gating (honesty knob, not leniency).' + required: false + default: 'true' + +runs: + using: composite + steps: + # NOTE (composite vs reusable): the CALLER job carries `actions/checkout` + # before this action -- a local composite (`./.github/actions/...`) can + # only resolve after the repository is materialised in the workspace. + - name: Install elan + shell: bash + run: | + curl -sSfL https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz + ./elan-init -y --default-toolchain none + echo "$HOME/.elan/bin" >> $GITHUB_PATH + + - name: Cache Lake build artifacts + uses: actions/cache@v4 + with: + path: ${{ inputs.project-path }}/.lake + key: lake-${{ inputs.display-name }}-axiom-${{ runner.os }}-${{ hashFiles(format('{0}/lakefile.lean', inputs.project-path), format('{0}/lakefile.toml', inputs.project-path), format('{0}/lean-toolchain', inputs.project-path)) }} + restore-keys: lake-${{ inputs.display-name }}-axiom-${{ runner.os }}- + + # Hosted leg only (#14337 tranche 2a): the specialised Lean pool carries + # its swap OUTSIDE the job (cgroup `--memory-swap 24g`, supervise.sh + # cmd_lean) precisely because a job container has no sudo to fallocate. + # This workflow rebuilds the lake too (its cache key differs from + # lean-build's, so it can miss independently) — on the hosted leg the swap + # stays the OOM guard (observed on PR #9798: BOTH proof-integrity jobs + # died at exit 143 alongside the build job). + - name: Add swap space (hosted only) + if: runner.environment == 'github-hosted' + shell: bash + run: | + df -h /mnt + sudo fallocate -l 32G /mnt/lean-swap + sudo chmod 600 /mnt/lean-swap + sudo mkswap /mnt/lean-swap + sudo swapon /mnt/lean-swap + free -h + + - name: Lake build + shell: bash + working-directory: ${{ inputs.project-path }} + run: | + set -o pipefail # propagate lake's exit code through the pipeline (FAILED must + # exit != 0; See incident conway_lean HashlifeCorrectness L1058, 2026-06-14). + lake exe cache get || true + # On failure, surface the error lines the `tail` window loses (See #8915). + if lake -R build 2>&1 | tee "$RUNNER_TEMP/lake.log" | tail -10; then + : + else + rc=$? + echo "::group::Error lines from the full lake log (See #8915)" + grep -nE "^error:|\.lean:[0-9]+:[0-9]+: (error|warning)" "$RUNNER_TEMP/lake.log" | head -100 || true + echo "::endgroup::" + exit "$rc" + fi + + - name: Setup Python + uses: actions/setup-python@v5 + with: + python-version: "3.13" + + # No `working-directory:` here, and no `cd`, on purpose. Both paths are + # derived from the environment below. A `working-directory:` on this step + # is silently cancelled by any `cd` inside `run:`, which is exactly the + # defect this replaces: the step declared the lake root, the `run` block + # then moved to `$GITHUB_WORKSPACE`, and the check ran against the repo + # root where no lake exists. `lake build` (which has a correct + # `working-directory` and no `cd`) succeeded, so the job looked like an + # axiom violation while it was really a "no lake here" error. See #8712. + - name: Run axiom check + shell: bash + env: + MODULES: ${{ inputs.target-modules }} + ALLOW: ${{ inputs.allow-axioms }} + DISPLAY_NAME: ${{ inputs.display-name }} + PROJECT_PATH: ${{ inputs.project-path }} + FAIL_ON_SORRY: ${{ inputs.fail-on-sorry }} + INCLUDE_I18N_SIBLINGS: ${{ inputs.include-i18n-siblings }} + run: | + set -eu + python - <<'PY' + import os + import subprocess + import sys + from pathlib import Path + + # Both roots come from the environment, never from the cwd: the cwd of + # this step is an implementation detail of the runner, and depending on + # it is what broke the gate on its first real run (#8712). + repo_root = Path(os.environ["GITHUB_WORKSPACE"]).resolve() + if not (repo_root / "MyIA.AI.Notebooks").exists(): + sys.exit(f"repo root has no MyIA.AI.Notebooks/: {repo_root}") + sys.path.insert(0, str(repo_root / "MyIA.AI.Notebooks" / "SymbolicAI" / "Lean" / "agent_tests")) + + from lean_server import LeanVerifier # noqa: E402 + + # `axiom_lookup_anomalies` is the complement filter for the + # build_failed_returncode_* path (#10486, ai-01 c.1044). It returns the + # lines of raw_output that are NOT healthy `#print axioms` verdicts -- + # i.e. the actual error (unknown constant, type error) wherever it sits + # in the stream. select_diagnostic_lines misses `unknown constant` + # (no `error:` prefix) and falls back to a tail slice, which on a batch + # of 537 commands shows twenty healthy verdicts and hides the cause. + # Same version-skew fallback as above: degrade to the tail slice, never + # crash the gate on an ImportError from an older caller checkout. + try: + from lean_server import axiom_lookup_anomalies # noqa: E402 + except ImportError: + def axiom_lookup_anomalies(raw_output, limit=50): + lines = (raw_output or "").strip().splitlines() + return lines[-20:] + + # `target-modules: "*"` (issue #10889): derive the module list at + # runtime instead of trusting a hand-maintained caller list that drifts + # out of sync with the lake (26 modules were out of view on 4 lakes). + # discover_modules walks exactly what `lake build` compiles -- every + # `*.lean` under the project root minus `.lake/`, `.git/, `node_modules`, + # `.venv`, lakefile* and `lean-toolchain`. Its imports are stdlib-only + # (no PyYAML here), so importing it into this step is safe. + project_path = (repo_root / os.environ["PROJECT_PATH"]).resolve() + if not project_path.is_dir(): + sys.exit(f"lake project path does not exist: {project_path}") + + modules_raw = os.environ["MODULES"].strip() + if modules_raw == "*": + sys.path.insert(0, str(repo_root / "scripts" / "lean")) + from check_target_coverage import ( # noqa: E402 + discover_modules, + filter_i18n_siblings, + ) + + modules = sorted(discover_modules(project_path, None)) + # i18n `_en` siblings are excluded by default: any path SEGMENT + # ending in `_en` (dir or stem -- e.g. `Conway/Life_en.lean`), not + # only a root-level stem. Mirrors the FR-only measurement of #10889; + # a caller that wants the full bilingual surface opts in via + # `include-i18n-siblings: "true"`. The filter lives in the script + # (unit-tested) so the gate never carries a second copy of the rule. + if os.environ.get("INCLUDE_I18N_SIBLINGS", "false").strip().lower() != "true": + modules = sorted(filter_i18n_siblings(modules)) + if not modules: + sys.exit("target-modules='*' enumerated no modules under " + f"{project_path} (no .lean outside .lake/?). " + "A gate that inspects nothing must fail, not pass silently.") + else: + modules = [m.strip() for m in modules_raw.split(",") if m.strip()] + allow = [a.strip() for a in os.environ.get("ALLOW", "").split(",") if a.strip()] + display_name = os.environ["DISPLAY_NAME"] + + fail_on_sorry = os.environ.get("FAIL_ON_SORRY", "true").strip().lower() == "true" + + verifier = LeanVerifier() + verifier.project_dir = str(project_path) + + all_clean = True + sorry_modules = [] + zero_decl_design = [] # modules that legitimately declare nothing (root aggregators) + total_enumerated = 0 # lake-level non-vacuity (Gesture 2, ai-01 c.84) + print(f"=== Proof integrity axiom check ({display_name}) ===") + print(f"Project: {project_path}") + print(f"Gate on sorry: {'yes' if fail_on_sorry else 'no (reported, not gated)'}") + print(f"Modules: {modules}") + print(f"Additional allow-list: {allow if allow else '(none)'}") + print() + for mod in modules: + print(f"--- Module {mod} ---") + result = verifier.check_axioms( + mod, + whitelist=[ + "Classical.choice", + "propext", + "funext", + "Quot.lift", + "Quot.mk", + "Quot.sound", + *allow, + ], + fail_on_sorry=fail_on_sorry, + # The post-#8680 default is False (prover path), right for the + # agent harness which tracks sorries via `has_sorry` separately. + # A CI gate wants True by default so a transitive sorryAx fails + # the run -- but a lake with acknowledged open sorries opts out + # via `fail-on-sorry: false` rather than staying permanently red. + ) + n_decls = len(result["declarations"]) + total_enumerated += n_decls + print(f" declarations: {n_decls} enumerated") + # Criterion 1 (#8782): render WHICH declarations were audited, not + # only the count. A bare count hides both directions of the blind + # spot -- a module that enumerated zero decls (a gate that inspected + # nothing, "non applicable") AND a sorry-bearing module whose only + # public anchor reaching the proof front is buried among hundreds. + # Naming the audited decls lets a reviewer see, e.g., + # `hashlifeResult_central_correct` in the list and trust that the + # private sorry chain behind it was reached transitively. Sample- + # bounded (head + tail) so a large module does not flood the log. + decls = result["declarations"] + if decls: + sample = decls[:12] + tail = decls[-3:] if len(decls) > 15 else [] + parts = [", ".join(sample)] + if len(decls) > 12: + omitted = len(decls) - 12 - (len(tail) if tail else 0) + parts.append(f" ... (+{omitted} more)" if not tail + else f" ... (+{omitted} more) ... {', '.join(tail)}") + print(f" enumerated decls: {''.join(parts)}") + else: + print(f" enumerated decls: (none -- module is 'non applicable', " + f"a gate that inspected nothing)") + # On the build_failed_returncode_* path, check_axioms reads the + # returncode BEFORE parsing (lean_server.py:760), so axioms are + # NEVER collected -- `axioms: []` / `forbidden: []` / + # `has_sorry: False` are the path's hardcoded defaults, not + # measurements. Printing them bare made a dead build read as + # "no forbidden axioms, no sorry" (ai-01 c.1044 on #10486: the gate + # said "couldn't measure", not "clean despite flake"). Say so. + if result.get("error"): + print(f" axioms: (non mesuré -- échec de lookup, see error below)") + print(f" forbidden: (non mesuré -- échec de lookup)") + print(f" has_sorry: (non mesuré -- échec de lookup)") + else: + print(f" axioms: {result['axioms']}") + print(f" forbidden: {result['forbidden']}") + print(f" has_sorry: {result['has_sorry']}") + # `error` is the ONLY field that separates "the lake did not build / + # was not found" from "a forbidden axiom was reached". Omitting it + # made a dead build indistinguishable from a real violation in the + # logs, and cost a full misattribution on #8712 -- the summary + # blamed forbidden axioms while `forbidden` was empty. + if result.get("error"): + print(f" error: {result['error']}") + # `error` names the class of failure; `raw_output` names the + # cause. Without it, "build_failed_returncode_1" sends you to a + # local reproduction to learn what any CI log already had. + # + # Print the COMPLEMENT of the healthy form (ai-01 c.1044 on + # #10486): any non-blank line of raw_output that is NOT a + # `'decl' depends on axioms: [...]` / `does not depend on any + # axioms` verdict. On a healthy run this prints nothing. On a + # failed run it prints the cause (`unknown constant`, type + # error) wherever it sits in the stream -- bulletproof by + # position, unlike select_diagnostic_lines which matches the + # `error:` marker that an `unknown constant` lacks and then + # falls back to a tail slice. On #10486 (galois_lean, 537 + # declarations) the tail was twenty healthy verdicts and the + # cause sat near the top, invisible. + anomalies = axiom_lookup_anomalies(result.get("raw_output") or "") + if anomalies: + print(f" | non-verdict lines in raw_output ({len(anomalies)} shown):") + for line in anomalies: + print(f" | {line}") + else: + print(" | (no non-verdict lines -- raw_output is all healthy" + " axioms verdicts; failure left no trace in this capture)") + if result["has_sorry"]: + sorry_modules.append(mod) + + module_ok = result["success"] + + # Discriminate the two causes of a zero enumeration (ai-01 c.84, + # #9446 CHANGES_REQUESTED). `lean_server.check_axioms` already + # classifies the empty case via `empty_reason` + # (`_classify_empty_enumeration`); only `declaration_free_module` + # is a pass -- every other reason (source_not_found, + # all_private_declarations, sorry_without_declaration, + # no_declarations_enumerated) is a gap where the gate inspected + # nothing and MUST fail loud, independently of the sorry policy + # (that is why we assert here and not only inside `check_axioms`: + # `fail_on_sorry` doubles as the "no declarations" guard there, so a + # false would otherwise silence a parse gap and yield a gate that + # can never go red). The previous `n_decls == 0 -> FAIL` conflated + # the two and red-flagged root aggregators (Grothendieck, + # .DirectImage, .MathlibMap, .SchemesTour) that the lake built and + # parsed clean but legitimately declare nothing. Vacuity moves to + # lake level (below) so a lake whose EVERY module is zero-decl is + # still caught without an exclusion list (ai-01: a list rots and + # does not scale to 20 lakes). + empty_reason = result.get("empty_reason") + if n_decls == 0 and empty_reason != "declaration_free_module": + module_ok = False + print(f" FAIL: no declarations enumerated -- source gap " + f"(empty_reason={empty_reason})") + elif n_decls == 0: + zero_decl_design.append(mod) + print(f" NOTE: declaration-free by design " + f"(empty_reason={empty_reason}) -- non-fatal; " + f"vacuity guarded at lake level") + + if not module_ok: + all_clean = False + print(f" FAIL") + else: + print(f" OK") + + # Gesture 2 (ai-01 c.84): non-vacuity at LAKE level. A gate whose + # every module enumerated zero declarations inspected nothing. Asserting + # this once at lake level catches that without false-positiving on + # individual root aggregators (handled above via empty_reason). Neutre + # for lean-knot.yml / lean-conway.yml: none of their target modules + # enumerate zero. + if total_enumerated == 0: + all_clean = False + print(f"FAIL: lake-level non-vacuity -- all {len(modules)} " + f"module(s) enumerated zero declarations (the gate inspected " + f"nothing; check target-modules / module resolution).") + + print() + if zero_decl_design: + print(f"NOTE: {len(zero_decl_design)} module(s) declaration-free by " + f"design (non-fatal): {', '.join(zero_decl_design)}") + if sorry_modules and not fail_on_sorry: + print(f"NOTE: sorry present in {', '.join(sorry_modules)} " + f"(reported, not gated -- fail-on-sorry is false for this lake).") + if all_clean: + print("OK: no forbidden axioms" + + (" (sorryAx caught transitively if any)." if fail_on_sorry else ".")) + else: + # Say what actually failed. A fixed "forbidden axioms detected." + # line is a lie whenever the cause was a build/lookup error, and a + # gate that misreports its own cause is worse than no gate. + print("FAIL: see per-module breakdown above " + "(`error:` for build/lookup failures, " + "`empty_reason` != declaration_free_module for a source gap, " + "lake-level non-vacuity if every module enumerated zero, " + "`forbidden:` for axiom violations" + + (", `has_sorry:` for sorryAx)." if fail_on_sorry else ").")) + sys.exit(1) + PY diff --git a/.github/actions/lean-build/action.yml b/.github/actions/lean-build/action.yml new file mode 100644 index 0000000000..3956144f4b --- /dev/null +++ b/.github/actions/lean-build/action.yml @@ -0,0 +1,180 @@ +name: 'Lean build + sorry gate' +description: > + Composite-action twin of .github/workflows/lean-build.yml (reusable), for + callers routed to the specialised self-hosted Lean pool (#14337 tranche 2a, + arbitrage (B) composite action, ai-01 DM msg-20260904T132737-02hnpi). Same + steps, same sorry-filter semantics, same bidirectional baseline gate. The + reusable stays the caller of record for the 25 unrouted lakes until 2b. + +inputs: + project-path: + description: 'Repo-relative path to the lake project root' + required: true + display-name: + description: 'Human-readable project name (for job labels)' + required: true + sorry-baseline: + description: 'Current real sorry count (must EXACTLY match the counter; bidirectional gate fails above AND below)' + required: true + sorry-filter-mode: + description: 'How to count sorry: raw | prose-header | standalone-tactic | real' + required: true + +runs: + using: composite + steps: + # NOTE (composite vs reusable): the CALLER job carries `actions/checkout` + # before this action -- a local composite (`./.github/actions/...`) can + # only resolve after the repository is materialised in the workspace. + - name: Sorry check (${{ inputs.display-name }}) + shell: bash + working-directory: ${{ inputs.project-path }} + run: | + set -eu + MODE="${{ inputs.sorry-filter-mode }}" + BASELINE="${{ inputs.sorry-baseline }}" + echo "=== Sorry inventory for ${{ inputs.display-name }} (mode: $MODE, baseline: $BASELINE) ===" + SORRY_TOTAL=0 + # Exclude i18n English siblings `*_en.lean` from the sorry scan: they are + # byte-identical mirrors of their FR counterpart (only docstrings/comments + # differ, and `real` mode strips comments before counting), so their sorries + # are DUPLICATES of the FR file's, not new debt. Counting both double-inflates + # the total above baseline (e.g. knot_lean: Reidemeister.lean(2) + + # Reidemeister_en.lean(2) => 19 > baseline 17, a false FAIL — C513-L1, #6429). + # FR<->EN body divergence is caught separately by the dedicated job + # `.github/workflows/lean-i18n-drift.yml` (#10007), which invokes + # `scripts/lean/check_i18n_siblings.py --all` and FAILs on real drift / + # orphan / non-whitelisted unbuilt. The exemption list lives there, + # NAMED (PetersTour_en, #7081 INTRINSIC). This exclusion only ever LOWERS + # a count here, never breaks a green lake. + for f in $(find . -name '*.lean' ! -name '*_en.lean' -not -path './.lake/*'); do + if [ -f "$f" ]; then + case "$MODE" in + raw) + COUNT=$(grep -c "sorry" "$f" || true) ;; + prose-header) + COUNT=$(grep "sorry" "$f" | grep -viE "sorries|sorry.s" | wc -l || true) ;; + standalone-tactic) + # Count `sorry` as the sole tactic on a line, INCLUDING the + # Lean case-bullet form `· sorry` (U+00B7). The bare + # `^\s*sorry\s*$` regex MISSED it, so a bullet-sorry reported + # delta 0 and silently passed the anti-regression gate (blind + # spot, See #2747). Strip bullet bytes (c2 b7) first so BOTH + # forms match in any locale (byte-exact, not UTF-8 dependent). + COUNT=$(tr -d '\302\267' < "$f" | grep -cE "^\s*sorry\s*$" || true) ;; + real) + # Strip Lean line comments (-- ...) and nested block comments + # (/- ... -/) then count word-bounded `sorry`. Mirrors the + # prover harness `count_real_sorries` (FX-6 #1453), the repo's + # canonical counter. Catches every compiled-tactic form + # (`exact sorry`, `:= by sorry`, bare `sorry`, `sorry -- c`) + # while ignoring prose mentions in docstrings/comments. Use + # when docstring prose legitimately says "sorry" so comment + # edits do not flip the raw count (See #5120). + COUNT=$(awk ' + BEGIN { depth=0 } + { + line=$0; out=""; i=1; n=length(line) + while (i<=n) { + two = (i0 && two=="-/") { depth--; i+=2; continue } + if (depth==0) { out = out substr(line,i,1) } + i++ + } + if (depth==0) print out + } + ' "$f" | grep -oE '\bsorry\b' | wc -l || true) ;; + *) + echo "ERROR: unknown sorry-filter-mode '$MODE'"; exit 2 ;; + esac + if [ "${COUNT:-0}" -gt 0 ]; then + echo " $f: $COUNT" + SORRY_TOTAL=$((SORRY_TOTAL + COUNT)) + fi + fi + done + echo "" + echo "Real sorry ($MODE): $SORRY_TOTAL" + echo "Known baseline: $BASELINE" + if [ "$SORRY_TOTAL" -gt "$BASELINE" ]; then + echo "" + echo "FAIL: sorry count ($SORRY_TOTAL) exceeds baseline ($BASELINE)" + echo "A sorry-as-tactic was introduced. If intentional (new intractable/" + echo "scaffolding target), raise sorry-baseline in the caller workflow WITH" + echo "a documented justification in the PR body." + exit 1 + elif [ "$SORRY_TOTAL" -lt "$BASELINE" ]; then + # Bidirectional enforcement (anti-regression §D, See #8853/#8856). + # The gate previously only failed on above-baseline regressions; a + # discharged sorry (real count drops) left the baseline stale with no + # signal, so the NEXT regression above the stale floor passed silently. + # A baseline must track the real count exactly. Real < baseline means + # the caller workflow's sorry-baseline is stale — decrement it here. + echo "" + echo "FAIL: sorry count ($SORRY_TOTAL) is BELOW baseline ($BASELINE)." + echo "A sorry was discharged (or the counter scope changed) but the" + echo "sorry-baseline in the caller workflow was not decremented to match." + echo "A stale baseline hides the next regression — the gate only flags" + echo "above-baseline. Decrement sorry-baseline to $SORRY_TOTAL in the" + echo "caller workflow, in this same PR (anti-regression §D, #8853/#8856)." + exit 1 + fi + echo "OK: sorry count matches baseline exactly ($SORRY_TOTAL == $BASELINE)." + + - name: Install elan + shell: bash + run: | + curl -sSfL https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz + ./elan-init -y --default-toolchain none + echo "$HOME/.elan/bin" >> $GITHUB_PATH + + - name: Cache Lake build artifacts + uses: actions/cache@v4 + with: + path: ${{ inputs.project-path }}/.lake + key: lake-${{ inputs.display-name }}-${{ runner.os }}-${{ hashFiles(format('{0}/lakefile.lean', inputs.project-path), format('{0}/lakefile.toml', inputs.project-path), format('{0}/lean-toolchain', inputs.project-path)) }} + restore-keys: lake-${{ inputs.display-name }}-${{ runner.os }}- + + # Hosted leg only (#14337 tranche 2a): the specialised Lean pool carries + # its swap OUTSIDE the job (cgroup `--memory-swap 24g`, supervise.sh + # cmd_lean) precisely because a job container has no sudo to fallocate. + # On github-hosted the 32 G swap stays the OOM guard for a cache-miss + # elaboration peak (history: PR #9798/#9840, see the long note that used + # to live in lean-build.yml — now in the reusable, same wording). + - name: Add swap space (hosted only) + if: runner.environment == 'github-hosted' + shell: bash + run: | + df -h /mnt + sudo fallocate -l 32G /mnt/lean-swap + sudo chmod 600 /mnt/lean-swap + sudo mkswap /mnt/lean-swap + sudo swapon /mnt/lean-swap + free -h + + - name: Lake build + shell: bash + working-directory: ${{ inputs.project-path }} + run: | + set -o pipefail # propagate lake's exit code through the pipeline — without this a + # FAILED lake build reports exit 0 (tail always succeeds), and the + # CI step passes regardless. See incident conway_lean HashlifeCorrectness + # L1058 (rfl fail masked as CI PASS, 2026-06-14). + lake exe cache get || true + # `tail` keeps the SUCCESS path terse, but on FAILURE it also truncates the + # `File.lean:L:C: error:` line — lake builds in parallel and pushes an early + # failure ~8000 lines out of the tail window (See #8915). Tee the full log so + # the error lines can be surfaced in a ::group:: on failure. `if cmd;` exempts + # the pipeline from errexit, but pipefail still feeds `$?` here — this is what + # preserves the 2026-06-14 invariant (FAILED build still exits != 0). + if lake -R build 2>&1 | tee "$RUNNER_TEMP/lake.log" | tail -20; then + : + else + rc=$? + echo "::group::Error lines from the full lake log (See #8915)" + grep -nE "^error:|\.lean:[0-9]+:[0-9]+: (error|warning)" "$RUNNER_TEMP/lake.log" | head -100 || true + echo "::endgroup::" + exit "$rc" + fi diff --git a/.github/workflows/lean-knot.yml b/.github/workflows/lean-knot.yml index ed07fd6303..1f3b53adc0 100644 --- a/.github/workflows/lean-knot.yml +++ b/.github/workflows/lean-knot.yml @@ -74,6 +74,10 @@ on: - '.github/workflows/lean-knot.yml' - '.github/workflows/lean-axiom.yml' - '.github/workflows/lean-build.yml' + # Self-cover des composites consommes par les jobs routes (#14337 2a) : + # le gate doit tourner quand son propre code change (lecon #8712). + - '.github/actions/lean-build/action.yml' + - '.github/actions/lean-axiom/action.yml' # ...and the gate is not only its YAML. The axiom step is a Python # program whose whole body is `from lean_server import LeanVerifier`, # so lean_server.py (and the helper it loads) ARE gate inputs. Omitting @@ -96,6 +100,8 @@ on: - '.github/workflows/lean-knot.yml' - '.github/workflows/lean-axiom.yml' - '.github/workflows/lean-build.yml' + - '.github/actions/lean-build/action.yml' + - '.github/actions/lean-axiom/action.yml' - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/lean_server.py' - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/lean_utils.py' - 'scripts/lean/check_target_coverage.py' @@ -109,13 +115,31 @@ concurrency: cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: + # Routage #14337 tranche 2a (arbitrage (B) composite action, ai-01 DM + # 2026-09-04 msg-20260904T132737-02hnpi) : jambe Lean auto-hébergée sur le + # pool coursia-lean (image Dockerfile.lean = elan + toolchain pré-cuits, + # volume .lake chaud par slot #14285). Le `if:` ci-dessous est la garde + # anti-fork exigée par scripts/ci/check_self_hosted_runner_policy.py ; un + # `runs-on` STATIQUE la rend auditable (une expression dynamique lève + # DYNAMIC_RUNS_ON). Les PRs de fork sautent le job -- pr_gate.py compte + # `skipped` comme OK (le code d'un fork ne tourne jamais sur le pool). + # Le twin composite-action (.github/actions/lean-build/action.yml) porte + # les steps ; le checkout vit ICI car une action locale ne se résout + # qu'une fois le dépôt materialisé dans le workspace. + # Retour arrière = remettre `uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main` + # avec ses `with:` + retirer runs-on/if/steps du job. ci: - uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main - with: - project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean - display-name: knot_lean - sorry-baseline: "11" - sorry-filter-mode: real + name: "Lean CI (knot_lean)" + runs-on: [self-hosted, coursia-ephemeral, coursia-lean] + if: github.event.pull_request.head.repo.full_name == null || github.event.pull_request.head.repo.full_name == github.repository + steps: + - uses: actions/checkout@v4 + - uses: ./.github/actions/lean-build + with: + project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean + display-name: knot_lean + sorry-baseline: "11" + sorry-filter-mode: real # Level 3 proof-integrity gate (criterion B.3 of pr-review-discipline). # Closes #8677: catches forbidden axioms (incl. transitive `sorryAx`) @@ -123,24 +147,28 @@ jobs: # reuse the cached lake artifacts. # Opt-in per lake; knot_lean is the pilote because it has a stable # sorry profile (16 real tactic sorries, all enumerated + justified). - # NOTE: `uses: ./...` (not `@main`) -- `lean-axiom.yml` is introduced by - # THIS PR; resolving it from `main` would mean the pilot job silently - # fails to dispatch on the branch and never proves the gate works. - # Once the workflow lands on `main`, future lakes can either keep `./` - # (resolved per-PR) or switch to `@main` (resolved once). + # #14337 tranche 2a: routed to the coursia-lean pool via the composite + # twin (.github/actions/lean-axiom) -- job-level `uses:` on the local + # reusable replaced by a LOCAL job (runs-on/if/steps) invoking the + # composite. check_target_coverage.py unions BOTH wiring forms. proof-integrity: - uses: ./.github/workflows/lean-axiom.yml - with: - project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean - display-name: knot_lean - target-modules: "*" - allow-axioms: "" - # 11 acknowledged tactic `sorry`s = the `sorry-baseline` declared by the - # build job above; the gate tolerates them (`fail-on-sorry: false`) but - # still reports `has_sorry` per module and hard-fails forbidden axioms. - # The per-module enumeration now lives in the gate's runtime derivation - # (issue #10889) -- flip to `true` when the baseline reaches 0. - fail-on-sorry: false + name: "Proof integrity (knot_lean)" + runs-on: [self-hosted, coursia-ephemeral, coursia-lean] + if: github.event.pull_request.head.repo.full_name == null || github.event.pull_request.head.repo.full_name == github.repository + steps: + - uses: actions/checkout@v4 + - uses: ./.github/actions/lean-axiom + with: + project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean + display-name: knot_lean + target-modules: "*" + allow-axioms: "" + # 11 acknowledged tactic `sorry`s = the `sorry-baseline` declared by the + # build job above; the gate tolerates them (`fail-on-sorry: false`) but + # still reports `has_sorry` per module and hard-fails forbidden axioms. + # The per-module enumeration now lives in the gate's runtime derivation + # (issue #10889) -- flip to `true` when the baseline reaches 0. + fail-on-sorry: false # Advisory proof-integrity coverage (See #8782). Same pattern as conway_lean # (#8787): the `target-modules` list above is hand-maintained while the diff --git a/scripts/ci/docker/linux-runner/supervise.sh b/scripts/ci/docker/linux-runner/supervise.sh index a1d22aed97..3166ce3b95 100644 --- a/scripts/ci/docker/linux-runner/supervise.sh +++ b/scripts/ci/docker/linux-runner/supervise.sh @@ -277,6 +277,7 @@ cmd_stop() { echo "sentinel pose : aucun nouveau conteneur ne sera lance." echo "Les jobs en cours vont a leur terme. Pour couper net (deconseille) :" echo " docker ps --filter name=$NAME_PREFIX -q | xargs -r docker kill" + echo " docker ps --filter name=$LEAN_NAME_PREFIX -q | xargs -r docker kill" } cmd_status() { @@ -398,6 +399,15 @@ cmd_lean() { [ -f "$STOP_FILE" ] && die "sentinel STOP pose -- arreter d'abord ($0 stop)" # Idempotence calquee sur cmd_waiters : le garde PPID de `start` filtre # `supervise.sh start` et ne verrait pas `lean`. Verrou par pid file. + # + # Budget CPU hors garde (a documenter, ai-01 DM 2026-09-04) : le garde PPID + # ne couvre que les superviseurs d'un MEME prefix, donc `start` et `lean` + # coexistent par design (familles distinctes, containers distincts). La + # somme des caps CPU des familles actives n'est gardee par RIEN -- c'est + # l'operateur qui dimensionne : slots generiques (N x CPUS) + waiters + # (N x WAITER_CPUS) + slots lean (N x LEAN_CPUS) doit rester <= le total + # machine. Le pool lean est dimensionne pour tourner SEUL sur la jambe CI + # lourde (arret des autres familles avant `lean` quand la machine sature). if [ -f "$STATE_DIR/lean-pids" ]; then local head_pid head_pid="$(head -1 "$STATE_DIR/lean-pids" 2>/dev/null || true)" diff --git a/scripts/lean/check_target_coverage.py b/scripts/lean/check_target_coverage.py index 09e3092094..aca0cc0926 100644 --- a/scripts/lean/check_target_coverage.py +++ b/scripts/lean/check_target_coverage.py @@ -150,9 +150,41 @@ def _uses_lean_axiom(uses: str) -> bool: return ref.rsplit("/", 1)[-1] == "lean-axiom.yml" +# Composite-action routing form (#14337 tranche 2a): the gate job is LOCAL +# (carries runs-on/if/steps) and invokes the composite twin of the reusable. +# The step-level ``with:`` holds the same inputs; without this companion form +# the union below silently drops every routed gate job and the advisory +# reports the modules the gate inspects as blind spots. +_COMPOSITE_LEAN_AXIOM_REFS = { + "./.github/actions/lean-axiom", + ".github/actions/lean-axiom", +} + + +def _composite_lean_axiom_targets(job: dict) -> set[str]: + """Union ``with.target-modules`` over the job's lean-axiom composite steps.""" + mods: set[str] = set() + for step in job.get("steps") or []: + if not isinstance(step, dict): + continue + uses = step.get("uses", "") + if not isinstance(uses, str): + continue + ref = uses.split("@", 1)[0].strip() + if ref not in _COMPOSITE_LEAN_AXIOM_REFS: + continue + raw = (step.get("with") or {}).get("target-modules", "") + mods |= parse_target_modules(str(raw)) + return mods + + def targets_from_workflow(workflow_path: Path) -> tuple[set[str], dict[str, set[str]]]: """Union ``with.target-modules`` over every lean-axiom job in a workflow. + Both wiring forms are unioned: a job-level ``uses:`` on the reusable + ``lean-axiom.yml``, and a local job's step-level ``uses:`` on the composite + ``.github/actions/lean-axiom`` (#14337 tranche 2a routing). + Returns ``(union, per_job)``. An **empty** ``per_job`` means no job in the file calls ``lean-axiom.yml`` -- reported by the caller as an explicit "no gate wired" line, never folded into a 0%-coverage figure: those two @@ -166,12 +198,17 @@ def targets_from_workflow(workflow_path: Path) -> tuple[set[str], dict[str, set[ per_job: dict[str, set[str]] = {} for job_id, job in jobs.items(): - if not isinstance(job, dict) or not _uses_lean_axiom(job.get("uses", "")): + if not isinstance(job, dict): + continue + if _uses_lean_axiom(job.get("uses", "")): + raw = (job.get("with") or {}).get("target-modules", "") + # A gate job with an empty target list is still a gate job: record it so + # the report shows it contributed nothing, rather than hiding it. + per_job[str(job_id)] = parse_target_modules(str(raw)) continue - raw = (job.get("with") or {}).get("target-modules", "") - # A gate job with an empty target list is still a gate job: record it so - # the report shows it contributed nothing, rather than hiding it. - per_job[str(job_id)] = parse_target_modules(str(raw)) + composite_mods = _composite_lean_axiom_targets(job) + if composite_mods: + per_job[str(job_id)] = composite_mods union: set[str] = set() for mods in per_job.values(): diff --git a/scripts/lean/tests/test_check_target_coverage.py b/scripts/lean/tests/test_check_target_coverage.py index 911b341291..5752d7a9ad 100644 --- a/scripts/lean/tests/test_check_target_coverage.py +++ b/scripts/lean/tests/test_check_target_coverage.py @@ -11,7 +11,9 @@ - lib-root scoping (``/`` subdir + ``.lean`` umbrella + ``_en.lean`` sibling); - maximal walk excludes build cache / lakefile / toolchain; - ``--from-workflow`` unions the target list over every gate job, so the report - cannot hold a stale copy of it (#8782); + cannot hold a stale copy of it (#8782), across BOTH wiring forms: job-level + ``uses:`` on the reusable lean-axiom.yml AND step-level ``uses:`` on the + composite twin ``.github/actions/lean-axiom`` (#14337 tranche 2a routing); - ``target-modules: "*"`` (issue #10889) is a runtime-derivation directive: the gate walks the lake itself (``discover_modules``) and drops ``_en`` i18n siblings by default (``filter_i18n_siblings``), so every compiled module is @@ -361,6 +363,95 @@ def test_a_source_is_required(self, tmp_path): main(["--project-path", str(lake)]) +# --------------------------------------------------------------------------- +# Composite-action routing (#14337 tranche 2a) -- step-level `uses:` on the +# local composite twin. Without this companion form the union silently drops +# every routed gate job and the advisory reports the modules the gate DOES +# inspect as blind spots -- the exact inverse of its job. +# --------------------------------------------------------------------------- + +class TestCompositeRouting: + def _composite_wf(self, tmp_path: Path, target: str) -> Path: + return _write_workflow(tmp_path, f""" +jobs: + proof-integrity: + runs-on: [self-hosted, coursia-ephemeral, coursia-lean] + steps: + - uses: actions/checkout@v4 + - uses: ./.github/actions/lean-build + with: + project-path: fake_lake + - uses: ./.github/actions/lean-axiom + with: + project-path: fake_lake + target-modules: "{target}" + fail-on-sorry: true +""") + + def test_composite_step_is_unioned(self, tmp_path): + wf = self._composite_wf(tmp_path, "Knots.Basic,Knots.Invariant") + union, per_job = targets_from_workflow(wf) + assert union == {"Knots.Basic", "Knots.Invariant"} + assert per_job == {"proof-integrity": {"Knots.Basic", "Knots.Invariant"}} + + def test_composite_star_directive_is_unioned(self, tmp_path): + # the knot pilote's routed form: runtime derivation via "*" + wf = self._composite_wf(tmp_path, "*") + union, per_job = targets_from_workflow(wf) + assert union == {"*"} + assert per_job == {"proof-integrity": {"*"}} + + def test_composite_bare_ref_form_matches(self, tmp_path): + # same action referenced without the leading "./" -- both are in + # _COMPOSITE_LEAN_AXIOM_REFS, and a regression to a single form + # would silently un-see the other. + wf = _write_workflow(tmp_path, """ +jobs: + gate: + steps: + - uses: .github/actions/lean-axiom + with: + target-modules: "Conway.KochenSpecker" +""") + union, _ = targets_from_workflow(wf) + assert union == {"Conway.KochenSpecker"} + + def test_lean_build_composite_step_is_not_a_gate(self, tmp_path): + # the lean-BUILD composite carries no target-modules; a job that only + # builds must not appear in per_job (only lean-axiom is the gate). + wf = _write_workflow(tmp_path, """ +jobs: + ci: + steps: + - uses: ./.github/actions/lean-build + with: + project-path: fake_lake +""") + union, per_job = targets_from_workflow(wf) + assert union == set() + assert per_job == {} + + def test_composite_and_reusable_mixed_union(self, tmp_path): + # during the 2a/2b transition the repo holds BOTH wiring forms + # (pilotes routed, 25 lakes still on the reusable); the union must + # carry both without one hiding the other. + wf = _write_workflow(tmp_path, """ +jobs: + routed-gate: + steps: + - uses: ./.github/actions/lean-axiom + with: + target-modules: "Conway.KochenSpecker" + reusable-gate: + uses: ./.github/workflows/lean-axiom.yml + with: + target-modules: "Knots.Basic" +""") + union, per_job = targets_from_workflow(wf) + assert union == {"Conway.KochenSpecker", "Knots.Basic"} + assert set(per_job) == {"routed-gate", "reusable-gate"} + + # --------------------------------------------------------------------------- # Runtime derivation (issue #10889) -- `target-modules: "*"` # ---------------------------------------------------------------------------