From 2e9e53e9479aaea596d72af36d09087854a81746 Mon Sep 17 00:00:00 2001 From: jsboige Date: Fri, 18 Sep 2026 17:26:52 +0200 Subject: [PATCH 1/2] =?UTF-8?q?feat(ci,#13751):=20pilote=20matrice=20lean-?= =?UTF-8?q?ci=20=E2=80=94=206=20dispatchers=20fondus=20dans=20lean-ci-matr?= =?UTF-8?q?ix.yml?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - lean-build.yml gagne un mode matrice (input lake-set, job ci-matrix, fromJSON(strategy)) ; job `ci` historique garde par if sentinel 'none' — les callers mono-lake restants ne changent pas. - lean-ci-matrix.yml (nouveau) : detecteur de chemins changes (API REST, sparse-checkout scripts/lean) -> lake-set ; union on.paths push+pr ; ref LOCALE ./ pour resolution per-PR. - scripts/lean/ci_lakes.json : manifeste source unique (lake, project-path, display-name, sorry-baseline bidirectionnel, sorry-filter-mode, paths). - scripts/lean/lake_matrix_dispatch.py : fnmatch pur + self-cover GATE_SELF_COVER -> tous les lakes (lecon #8712). - scripts/ci/check_lake_matrix_paths.py : garde fail-CLOSED (manifeste couvert par push ET pull_request, pas de double declencheur, self-cover vivant sur disque). - 6 dispatchers supprimes : lean-{sudoku,kelly,minimax,search,assignment, discrepancy}.yml — baselines "0"/real et chemins de declenchement verifies identiques contre le depot avant suppression. - 16 tests : selection fnmatch, ordre manifeste, dedup, self-cover par entree, format outputs-file, garde vert sur depot / rouge sur chaque classe de drift. Co-Authored-By: Claude Sonnet 5 --- .github/workflows/lean-assignment.yml | 46 ---- .github/workflows/lean-build.yml | 46 ++++ .github/workflows/lean-ci-matrix.yml | 190 +++++++++++++++++ .github/workflows/lean-discrepancy.yml | 46 ---- .github/workflows/lean-kelly.yml | 48 ----- .github/workflows/lean-minimax.yml | 52 ----- .github/workflows/lean-search.yml | 52 ----- .github/workflows/lean-sudoku.yml | 45 ---- scripts/ci/check_lake_matrix_paths.py | 87 ++++++++ scripts/lean/ci_lakes.json | 83 ++++++++ scripts/lean/lake_matrix_dispatch.py | 94 +++++++++ scripts/tests/test_lake_matrix_dispatch.py | 232 +++++++++++++++++++++ 12 files changed, 732 insertions(+), 289 deletions(-) delete mode 100644 .github/workflows/lean-assignment.yml create mode 100644 .github/workflows/lean-ci-matrix.yml delete mode 100644 .github/workflows/lean-discrepancy.yml delete mode 100644 .github/workflows/lean-kelly.yml delete mode 100644 .github/workflows/lean-minimax.yml delete mode 100644 .github/workflows/lean-search.yml delete mode 100644 .github/workflows/lean-sudoku.yml create mode 100644 scripts/ci/check_lake_matrix_paths.py create mode 100644 scripts/lean/ci_lakes.json create mode 100644 scripts/lean/lake_matrix_dispatch.py create mode 100644 scripts/tests/test_lake_matrix_dispatch.py diff --git a/.github/workflows/lean-assignment.yml b/.github/workflows/lean-assignment.yml deleted file mode 100644 index 0377da4a92..0000000000 --- a/.github/workflows/lean-assignment.yml +++ /dev/null @@ -1,46 +0,0 @@ -name: Lean CI (assignment_lean) - -# CI for assignment_lean (GameTheory/assignment_lean) — assignment problem, -# Kuhn-Munkres Hungarian method correction skeleton (Munkres tribute #12598): -# weak LP duality, zero-gap optimality certificate, equality graph, and the -# Hungarian tightening preserving dual feasibility. Companion lake of the -# notebook GameTheory-23-Munkres-Assignment.ipynb. -# -# sorry-filter-mode=real, baseline=0: the library is fully sorry-free; -# this guards that NO new `sorry` is introduced (never false-positives on -# prose mentions; catches any NEW sorry, including `exact sorry`, -# `theorem foo := by sorry`, `def f : T := sorry`, `<;> sorry`). - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/**.lean' - - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lean-toolchain' - pull_request: - branches: [main] - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/**.lean' - - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-assignment-${{ 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/assignment_lean - display-name: assignment_lean - sorry-baseline: "0" - sorry-filter-mode: real diff --git a/.github/workflows/lean-build.yml b/.github/workflows/lean-build.yml index 03afd4a653..73b918d611 100644 --- a/.github/workflows/lean-build.yml +++ b/.github/workflows/lean-build.yml @@ -62,12 +62,22 @@ on: description: "How to count sorry: raw | prose-header | standalone-tactic | real" type: string required: true + lake-set: + description: "Mode matrice #13751 : JSON {\"include\": [entrees ci_lakes.json]} rendu par scripts/lean/lake_matrix_dispatch.py. Sentinelle 'none' (defaut) -> seul le job `ci` mono-lake tourne. JSON non vide -> seul `ci-matrix` tourne (les 4 inputs ci-dessus sont alors des valeurs de facade ignorees)." + type: string + required: false + default: 'none' permissions: contents: read jobs: + # Mono-lake : comportement historique, inchange pour les ~26 dispatchers + # lean-.yml restants. Le garde `if` n'existe que pour le mode matrice + # (les deux jobs ne tournent jamais ensemble ; un job dont le `if` est faux + # ne cree AUCUN check-run, donc zero bruit pour les callers mono-lake). ci: + if: inputs.lake-set == 'none' name: "Lean CI (${{ inputs.display-name }})" runs-on: ubuntu-latest # BACKSTOP DE LIBERATION DE RUNNER -- PAS UN SEUIL DE SANTE (#15698). @@ -290,3 +300,39 @@ jobs: echo "[lake-heartbeat] still running after ${_elapsed} min - last line: $(tail -1 "$RUNNER_TEMP/lake.log" 2>/dev/null | cut -c1-160)" done wait "$_lake_pipeline" + + # Mode matrice #13751 : fan-out par lake, pilote par lean-ci-matrix.yml. + # Un job appelant (`uses:`) ne peut PAS porter `strategy:` (limite GitHub + # Actions) -- c'est la contrainte qui a produit les 32 dispatchers un + # fichier par lake. La matrice vit donc ICI, dans le workflow appele : + # le caller passe `lake-set` (JSON du manifeste filtre par les chemins + # changes), et ce job l'etale en une entree par lake. + # Le corps du build n'est PAS duplique : le composite jumeau + # .github/actions/lean-build (meme etapes, meme semantique sorry, memes + # cles de cache -- cf son en-tete) porte tout ; ce job n'est que le + # checkout prealable (un composite local ne se resout qu'apres que le + # depot est materialise) + l'appel parametre. + ci-matrix: + if: inputs.lake-set != 'none' + name: "Lean CI (${{ matrix.display-name }})" + runs-on: ubuntu-latest + timeout-minutes: 300 + strategy: + fail-fast: false + matrix: ${{ fromJSON(inputs.lake-set) }} + # Concurrency par lake, pas par workflow : une nouvelle poussee qui + # touche sudoku doit annuler l'encien run sudoku SANS toucher un run + # kelly en cours. Reprend le contrat des anciens dispatchers + # (cancel sur PR, jamais sur push main). + concurrency: + group: lean-matrix-${{ matrix.lake }}-${{ github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + steps: + - uses: actions/checkout@v4 + - name: Build + sorry gate (${{ matrix.display-name }}) + uses: ./.github/actions/lean-build + with: + project-path: ${{ matrix.project-path }} + display-name: ${{ matrix.display-name }} + sorry-baseline: ${{ matrix.sorry-baseline }} + sorry-filter-mode: ${{ matrix.sorry-filter-mode }} diff --git a/.github/workflows/lean-ci-matrix.yml b/.github/workflows/lean-ci-matrix.yml new file mode 100644 index 0000000000..dd92677948 --- /dev/null +++ b/.github/workflows/lean-ci-matrix.yml @@ -0,0 +1,190 @@ +name: Lean CI Matrix + +# Dispatcher matriciel des lakes Lean (#13751, sous-item « 23 workflows +# lean-*.yml -> matrice parametree » ; mesure 2026-09-18 : 32 dispatchers, +# dont 6 migres ici en pilote). +# +# POURQUOI UN DISPATCHER + UNE MATRICE DANS LE REUSABLE. Un job qui APPELLE +# un workflow reutilisable (`uses:`) ne peut pas porter `strategy:` (limite +# GitHub Actions) -- c'est la contrainte qui avait produit un fichier par +# lake. La matrice vit donc dans lean-build.yml (job `ci-matrix`), et ce +# fichier ne fait que : (1) detecter les lakes touches via le manifeste +# scripts/lean/ci_lakes.json, (2) passer l'ensemble au reutilisable. +# +# CONTRAT DE DECLENCHEMENT. `on.paths` ci-dessous est l'UNION des chemins +# des lakes du manifeste + le self-cover du gate. Le garde +# scripts/ci/check_lake_matrix_paths.py verifie que l'union couvre le +# manifeste : ajouter un lake au manifeste SANS l'ajouter ici fait rougir +# le garde (fail-CLOSED) -- un lake non couvert serait un lake que plus +# aucun declencheur ne voit. +# +# SELF-COVER (lecon #8712) : un changement du gate (ce fichier, +# lean-build.yml, le composite, le script de dispatch, le manifeste) lance +# TOUS les lakes du manifeste -- lake_matrix_dispatch.py porte la liste +# GATE_SELF_COVER. +# +# Un lake migre ici en DEUX temps dans la MEME PR : suppression de son +# dispatcher lean-.yml + entree dans ci_lakes.json + chemin dans +# l'union. Jamais les deux declencheurs en meme temps (double build). + +on: + push: + branches: [main] + paths: + # sudoku_lean + - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/**.lean' + - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lean-toolchain' + # kelly_lean + - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/**.lean' + - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lean-toolchain' + # minimax_lean + - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/**.lean' + - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lean-toolchain' + # search_lean + - 'MyIA.AI.Notebooks/Search/search_lean/**.lean' + - 'MyIA.AI.Notebooks/Search/search_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/Search/search_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/Search/search_lean/lean-toolchain' + # assignment_lean + - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/**.lean' + - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lean-toolchain' + # discrepancy_lean + - 'MyIA.AI.Notebooks/Search/discrepancy_lean/**.lean' + - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/Search/discrepancy_lean/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' + - '.github/actions/lean-build/action.yml' + - 'scripts/lean/ci_lakes.json' + - 'scripts/lean/lake_matrix_dispatch.py' + - 'scripts/ci/check_lake_matrix_paths.py' + pull_request: + branches: [main] + types: [opened, synchronize, edited, reopened] + paths: + # UNION identique au push -- le garde check_lake_matrix_paths.py + # verifie les DEUX blocs contre le manifeste. + - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/**.lean' + - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/**.lean' + - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/**.lean' + - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/Search/search_lean/**.lean' + - 'MyIA.AI.Notebooks/Search/search_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/Search/search_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/Search/search_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/**.lean' + - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/GameTheory/assignment_lean/lean-toolchain' + - 'MyIA.AI.Notebooks/Search/discrepancy_lean/**.lean' + - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.toml' + - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lean-toolchain' + - '.github/workflows/lean-ci-matrix.yml' + - '.github/workflows/lean-build.yml' + - '.github/actions/lean-build/action.yml' + - 'scripts/lean/ci_lakes.json' + - 'scripts/lean/lake_matrix_dispatch.py' + - 'scripts/ci/check_lake_matrix_paths.py' + workflow_dispatch: + +permissions: + contents: read + +jobs: + # Detection : quels lakes du manifeste sont touches par l'evenement. + # Les fichiers changes viennent de l'API REST (pull_request : fichiers + # de la PR ; push : compare avant..apres) -- pas d'un checkout profond + # du depot. Sur workflow_dispatch : tous les lakes (le declenchement + # manuel est une intention explicite de tout lancer ; le script y + # arrive par le self-cover). + changes: + name: lean-matrix-changes + runs-on: ubuntu-latest + timeout-minutes: 10 + outputs: + any: ${{ steps.dispatch.outputs.any }} + lake-set: ${{ steps.dispatch.outputs.lake-set }} + env: + GH_TOKEN: ${{ github.token }} + steps: + - name: Changed files for this event + run: | + set -eu + out="$RUNNER_TEMP/changed.txt" + case "${{ github.event_name }}" in + pull_request) + gh api --paginate "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \ + --jq '.[].filename' > "$out" || echo -n "" > "$out" + ;; + push) + before="${{ github.event.before }}" + sha="${{ github.sha }}" + if [ "${before:0:7}" = "0000000" ]; then + # Nouvelle histoire de branche : on ne peut pas differencer -> tout. + echo ".github/workflows/lean-ci-matrix.yml" > "$out" + else + gh api "repos/${{ github.repository }}/compare/${before}...${sha}" \ + --jq '.files[].filename' > "$out" || echo -n "" > "$out" + fi + ;; + workflow_dispatch) + # Self-cover -> tous les lakes du manifeste. + echo ".github/workflows/lean-ci-matrix.yml" > "$out" + ;; + esac + echo "--- changed files (${{ github.event_name }}) ---" + cat "$out" + - name: Checkout (dispatch script + manifest only) + uses: actions/checkout@v4 + with: + sparse-checkout: | + scripts/lean + - name: Dispatch lakes from manifest + id: dispatch + run: | + python scripts/lean/lake_matrix_dispatch.py \ + --changed-file "$RUNNER_TEMP/changed.txt" \ + --outputs-file "$GITHUB_OUTPUT" + echo "--- lake-set ---" + cat "$GITHUB_OUTPUT" + + # Fan-out : passe l'ensemble au reutilisable, qui l'etale en une entree + # par lake (job `ci-matrix` de lean-build.yml). Les 4 inputs mono-lake + # sont des valeurs de facade (required: true au sens du schema) -- en + # mode matrice, `ci` est garde par `if: lake-set == 'none'` et ne tourne + # jamais ; aucun check-run n'est cree pour lui. + lean-matrix: + needs: changes + if: needs.changes.outputs.any == 'true' + # Ref LOCALE `./` (pas `jsboige/CoursIA/...@main`) : la resolution + # per-PR est la condition meme de livrabilite de cette PR -- sur une + # PR de test, `@main` appellerait le lean-build.yml de main, qui n'a + # pas encore l'input `lake-set` (echec d'appel : unknown input). + # Meme pattern que le job proof-integrity de lean-knot.yml (« ref + # locale ./ = resolution per-PR »). + uses: ./.github/workflows/lean-build.yml + with: + project-path: scripts/lean/ci_lakes.json + display-name: matrix + sorry-baseline: "0" + sorry-filter-mode: real + lake-set: ${{ needs.changes.outputs.lake-set }} diff --git a/.github/workflows/lean-discrepancy.yml b/.github/workflows/lean-discrepancy.yml deleted file mode 100644 index a0f2bdb1a5..0000000000 --- a/.github/workflows/lean-discrepancy.yml +++ /dev/null @@ -1,46 +0,0 @@ -name: Lean CI (discrepancy_lean) - -# CI for discrepancy_lean (Search/discrepancy_lean) — combinatorial discrepancy -# lake (Beck-Fiala / Komlós / Bansal-Jiang 2025, arXiv:2508.03961). See #12823. -# P0: definitions + 3 elementary lemmas proven; conjectures live as named -# `def ... : Prop` (never sorry-truncated theorems), so the lake is fully -# sorry-free — baseline 0. -# -# sorry-filter-mode=real, baseline=0: `real` strips `--` and `/- -/` then -# counts `\bsorry\b` word-bordered (catches tactic/block/term `sorry`, never -# false-positives on prose). Baseline 0 = any new sorry fails CI. See -# lean-build.yml. - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/Search/discrepancy_lean/**.lean' - - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lean-toolchain' - pull_request: - branches: [main] - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/Search/discrepancy_lean/**.lean' - - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/Search/discrepancy_lean/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-discrepancy-${{ 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/Search/discrepancy_lean - display-name: discrepancy_lean - sorry-baseline: "0" - sorry-filter-mode: real diff --git a/.github/workflows/lean-kelly.yml b/.github/workflows/lean-kelly.yml deleted file mode 100644 index 566962d05d..0000000000 --- a/.github/workflows/lean-kelly.yml +++ /dev/null @@ -1,48 +0,0 @@ -name: Lean CI (kelly_lean) - -# CI for kelly_lean (QuantConnect/kelly_lean) — optimalité du critère de Kelly : -# pour un pari de Bernoulli (probabilité p de gain, cote nette b), la fraction -# optimale f* = (b·p − q)/b maximise de façon unique le taux de croissance espéré -# g(f) = p·log(1+b·f) + q·log(1−f). Prouvé via la tangente log t ≤ t − 1, sans -# recourir à la concavité abstraite. Premier Lean lake liant position sizing à un -# résultat formel (roadmap #4038 Tier 2, issue #4052). -# -# sorry-filter-mode=real, baseline=0 : la bibliothèque est intégralement -# sans sorry ; les deux théorèmes `kelly_optimal` (f* maximise g) et `kelly_unique` -# (sur/sous-pari strictement sous-optimaux) sont prouvés. Ce CI garde qu'AUCUN nouveau -# `sorry` tactic standalone n'est introduit (jamais de faux positif sur les mentions -# prose « 0-sorry »/« sans sorry » ; rattrape tout nouveau sorry standalone). - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/**.lean' - - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lean-toolchain' - pull_request: - branches: [main] - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/**.lean' - - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/QuantConnect/kelly_lean/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-kelly-${{ 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/QuantConnect/kelly_lean - display-name: kelly_lean - sorry-baseline: "0" - sorry-filter-mode: real diff --git a/.github/workflows/lean-minimax.yml b/.github/workflows/lean-minimax.yml deleted file mode 100644 index eb8ea9f009..0000000000 --- a/.github/workflows/lean-minimax.yml +++ /dev/null @@ -1,52 +0,0 @@ -name: Lean CI (minimax_lean) - -# CI for minimax_lean (GameTheory/minimax_lean) — zero-sum games: bilinear payoff -# xᵀAy and the analytical core of the von Neumann minimax theorem. Specialization of -# the GameTheory series to the zero-sum setting (Nash already in lean_game_defs). -# -# This first deliverable proves the FORMAL CORE (roadmap #4038, issue #4054): -# bilinearity of the payoff (additivity + homogeneity in each variable) and joint + -# restricted continuity — the properties that carry the four Sion hypotheses. -# The full Sion application on stdSimplex (compactness/convexity of the simplex + -# affine⇒quasi-convex/quasi-concave + continuous⇒LSC/USC) is the OPEN next milestone, -# honestly documented (NOT sorry-stubbed). -# -# sorry-filter-mode=real, baseline=0: the library is fully sorry-free; -# this guards that NO new `sorry` is introduced (never -# false-positives on prose mentions of "0-sorry"/"sans sorry"; catches any NEW -# sorry, including `exact sorry`, `theorem foo := by sorry`, `def f : T := sorry`, -# `<;> sorry`). All proved lemmas (bilinearity, continuity) are 0-sorry. - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/**.lean' - - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lean-toolchain' - pull_request: - branches: [main] - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/**.lean' - - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/GameTheory/minimax_lean/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-minimax-${{ 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/minimax_lean - display-name: minimax_lean - sorry-baseline: "0" - sorry-filter-mode: real diff --git a/.github/workflows/lean-search.yml b/.github/workflows/lean-search.yml deleted file mode 100644 index aefd714eda..0000000000 --- a/.github/workflows/lean-search.yml +++ /dev/null @@ -1,52 +0,0 @@ -name: Lean CI (search_lean) - -# CI for search_lean (Search/search_lean) — A* optimality lake at the Search series -# root. Formalizes the landmark theorems of A* (Hart, Nilsson & Raphael, 1968): -# phase-1 `admissible_le_suffix_cost` (anciennement `admissible_implies_optimal`, PR #4090), phase-2 -# `consistent_implies_admissible` (téléscopage). See #4048, roadmap #4038, -# registry #3801 (prong B « problème non-trivial » — répond au grief BFS-vs-A* -# dégénéré sur graphe à coût uniforme). -# -# Renamed astar_lean -> search_lean (lake rename, multi-module vocation: A* proven, -# future WFC/CSP modules as sibling libs). Lib «Astar» unchanged. See #4365. -# -# sorry-filter-mode=real, baseline=0: the lake is fully -# sorry-free across all modules (Graph, Heuristic, Optimality, Consistency). -# `real` strips `--` and `/- -/` then counts `\bsorry\b` word-bounded -# (catches `exact sorry`, `theorem foo := by sorry`, `def f : T := sorry`, -# `<;> sorry`; never false-positives on prose); baseline 0 = any new sorry -# fails CI. See lean-build.yml. - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/Search/search_lean/**.lean' - - 'MyIA.AI.Notebooks/Search/search_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/Search/search_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/Search/search_lean/lean-toolchain' - pull_request: - branches: [main] - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/Search/search_lean/**.lean' - - 'MyIA.AI.Notebooks/Search/search_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/Search/search_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/Search/search_lean/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-search-${{ 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/Search/search_lean - display-name: search_lean - sorry-baseline: "0" - sorry-filter-mode: real diff --git a/.github/workflows/lean-sudoku.yml b/.github/workflows/lean-sudoku.yml deleted file mode 100644 index 51dc27e42b..0000000000 --- a/.github/workflows/lean-sudoku.yml +++ /dev/null @@ -1,45 +0,0 @@ -name: Lean CI (sudoku_lean) - -# CI for sudoku_lean (MyIA.AI.Notebooks/Sudoku/sudoku_lean) — Sudoku constraint -# propagation soundness lake (naked/hidden single, peer exclusion). Part of Lean roadmap -# #4038 Tier 3, issue #4055. Coordination with #2978 verified (no overlap: #2978's Lean -# angle is finiteness-derivatives regex termination). -# -# sorry-filter-mode=real, baseline=0: the module is entirely sorry-free. -# `real` strips `--` and `/- -/` then counts `\bsorry\b` word-bounded -# (catches `exact sorry`, `theorem foo := by sorry`, `def f : T := sorry`, -# `<;> sorry`; never prose false-positives). See lean-build.yml. - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/**.lean' - - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lean-toolchain' - pull_request: - branches: [main] - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/**.lean' - - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.toml' - - 'MyIA.AI.Notebooks/Sudoku/sudoku_lean/lean-toolchain' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-sudoku-${{ 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/Sudoku/sudoku_lean - display-name: sudoku_lean - sorry-baseline: "0" - sorry-filter-mode: real diff --git a/scripts/ci/check_lake_matrix_paths.py b/scripts/ci/check_lake_matrix_paths.py new file mode 100644 index 0000000000..873d9a457a --- /dev/null +++ b/scripts/ci/check_lake_matrix_paths.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python3 +"""Garde anti-drift du dispatcher matriciel Lean (#13751). + +Le manifeste ``scripts/lean/ci_lakes.json`` est la source unique des lakes +migres vers la matrice ; le ``on.paths`` de +``.github/workflows/lean-ci-matrix.yml`` est l'UNION des chemins de +declenchement. Ces deux surfaces derivent si on les maintient a la main : +un lake ajoute au manifeste sans chemin dans l'union serait un lake que +PLUS AUCUN declencheur ne voit (CI silencieusement morte -- exactement le +defaut que le self-cover de #8712 ferme pour les fichiers du gate). + +Ce garde verifie, fail-CLOSED (exit 1) : + + 1. chaque chemin ``paths`` de chaque lake du manifeste figure dans les + DEUX blocs (``push`` et ``pull_request``) du dispatcher ; + 2. chaque self-cover du dispatcher existe bien sur le disque (chemin + mort = garde muette) ; + 3. aucun lake du manifeste ne garde son dispatcher historique + ``lean-.yml`` : les deux declencheurs ensemble produiraient un + DOUBLE build du meme lake sur la meme PR. +""" + +from __future__ import annotations + +import argparse +import json +import sys +from pathlib import Path + +import yaml + +REPO_ROOT = Path(__file__).resolve().parents[2] +DEFAULT_MANIFEST = REPO_ROOT / "scripts" / "lean" / "ci_lakes.json" +DEFAULT_WORKFLOW = (REPO_ROOT / ".github" / "workflows" / + "lean-ci-matrix.yml") + + +def workflow_paths(doc: dict, event: str) -> set[str]: + trig = doc.get("on") or doc.get(True) + return set(trig.get(event, {}).get("paths", [])) + + +def main(argv: list[str] | None = None) -> int: + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--manifest", type=Path, default=DEFAULT_MANIFEST) + ap.add_argument("--workflow", type=Path, default=DEFAULT_WORKFLOW) + ap.add_argument("--repo-root", type=Path, default=REPO_ROOT) + args = ap.parse_args(argv) + + manifest = json.loads(args.manifest.read_text(encoding="utf-8")) + doc = yaml.safe_load(args.workflow.read_text(encoding="utf-8")) + push = workflow_paths(doc, "push") + pr = workflow_paths(doc, "pull_request") + + errors: list[str] = [] + for lake in manifest["lakes"]: + for p in lake["paths"]: + for event, surface in (("push", push), ("pull_request", pr)): + if p not in surface: + errors.append( + f"lake {lake['lake']}: chemin {p!r} absent du " + f"on.paths[{event}] de {args.workflow.name} -- la " + f"CI de ce lake ne se declenche plus") + legacy = args.repo_root / ".github" / "workflows" / f"lean-{lake['lake']}.yml" + if legacy.exists(): + errors.append( + f"lake {lake['lake']}: le dispatcher historique " + f"{legacy.name} existe encore ALORS que le lake est au " + f"manifeste -- double declencheur = double build") + + for p in sorted(push | pr): + if p.startswith((".github/", "scripts/")) and not (args.repo_root / p).exists(): + errors.append( + f"self-cover {p!r} du dispatcher n'existe pas sur le disque") + + if errors: + for e in errors: + print(f"LAKE-MATRIX DRIFT: {e}", file=sys.stderr) + return 1 + n = len(manifest["lakes"]) + print(f"lake-matrix OK : {n} lake(s) couvert(s), union push/pr " + f"coherente avec le manifeste, aucun double declencheur") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/lean/ci_lakes.json b/scripts/lean/ci_lakes.json new file mode 100644 index 0000000000..6ceb561a29 --- /dev/null +++ b/scripts/lean/ci_lakes.json @@ -0,0 +1,83 @@ +{ + "_comment": "Manifeste des lakes pilotes de la matrice lean-ci (#13751 sous-item workflows). Source unique de verite pour le dispatcher lean-ci-matrix.yml : chemins de declenchement + parametres par lake. Le sorry-baseline est le MEME contrat bidirectionnel que lean-build.yml (echoue au-dessus ET en-dessous) : decharger un sorry = decrementer ici dans la meme PR. Un lake migre ici seulement apres suppression de son dispatcher lean-.yml (jamais les deux declencheurs a la fois). Garde anti-drift : scripts/ci/check_lake_matrix_paths.py verifie que chaque chemin du manifeste figure dans le on.paths du dispatcher.", + "lakes": [ + { + "lake": "sudoku", + "project-path": "MyIA.AI.Notebooks/Sudoku/sudoku_lean", + "display-name": "sudoku_lean", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/Sudoku/sudoku_lean/**.lean", + "MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.lean", + "MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.toml", + "MyIA.AI.Notebooks/Sudoku/sudoku_lean/lean-toolchain" + ] + }, + { + "lake": "kelly", + "project-path": "MyIA.AI.Notebooks/QuantConnect/kelly_lean", + "display-name": "kelly_lean", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/QuantConnect/kelly_lean/**.lean", + "MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.lean", + "MyIA.AI.Notebooks/QuantConnect/kelly_lean/lakefile.toml", + "MyIA.AI.Notebooks/QuantConnect/kelly_lean/lean-toolchain" + ] + }, + { + "lake": "minimax", + "project-path": "MyIA.AI.Notebooks/GameTheory/minimax_lean", + "display-name": "minimax_lean", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/GameTheory/minimax_lean/**.lean", + "MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.lean", + "MyIA.AI.Notebooks/GameTheory/minimax_lean/lakefile.toml", + "MyIA.AI.Notebooks/GameTheory/minimax_lean/lean-toolchain" + ] + }, + { + "lake": "search", + "project-path": "MyIA.AI.Notebooks/Search/search_lean", + "display-name": "search_lean", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/Search/search_lean/**.lean", + "MyIA.AI.Notebooks/Search/search_lean/lakefile.lean", + "MyIA.AI.Notebooks/Search/search_lean/lakefile.toml", + "MyIA.AI.Notebooks/Search/search_lean/lean-toolchain" + ] + }, + { + "lake": "assignment", + "project-path": "MyIA.AI.Notebooks/GameTheory/assignment_lean", + "display-name": "assignment_lean", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/GameTheory/assignment_lean/**.lean", + "MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.lean", + "MyIA.AI.Notebooks/GameTheory/assignment_lean/lakefile.toml", + "MyIA.AI.Notebooks/GameTheory/assignment_lean/lean-toolchain" + ] + }, + { + "lake": "discrepancy", + "project-path": "MyIA.AI.Notebooks/Search/discrepancy_lean", + "display-name": "discrepancy_lean", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "paths": [ + "MyIA.AI.Notebooks/Search/discrepancy_lean/**.lean", + "MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.lean", + "MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.toml", + "MyIA.AI.Notebooks/Search/discrepancy_lean/lean-toolchain" + ] + } + ] +} diff --git a/scripts/lean/lake_matrix_dispatch.py b/scripts/lean/lake_matrix_dispatch.py new file mode 100644 index 0000000000..78dce245ac --- /dev/null +++ b/scripts/lean/lake_matrix_dispatch.py @@ -0,0 +1,94 @@ +#!/usr/bin/env python3 +"""Dispatch des lakes Lean vers la matrice CI (#13751, sous-item workflows). + +Consomme le manifeste ``scripts/lean/ci_lakes.json`` et la liste des +fichiers changes d'un evenement push/pull_request, et rend l'ensemble +``include`` de la matrice a executer : + + - un fichier qui matche les ``paths`` d'un lake -> ce lake ; + - un fichier de GATE_SELF_COVER (le workflow lui-meme, le reusable + lean-build.yml, le composite, ce script, le manifeste) -> TOUS les + lakes : un changement du gate doit lancer le gate (lecon #8712 -- + les workflows definissant la CI sont les seuls fichiers qu'elle ne + verifiait jamais ; la forme matricielle herite de l'obligation). + +Sortie : JSON ``{"any": bool, "include": [entrees de manifeste]}`` sur +stdout, ou ecriture directe du fichier outputs GitHub via +``--outputs-file`` (cles ``any`` et ``lake-set``). Pur et testable : +aucun acces reseau, aucun appel gh, fnmatch uniquement. +""" + +from __future__ import annotations + +import argparse +import fnmatch +import json +import sys +from pathlib import Path + +REPO_ROOT = Path(__file__).resolve().parents[2] +DEFAULT_MANIFEST = REPO_ROOT / "scripts" / "lean" / "ci_lakes.json" + +# Un changement du gate lance le gate pour TOUS les lakes du manifeste +# (self-cover, lecon #8712 : le dispatcher supprime `lean-.yml` +# de la liste -- c'est ce fichier qui le remplace). +GATE_SELF_COVER = [ + ".github/workflows/lean-ci-matrix.yml", + ".github/workflows/lean-build.yml", + ".github/actions/lean-build/action.yml", + "scripts/lean/ci_lakes.json", + "scripts/lean/lake_matrix_dispatch.py", + "scripts/ci/check_lake_matrix_paths.py", +] + + +def changed_lakes(changed: list[str], manifest: dict) -> list[dict]: + lakes = manifest["lakes"] + if any(f in GATE_SELF_COVER for f in changed): + return list(lakes) + selected: dict[str, dict] = {} + for entry in lakes: + for pattern in entry["paths"]: + if any(fnmatch.fnmatch(f, pattern) for f in changed): + selected[entry["lake"]] = entry + break + # Ordre stable = ordre du manifeste (determinisme des check-runs). + return [e for e in lakes if e["lake"] in selected] + + +def main(argv: list[str] | None = None) -> int: + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--manifest", type=Path, default=DEFAULT_MANIFEST) + ap.add_argument("--changed-file", type=Path, default=None, + help="fichier contenant un chemin change par ligne " + "(defaut : stdin)") + ap.add_argument("--outputs-file", type=Path, default=None, + help="ecrire les outputs GitHub (any, lake-set) dans " + "ce fichier au lieu du JSON stdout") + args = ap.parse_args(argv) + + manifest = json.loads(args.manifest.read_text(encoding="utf-8")) + if args.changed_file is not None: + changed = [l.strip() for l in + args.changed_file.read_text(encoding="utf-8").splitlines() + if l.strip()] + else: + changed = [l.strip() for l in sys.stdin if l.strip()] + + include = changed_lakes(changed, manifest) + result = {"any": bool(include), "include": include} + + if args.outputs_file is not None: + lines = [ + f"any={'true' if result['any'] else 'false'}", + "lake-set=" + json.dumps({"include": include}, separators=(",", ":")), + ] + args.outputs_file.write_text("\n".join(lines) + "\n", encoding="utf-8") + else: + json.dump(result, sys.stdout, indent=1, ensure_ascii=False) + sys.stdout.write("\n") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/tests/test_lake_matrix_dispatch.py b/scripts/tests/test_lake_matrix_dispatch.py new file mode 100644 index 0000000000..5761e20431 --- /dev/null +++ b/scripts/tests/test_lake_matrix_dispatch.py @@ -0,0 +1,232 @@ +"""Tests de scripts/lean/lake_matrix_dispatch.py et +scripts/ci/check_lake_matrix_paths.py (#13751 pilote). + +Charge les modules par importlib depuis le worktree (pattern maison des +tests de scripts), construit des manifestes/workflows de fixture MINIMAUX, +et verifie les trois contrats : + + 1. selection par fnmatch (un chemin change -> un lake) ; + 2. self-cover GATE_SELF_COVER -> TOUS les lakes (lecon #8712) ; + 3. garde fail-CLOSED : chemin de manifeste absent de l'union -> + exit 1 ; dispatcher historique encore present -> exit 1. + +La garde est aussi testee CONTRE LES VRAIS FICHIERS du depot (manifeste + +workflow reels) : c'est le contrat qui protege le merge. +""" + +from __future__ import annotations + +import importlib.util +import json +import subprocess +import sys +from pathlib import Path + +import pytest + +REPO_ROOT = Path(__file__).resolve().parents[2] +DISPATCH = REPO_ROOT / "scripts" / "lean" / "lake_matrix_dispatch.py" +GUARD = REPO_ROOT / "scripts" / "ci" / "check_lake_matrix_paths.py" + + +def _load(path: Path, name: str): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +@pytest.fixture(scope="module") +def dispatch_mod(): + return _load(DISPATCH, "lake_matrix_dispatch_under_test") + + +@pytest.fixture(scope="module") +def manifest(): + return json.loads( + (REPO_ROOT / "scripts" / "lean" / "ci_lakes.json") + .read_text(encoding="utf-8")) + + +# --- Selection ----------------------------------------------------------- + + +def test_one_changed_file_selects_its_lake(dispatch_mod, manifest): + lakes = dispatch_mod.changed_lakes( + ["MyIA.AI.Notebooks/Sudoku/sudoku_lean/src/Sudoku.lean"], manifest) + assert [l["lake"] for l in lakes] == ["sudoku"] + + +def test_nested_lean_file_matches_glob(dispatch_mod, manifest): + lakes = dispatch_mod.changed_lakes( + ["MyIA.AI.Notebooks/GameTheory/minimax_lean/Nim/Core.lean"], manifest) + assert [l["lake"] for l in lakes] == ["minimax"] + + +def test_lakefile_toml_triggers(dispatch_mod, manifest): + lakes = dispatch_mod.changed_lakes( + ["MyIA.AI.Notebooks/Search/discrepancy_lean/lakefile.toml"], manifest) + assert [l["lake"] for l in lakes] == ["discrepancy"] + + +def test_two_lakes_selected_in_manifest_order(dispatch_mod, manifest): + lakes = dispatch_mod.changed_lakes( + ["MyIA.AI.Notebooks/Search/search_lean/lakefile.lean", + "MyIA.AI.Notebooks/QuantConnect/kelly_lean/lean-toolchain"], + manifest) + # Ordre du manifeste (kelly avant search), pas l'ordre des fichiers. + assert [l["lake"] for l in lakes] == ["kelly", "search"] + + +def test_unrelated_file_selects_nothing(dispatch_mod, manifest): + assert dispatch_mod.changed_lakes( + ["docs/reference/whatever.md"], manifest) == [] + + +def test_self_cover_file_selects_all(dispatch_mod, manifest): + lakes = dispatch_mod.changed_lakes( + ["scripts/lean/ci_lakes.json"], manifest) + assert [l["lake"] for l in lakes] == [l["lake"] for l in manifest["lakes"]] + + +def test_every_self_cover_entry_selects_all(dispatch_mod, manifest): + for f in dispatch_mod.GATE_SELF_COVER: + lakes = dispatch_mod.changed_lakes([f], manifest) + assert len(lakes) == len(manifest["lakes"]), f( + "self-cover {f} ne declenche pas tous les lakes") + + +def test_dedup_when_glob_and_literal_both_match(dispatch_mod, manifest): + # Un commit qui touche lakefile.lean ET un .lean profond du meme lake : + # le lake n'apparait qu'une fois. + lakes = dispatch_mod.changed_lakes( + ["MyIA.AI.Notebooks/Sudoku/sudoku_lean/lakefile.lean", + "MyIA.AI.Notebooks/Sudoku/sudoku_lean/src/Deep.lean"], + manifest) + assert [l["lake"] for l in lakes] == ["sudoku"] + + +# --- CLI : format outputs-file -------------------------------------------- + + +def test_outputs_file_format(tmp_path, manifest): + changed = tmp_path / "changed.txt" + changed.write_text( + "MyIA.AI.Notebooks/GameTheory/assignment_lean/A.lean\n", encoding="utf-8") + out = tmp_path / "gh_outputs.txt" + rc = subprocess.call( + [sys.executable, str(DISPATCH), + "--changed-file", str(changed), "--outputs-file", str(out)]) + assert rc == 0 + text = out.read_text(encoding="utf-8") + lines = dict(l.split("=", 1) for l in text.strip().splitlines()) + assert lines["any"] == "true" + payload = json.loads(lines["lake-set"]) + assert [e["lake"] for e in payload["include"]] == ["assignment"] + # Chaque entree porte les cles que la matrice consomme. + entry = payload["include"][0] + for k in ("lake", "project-path", "display-name", + "sorry-baseline", "sorry-filter-mode"): + assert k in entry, f"cle matrice manquante: {k}" + + +def test_outputs_file_empty_intersection_any_false(tmp_path): + changed = tmp_path / "changed.txt" + changed.write_text("README.md\n", encoding="utf-8") + out = tmp_path / "gh_outputs.txt" + subprocess.call([sys.executable, str(DISPATCH), + "--changed-file", str(changed), + "--outputs-file", str(out)]) + lines = dict(l.split("=", 1) + for l in out.read_text(encoding="utf-8").strip().splitlines()) + assert lines["any"] == "false" + assert json.loads(lines["lake-set"])["include"] == [] + + +# --- Garde : fail-CLOSED --------------------------------------------------- + + +def _write_workflow(path: Path, push_paths: list[str], pr_paths: list[str]): + doc = { + "on": { + "push": {"branches": ["main"], "paths": push_paths}, + "pull_request": {"branches": ["main"], + "types": ["opened", "synchronize"], + "paths": pr_paths}, + }, + "jobs": {"changes": {"runs-on": "ubuntu-latest"}}, + } + import yaml + path.write_text(yaml.safe_dump(doc, sort_keys=False), encoding="utf-8") + return path + + +def test_guard_green_on_repo_files(): + rc = subprocess.call([sys.executable, str(GUARD)]) + assert rc == 0, "le garde doit etre vert sur l'etat livre du depot" + + +def test_guard_red_when_manifest_path_missing_from_push(tmp_path, manifest): + wf = _write_workflow( + tmp_path / "wf.yml", + push_paths=[], # push vide -> chaque chemin manque + pr_paths=[p for l in manifest["lakes"] for p in l["paths"]], + ) + rc = subprocess.call( + [sys.executable, str(GUARD), + "--manifest", str(REPO_ROOT / "scripts" / "lean" / "ci_lakes.json"), + "--workflow", str(wf), "--repo-root", str(REPO_ROOT)]) + assert rc == 1 + + +def test_guard_red_when_only_pr_block_covers(tmp_path, manifest): + """Le push couvre, le pull_request oublie un lake -> fail-CLOSED.""" + all_paths = [p for l in manifest["lakes"] for p in l["paths"]] + pr_paths = [p for p in all_paths if not p.startswith( + "MyIA.AI.Notebooks/Sudoku/")] + wf = _write_workflow(tmp_path / "wf.yml", all_paths, pr_paths) + rc = subprocess.call( + [sys.executable, str(GUARD), + "--manifest", str(REPO_ROOT / "scripts" / "lean" / "ci_lakes.json"), + "--workflow", str(wf), "--repo-root", str(REPO_ROOT)]) + assert rc == 1 + + +def test_guard_red_when_legacy_dispatcher_still_present(tmp_path, manifest): + all_paths = [p for l in manifest["lakes"] for p in l["paths"]] + wf = _write_workflow(tmp_path / "wf.yml", all_paths, all_paths) + legacy = tmp_path / ".github" / "workflows" / "lean-sudoku.yml" + legacy.parent.mkdir(parents=True) + legacy.write_text("name: legacy\n", encoding="utf-8") + rc = subprocess.call( + [sys.executable, str(GUARD), + "--manifest", str(REPO_ROOT / "scripts" / "lean" / "ci_lakes.json"), + "--workflow", str(wf), "--repo-root", str(tmp_path)]) + assert rc == 1 + + +def test_guard_green_on_full_coverage_with_fake_repo(tmp_path, manifest): + all_paths = [p for l in manifest["lakes"] for p in l["paths"]] + wf = _write_workflow(tmp_path / "wf.yml", all_paths, all_paths) + # Pas de dispatcher legacy, et les self-cover references par le workflow + # fixture n'existent pas -- mais la fixture n'en porte pas, donc rien + # a verifier : vert. + rc = subprocess.call( + [sys.executable, str(GUARD), + "--manifest", str(REPO_ROOT / "scripts" / "lean" / "ci_lakes.json"), + "--workflow", str(wf), "--repo-root", str(tmp_path)]) + assert rc == 0 + + +def test_guard_red_on_dead_self_cover_path(tmp_path, manifest): + all_paths = [p for l in manifest["lakes"] for p in l["paths"]] + wf = _write_workflow( + tmp_path / "wf.yml", + all_paths + ["scripts/lean/does_not_exist.py"], + all_paths + ["scripts/lean/does_not_exist.py"], + ) + rc = subprocess.call( + [sys.executable, str(GUARD), + "--manifest", str(REPO_ROOT / "scripts" / "lean" / "ci_lakes.json"), + "--workflow", str(wf), "--repo-root", str(REPO_ROOT)]) + assert rc == 1 From 04d1ed1bb703cbf64e558f2f282aeefa501ba9a9 Mon Sep 17 00:00:00 2001 From: jsboige Date: Fri, 18 Sep 2026 18:00:26 +0200 Subject: [PATCH 2/2] docs(ci,#13751): commentaire skip check-run corrige sur preuve du run pilote MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Le run 35362544806 montre le job ci garde comme check-run SKIPPED ("Lean CI (${{ inputs.display-name }})"), pas absent : un job dont le if est faux cree BIEN un check-run (inactif, jamais bloquant). Les deux commentaires qui affirmaient "aucun check-run cree" sont corriges sur cette mesure — un caller mono-lake verra une ligne ci-matrix SKIPPED par run, bruit cosmetique assumé. Co-Authored-By: Claude Sonnet 5 --- .github/workflows/lean-build.yml | 6 ++++-- .github/workflows/lean-ci-matrix.yml | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/.github/workflows/lean-build.yml b/.github/workflows/lean-build.yml index 73b918d611..77a8452977 100644 --- a/.github/workflows/lean-build.yml +++ b/.github/workflows/lean-build.yml @@ -74,8 +74,10 @@ permissions: jobs: # Mono-lake : comportement historique, inchange pour les ~26 dispatchers # lean-.yml restants. Le garde `if` n'existe que pour le mode matrice - # (les deux jobs ne tournent jamais ensemble ; un job dont le `if` est faux - # ne cree AUCUN check-run, donc zero bruit pour les callers mono-lake). + # (les deux jobs ne tournent jamais ensemble). Un job garde par un `if` + # faux apparait comme check-run SKIPPED (inactif, jamais bloquant) : un + # caller mono-lake verra donc une ligne ci-matrix SKIPPED par run — bruit + # cosmétique, pas d'exécution. ci: if: inputs.lake-set == 'none' name: "Lean CI (${{ inputs.display-name }})" diff --git a/.github/workflows/lean-ci-matrix.yml b/.github/workflows/lean-ci-matrix.yml index dd92677948..d1c7547818 100644 --- a/.github/workflows/lean-ci-matrix.yml +++ b/.github/workflows/lean-ci-matrix.yml @@ -171,7 +171,7 @@ jobs: # par lake (job `ci-matrix` de lean-build.yml). Les 4 inputs mono-lake # sont des valeurs de facade (required: true au sens du schema) -- en # mode matrice, `ci` est garde par `if: lake-set == 'none'` et ne tourne - # jamais ; aucun check-run n'est cree pour lui. + # jamais ; il apparait comme check-run SKIPPED (inactif, jamais bloquant). lean-matrix: needs: changes if: needs.changes.outputs.any == 'true'