diff --git a/.github/workflows/lean-ci-matrix.yml b/.github/workflows/lean-ci-matrix.yml index 670e5d8ce4..65cb0963ac 100644 --- a/.github/workflows/lean-ci-matrix.yml +++ b/.github/workflows/lean-ci-matrix.yml @@ -130,6 +130,12 @@ on: - 'MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/**.lean' - 'MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/lakefile.lean' - 'MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/lean-toolchain' + # geometry_lean (herite du wrapper lean-geometry.yml supprime, #13751 : + # 0 sorry verifie de naissance, axiom target-modules "*" + allow-axioms vide, + # fail-on-sorry true par defaut -- parametres reportes au manifeste) + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/**.lean' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lean-toolchain' # Self-cover B.3 herite du wrapper lean-serre.yml supprime (#17336) : # le moteur d'axiomes change -> le gate axiom de serre100 rejoue. - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/lean_server.py' @@ -248,6 +254,12 @@ on: - 'MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/**.lean' - 'MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/lakefile.lean' - 'MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/lean-toolchain' + # geometry_lean (herite du wrapper lean-geometry.yml supprime, #13751 : + # 0 sorry verifie de naissance, axiom target-modules "*" + allow-axioms vide, + # fail-on-sorry true par defaut -- parametres reportes au manifeste) + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/**.lean' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lakefile.lean' + - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lean-toolchain' # Self-cover B.3 herite du wrapper lean-serre.yml supprime (#17336) : # le moteur d'axiomes change -> le gate axiom de serre100 rejoue. - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/lean_server.py' diff --git a/.github/workflows/lean-geometry.yml b/.github/workflows/lean-geometry.yml deleted file mode 100644 index 0dad806a20..0000000000 --- a/.github/workflows/lean-geometry.yml +++ /dev/null @@ -1,69 +0,0 @@ -name: Lean CI (geometry_lean) - -# CI for geometry_lean (MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry). -# Companion lake of the Geometry series (EPIC #18601 volet B): each Python -# concept notebook gets a Lean module formalizing what the algorithm computes. -# First theorem: the midpoint of the hypotenuse (position 05 of #17544). -# 0 sorry (raw=0, verified), fully proven from birth. -# Template: lean-percolation.yml (small lake, sorry-filter-mode: real). - -on: - push: - branches: [main] - paths: - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/**.lean' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lean-toolchain' - # The gate's own implementation: a change to it must re-run the gate - # (same rationale as lean-galois.yml / lean-conway.yml, cf #8951). - - '.github/workflows/lean-geometry.yml' - - '.github/workflows/lean-axiom.yml' - # The axiom step is a Python program (`from lean_server import LeanVerifier`); - # lean_server.py + lean_utils.py ARE gate inputs (cf #8722). - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/lean_server.py' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/lean_utils.py' - pull_request: - types: [opened, synchronize, edited, reopened] - paths: - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/**.lean' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lakefile.lean' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lean-toolchain' - # The gate must run on the PR that introduces or changes it (cf #8712). - - '.github/workflows/lean-geometry.yml' - - '.github/workflows/lean-axiom.yml' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/lean_server.py' - - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/lean_utils.py' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: lean-geometry-${{ 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/Geometry/geometry_lean - display-name: geometry_lean - sorry-baseline: "0" - sorry-filter-mode: real - - # Level 3 proof-integrity gate (criterion B.3 of pr-review-discipline): - # a lake born with a dedicated workflow -- B.3 never reads "non applicable". - # fail-on-sorry: true -- sorry-baseline is 0, the lake is fully proven. - # target-modules: "*" (issue #10889) -- the module list is derived at runtime - # from the lake walk, so it cannot drift out of view. The `_en` i18n siblings - # are EXCLUDED by default (FR-only measurement; the byte-parity of the i18n - # pair is covered structurally by `lean-i18n-drift.yml`, #10007). - proof-integrity: - needs: ci # serialize the two compiles (parity with knot_lean #14922) - uses: jsboige/CoursIA/.github/workflows/lean-axiom.yml@main - with: - project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean - display-name: geometry_lean - target-modules: "*" - allow-axioms: "" - fail-on-sorry: true diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md index a490259979..b9c15360ca 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md @@ -20,9 +20,10 @@ lake build # 0 sorry — le lac est intégralement prouvé ``` La CI -([`lean-geometry.yml`](https://github.com/jsboige/CoursIA/blob/main/.github/workflows/lean-geometry.yml)) -rejoue le build et le gate proof-integrity (axiomes) sur chaque PR touchant le -lac. +([`lean-ci-matrix.yml`](https://github.com/jsboige/CoursIA/blob/main/.github/workflows/lean-ci-matrix.yml), +entrée `geometry` du manifeste `scripts/lean/ci_lakes.json` depuis la +consolidation #13751) rejoue le build et le gate proof-integrity (axiomes) +sur chaque PR touchant le lac. ## Feuille de route diff --git a/scripts/lean/ci_lakes.json b/scripts/lean/ci_lakes.json index 8106e93315..5f2be4be5f 100644 --- a/scripts/lean/ci_lakes.json +++ b/scripts/lean/ci_lakes.json @@ -296,6 +296,19 @@ "MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/lakefile.lean", "MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/lean-toolchain" ] + }, + { + "lake": "geometry", + "project-path": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean", + "display-name": "geometry_lean", + "sorry-baseline": "0", + "sorry-filter-mode": "real", + "axiom-target-modules": "*", + "paths": [ + "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/**.lean", + "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lakefile.lean", + "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lean-toolchain" + ] } ] }