From 31c1a4b25461b22878aa255da0a9697a6c6d0170 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 13 Sep 2026 11:06:27 +0200 Subject: [PATCH] fix(lean-scripts): retirer la queue orpheline qui empeche run_lean9_demos.py de compiler MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Le fichier ne compilait pas sur `main` : `IndentationError: unexpected indent`, ligne 511. Defaut entre a `c80aea1106` (2026-01-31), dont le parent `ef567c47a9` compile (552 lignes). Ce commit inserait quatre demos graduees a la place de l'ancien `DEMO_1_REFLEXIVITY`, mais son texte se terminait par `],` — une fermeture prematuree de la liste `DEMOS` — et laissait les trois dernieres lignes de l'ancien `DEMO_1_REFLEXIVITY` orphelines apres ce `],`, alors que la liste continue jusqu'a son `]` en ligne 544. Ces trois lignes sont exactement les anciennes lignes 473-475 du parent, queue d'un dict dont le remplacant (le nouveau `DEMO_1_REFLEXIVITY`) porte la meme intention : `strategy = "rfl"`. Rien n'est perdu a les retirer. Correctif : `],` redevient la continuation `},` de `DEMO_4_COMPOSITION`, les trois lignes orphelines disparaissent. 0 insertion, 4 suppressions. Verifie : `py_compile` OK ; `ast.parse` -> `DEMOS` = 7 entrees, noms, complexites et strategies preserves. Sweep de classe : 51 fichiers `.py` sous SymbolicAI/Lean/scripts/ dont 1 seul en echec de syntaxe (celui-ci) ; CodeQL en compte 1 sur 2036 a l'echelle du depot. Ce n'est pas une classe, c'est un fichier. Co-Authored-By: Claude Sonnet 5 --- .../SymbolicAI/Lean/scripts/_archive/run_lean9_demos.py | 4 ---- 1 file changed, 4 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/run_lean9_demos.py b/MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/run_lean9_demos.py index b98cc12ad7..9f94b251ea 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/run_lean9_demos.py +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/run_lean9_demos.py @@ -506,10 +506,6 @@ def prove_with_multi_agents( "complexity": "Avancee - plusieurs rewrites necessaires", "strategy": "rw [Nat.add_assoc, Nat.add_comm b c, ...] OU omega", "trap": "Un seul rewrite ne suffit pas, strategie multi-etapes" - } -], - "complexity": "Triviale - une tactique suffit", - "strategy": "rfl" }, { "name": "DEMO_2_SUCCESSOR",