diff --git a/.github/workflows/lean-ci-matrix.yml b/.github/workflows/lean-ci-matrix.yml index 780f071ee8..e91a0f9c7c 100644 --- a/.github/workflows/lean-ci-matrix.yml +++ b/.github/workflows/lean-ci-matrix.yml @@ -92,6 +92,22 @@ on: - 'MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.lean' - 'MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.toml' - 'MyIA.AI.Notebooks/ML/learning_theory_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/**.lean' + - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/**.lean' + - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/**.lean' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.lean' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.toml' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lean-toolchain' + - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/**.lean' + - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean' + - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.toml' + - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lean-toolchain' # self-cover du gate (#8712) : un changement du gate lance le gate - '.github/workflows/lean-ci-matrix.yml' - '.github/workflows/lean-build.yml' @@ -160,6 +176,22 @@ on: - 'MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.lean' - 'MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.toml' - 'MyIA.AI.Notebooks/ML/learning_theory_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/**.lean' + - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/**.lean' + - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/**.lean' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.lean' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.toml' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lean-toolchain' + - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/**.lean' + - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean' + - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.toml' + - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lean-toolchain' - '.github/workflows/lean-ci-matrix.yml' - '.github/workflows/lean-build.yml' - '.github/actions/lean-build/action.yml' diff --git a/.github/workflows/lean-decision-theory.yml b/.github/workflows/lean-decision-theory.yml deleted file mode 100644 index 875a56ea76..0000000000 --- a/.github/workflows/lean-decision-theory.yml +++ /dev/null @@ -1,83 +0,0 @@ -name: Lean CI (decision_theory_lean) - -# CI for decision_theory_lean (Probas/decision_theory_lean) — decision-theory lake -# at the Probas series root, lifted from Probas/Infer/gittins_lean in PR #4058 -# (lake content unchanged by the lift). First module: Gittins index. Research scaffolding. -# -# sorry-filter-mode=real, baseline=2: regression floor matching what -# the CI counter actually reports. lean-build.yml counts FR files only -# (`find ! -name '*_en.lean'`), so the EN siblings are OUT of the gate's scope. -# GittinsTheorem.lean (FR) carries 2 standalone `sorry` (gittins_optimality, the -# value V := sorry and the inequality proof sorry, both INTRINSIC #4039 MDP -# barrier) — and 2 is ALSO the `real`-mode count (no inline `exact sorry` -# forms), so standalone-tactic did not undercount here. The EN sibling -# GittinsTheorem_en.lean mirrors them 1:1 (i18n #4980 byte-identical proofs) -# but, being `_en`, is never scanned — its parity with FR is enforced by -# the i18n convention, not by this gate. -# -# `real` mode is the prover harness canonical count (FX-6 #1453): -# depth-tracked `/-- ... -/` and `/- ... -/` strip, then word-bounded -# `\bsorry\b` grep. Catches every compiled-tactic form (`:= by sorry`, -# `exact sorry`, bare `sorry`, case-bullet `· sorry`) while ignoring -# prose mentions in docstrings/comments. The discount sub-module -# (Discount.lean, 0 since #2911) is EN-sibling-clean; the 2 baseline -# captures the INTRINSIC gittins_optimality barrier honestly. -# -# Was baseline=4: that value counted FR(2)+EN(2), but the counter excludes -# `_en`, so the EN half was never seen — a scope mismatch that left the -# floor 2 above the real count (Discount.lean, also 0 since #2911, compounded -# it). A floor 2 above real defeats the §D anti-regression gate: a 2-sorry -# regression (2->4) would pass undetected (CI run 29857938621 already reports -# "Real sorry (standalone-tactic): 2 / Known baseline: 4"). Corrected to 2 -# so the gate is sensitive again. Consolidated per ai-01 DRY decision. -# the CI counter actually reports. lean-build.yml counts FR files only -# (`find ! -name '*_en.lean'`), so the EN siblings are OUT of the gate's scope. -# GittinsTheorem.lean (FR) carries 2 standalone `sorry` (gittins_optimality, the -# value V := sorry and the inequality proof sorry, both INTRINSIC #4039 MDP -# barrier) — and 2 is ALSO the `real`-mode count (no inline `exact sorry` forms), -# so standalone-tactic does not undercount here. The EN sibling -# GittinsTheorem_en.lean mirrors them 1:1 (i18n #4980 byte-identical proofs) but, -# being `_en`, is never scanned — its parity with FR is enforced by the i18n -# convention, not by this gate. -# -# Was baseline=4: that value counted FR(2)+EN(2), but the counter excludes `_en`, -# so the EN half was never seen — a scope mismatch that left the floor 2 above -# the real count (Discount.lean, also 0 since #2911, compounded it). A floor 2 -# above real defeats the §D anti-regression gate: a 2-sorry regression (2->4) -# would pass undetected (CI run 29857938621 already reports "Real sorry -# (standalone-tactic): 2 / Known baseline: 4"). Corrected to 2 so the gate is -# sensitive again. Consolidated per ai-01 DRY decision (matrix). See lean-build.yml. - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/**.lean' - - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lean-toolchain' - pull_request: - types: [opened, synchronize, edited, reopened] - branches: [main] - paths: - - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/**.lean' - - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/Probas/decision_theory_lean/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-decision-theory-${{ github.ref }} - cancel-in-progress: ${{ github.event_name == 'pull_request' }} - -jobs: - ci: - uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main - with: - project-path: MyIA.AI.Notebooks/Probas/decision_theory_lean - display-name: decision_theory_lean - sorry-baseline: "2" - sorry-filter-mode: real diff --git a/.github/workflows/lean-game-theory.yml b/.github/workflows/lean-game-theory.yml deleted file mode 100644 index 581f039ec1..0000000000 --- a/.github/workflows/lean-game-theory.yml +++ /dev/null @@ -1,96 +0,0 @@ -name: Lean Game Theory CI - -# CI for game_theory_lean (multi-module lake: SocialChoice + StableMarriage + -# CooperativeGames + RepeatedGames, EPIC #4365). The legacy cooperative_games_lean -# and stable_marriage_lean lakes were absorbed into game_theory_lean (#4362/#4365). -# -# Migrated to the shared lean-build.yml reusable workflow (See #8947), like -# conway / grothendieck / calibration. It replaces THREE hand-rolled bash gates -# (check-sorry-stable-marriage + check-sorry-cooperative-games here, and -# check-sorry-repeated-games in the now-deleted lean-repeated-games.yml) whose -# hardcoded file lists scanned 10 of the lake's 26 FR modules. SocialChoice/ -# (8 modules, including Arrow.lean and Sen.lean) was covered by NOTHING -- the -# very file whose #524 regression (9 proofs replaced by `sorry`, one week of -# Lean port lost, restored by #527) founded the anti-regression rule §D. -# `find .` in the reusable workflow scans all 26. -# -# Sorry profile (measured 2026-07-30 on 27ddbfae6, mode `real`, baseline 1): -# RepeatedGames/Folk.lean : 1 -- the authentic hard direction of the folk -# theorem (convexity + extreme-point -# machinery), tolerated stretch per #4880 -# every other FR module : 0 -# -# Mode `real` (not `raw`): the legacy gates' baselines (5 + 1 + 10 = 16) counted -# the WORD "sorry" in FR/EN prose. `raw` over the same FR file set returns 17 for -# this lake, of which 16 are docstring mentions ("plusieurs lemmes portent un -# `sorry`", "ses sorries comptés", ...). Two consequences it had: a docs-only PR -# that wrote the word reddened the gate, and rewording a docstring to drop it -# freed a slot for a genuine sorry. `real` strips Lean comments (-- and nested -# /- -/) before counting \bsorry\b -- mirror of the prover harness -# count_real_sorries (FX-6 #1453), See #5120. -# -# The baseline is BIDIRECTIONAL (#8853/#8856): it must EXACTLY equal the -# counter's output, so the gate fails above (a sorry was introduced) AND below -# (a sorry was discharged without decrementing -- a stale floor hides the next -# regression). This is precisely what the legacy gates could not do: -# RepeatedGames counted 5 against a baseline of 10 and slept green on 5 units of -# phantom headroom. When Folk's sorry is discharged, set sorry-baseline to "0" -# in the same PR. -# -# `*_en.lean` siblings are excluded by the reusable workflow: under the i18n -# convention (code-style.md, signatures and proofs byte-identical, only -# docstrings differ) Folk_en.lean's sorry is the SAME obligation as Folk.lean's, -# not new debt -- counting both double-inflates past baseline (C513-L1, #6429). -# FR<->EN divergence is caught separately by the i18n drift CI, so nothing hides. -# -# Lake build: the reusable runs `lake exe cache get || true` then `lake -R build`, -# which builds every @[default_target] of the lakefile -- SocialChoice, -# StableMarriage, CooperativeGames, RepeatedGames and their _en siblings. The -# deleted lean-repeated-games.yml ran `lake build RepeatedGames` (a strict -# subset) WITHOUT `cache get`, so it recompiled Mathlib from source: on #8946 it -# was still running after 50 minutes while this build finished in 3 min 50 s. -# -# Preserved from the deleted lean-repeated-games.yml (EPIC #4365 Phase-4, PR -# c.371, po-2023), so the intent is not lost with the file: RepeatedGames was -# absorbed into `game_theory_lean/RepeatedGames/` (its canonical home) and the -# old `repeated_games_lean/` lake stays archived (docs + lakefile + manifest, -# no @[default_target] pointing at it). Its certification intent -- Stage, -# Discounting and GrimTrigger at 0 sorry, `grim_trigger_sustains_iff` proved -- -# is now enforced lake-wide by the single baseline below: any sorry appearing in -# those modules pushes the count above 1 and fails. - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/**.lean' - - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lean-toolchain' - - '.github/workflows/lean-game-theory.yml' - pull_request: - types: [opened, synchronize, edited, reopened] - branches: [main] - paths: - - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/**.lean' - - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lean-toolchain' - - '.github/workflows/lean-game-theory.yml' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-game-theory-${{ github.ref }} - cancel-in-progress: ${{ github.event_name == 'pull_request' }} - -jobs: - ci: - uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main - with: - project-path: MyIA.AI.Notebooks/GameTheory/game_theory_lean - display-name: game_theory_lean - sorry-baseline: "1" - sorry-filter-mode: real diff --git a/.github/workflows/lean-mathlib-examples.yml b/.github/workflows/lean-mathlib-examples.yml deleted file mode 100644 index c57baf4e48..0000000000 --- a/.github/workflows/lean-mathlib-examples.yml +++ /dev/null @@ -1,39 +0,0 @@ -name: Lean CI (mathlib_examples) - -# CI for mathlib_examples (SymbolicAI/Lean/mathlib_examples). -# Mathlib usage examples. 0 sorry (raw=0, verified). Toolchain v4.27.0. -# Consolidated per ai-01 DRY decision (option 2: matrix). See lean-build.yml. - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/**.lean' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.lean' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.toml' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lean-toolchain' - pull_request: - branches: [main] - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/**.lean' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.lean' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.toml' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-mathlib-examples-${{ github.ref }} - cancel-in-progress: ${{ github.event_name == 'pull_request' }} - -jobs: - ci: - uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main - with: - project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples - display-name: mathlib_examples - sorry-baseline: "0" - sorry-filter-mode: real diff --git a/.github/workflows/lean-social-choice-peters.yml b/.github/workflows/lean-social-choice-peters.yml deleted file mode 100644 index 785436fdf3..0000000000 --- a/.github/workflows/lean-social-choice-peters.yml +++ /dev/null @@ -1,39 +0,0 @@ -name: Lean CI (social_choice_lean_peters) - -# CI for social_choice_lean_peters (GameTheory/social_choice_lean_peters). -# Reference port (Peters). 0 sorry (raw=0, verified). Toolchain v4.27.0-rc1. -# Consolidated per ai-01 DRY decision (option 2: matrix). See lean-build.yml. - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/**.lean' - - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean' - - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.toml' - - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lean-toolchain' - pull_request: - branches: [main] - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/**.lean' - - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean' - - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.toml' - - 'MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-social-choice-peters-${{ github.ref }} - cancel-in-progress: ${{ github.event_name == 'pull_request' }} - -jobs: - ci: - uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main - with: - project-path: MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters - display-name: social_choice_lean_peters - sorry-baseline: "0" - sorry-filter-mode: real diff --git a/scripts/lean/ci_lakes.json b/scripts/lean/ci_lakes.json index 5e2eefabca..1d83c89239 100644 --- a/scripts/lean/ci_lakes.json +++ b/scripts/lean/ci_lakes.json @@ -181,6 +181,58 @@ "MyIA.AI.Notebooks/ML/learning_theory_lean/lakefile.toml", "MyIA.AI.Notebooks/ML/learning_theory_lean/lean-toolchain" ] + }, + { + "lake": "decisiontheory", + "project-path": "MyIA.AI.Notebooks/Probas/decision_theory_lean", + "display-name": "decision_theory_lean", + "sorry-baseline": "2", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/Probas/decision_theory_lean/**.lean", + "MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.lean", + "MyIA.AI.Notebooks/Probas/decision_theory_lean/lakefile.toml", + "MyIA.AI.Notebooks/Probas/decision_theory_lean/lean-toolchain" + ] + }, + { + "lake": "gametheory", + "project-path": "MyIA.AI.Notebooks/GameTheory/game_theory_lean", + "display-name": "game_theory_lean", + "sorry-baseline": "1", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/GameTheory/game_theory_lean/**.lean", + "MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean", + "MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.toml", + "MyIA.AI.Notebooks/GameTheory/game_theory_lean/lean-toolchain" + ] + }, + { + "lake": "mathlibexamples", + "project-path": "MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples", + "display-name": "mathlib_examples", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/**.lean", + "MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.lean", + "MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lakefile.toml", + "MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples/lean-toolchain" + ] + }, + { + "lake": "socialchoicepeters", + "project-path": "MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters", + "display-name": "social_choice_lean_peters", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/**.lean", + "MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean", + "MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.toml", + "MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lean-toolchain" + ] } ] }