fix(lean-archive,#codeql): run_lean9_demos.py syntax + update_demos_v2.py ReDoS

MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/run_lean9_demos.py

@@ -507,40 +507,6 @@ def prove_with_multi_agents(
         "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",
-        "theorem": "theorem succ_ne_zero (n : Nat) : Nat.succ n != 0",
-        "description": "Propriete structurelle - SearchAgent trouve Nat.succ_ne_zero",
-        "expected_iterations": "1-2",
-        "expected_lemmas": 1,
-        "expected_agents": ["SearchAgent", "TacticAgent"],
-        "complexity": "Simple - recherche de lemme",
-        "strategy": "exact Nat.succ_ne_zero n OU decide"
-    },
-    {
-        "name": "DEMO_3_LIST_INDUCTION",
-        "theorem": "theorem length_append (xs ys : List Nat) : (xs ++ ys).length = xs.length + ys.length",
-        "description": "Induction sur liste - necessite raisonnement structurel",
-        "expected_iterations": "2-4",
-        "expected_lemmas": 2,
-        "expected_agents": ["SearchAgent", "TacticAgent", "VerifierAgent"],
-        "complexity": "Intermediaire - induction + simplification",
-        "strategy": "induction xs <;> simp [*]"
-    },
-    {
-        "name": "DEMO_4_ALGEBRAIC",
-        "theorem": "theorem mul_add_distrib (a b c : Nat) : a * (b + c) = a * b + a * c",
-        "description": "Distributivite - peut necessiter induction OU lemme direct",
-        "expected_iterations": "3-6",
-        "expected_lemmas": 3,
-        "expected_agents": ["SearchAgent", "TacticAgent", "VerifierAgent", "CriticAgent"],
-        "complexity": "Avancee - multiple strategies possibles",
-        "strategy": "exact Nat.mul_add OU induction a avec ring"
-    }
 ]
 
 all_results = []

MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/update_demos_v2.py

@@ -67,6 +67,33 @@
 ]'''
 
 
+def _match_demos_block(text):
+    """Match a `DEMOS = [ ... ]` block in linear time.
+
+    ReDoS fix (CodeQL py/redos): the previous regex
+    `(DEMOS\\s*=\\s*\\[(?:[^\\[\\]]*\\{[^}]*\\})*[^\\[\\]]*\\])` had nested
+    quantifiers and tripped the CodeQL py/redos check on input like
+    `DEMOS=[{{{{...`. Replace with a single-pass bracket counter — O(n),
+    no backtracking states.
+    """
+    m = re.search(r'DEMOS\s*=\s*\[', text)
+    if not m:
+        return None
+    depth = 0
+    i = m.end() - 1  # position of `[`
+    n = len(text)
+    while i < n:
+        c = text[i]
+        if c == '[':
+            depth += 1
+        elif c == ']':
+            depth -= 1
+            if depth == 0:
+                return text[m.start():i + 1]
+        i += 1
+    return None
+
+
 def update_file_demos(filepath, is_notebook=False):
     """Update DEMOS in a file."""
     print(f"Processing: {filepath}")
@@ -82,10 +109,9 @@ def update_file_demos(filepath, is_notebook=False):
 
                 # Look for DEMOS definition
                 if 'DEMOS = [' in source and '"name":' in source:
-                    # Find the start and end of DEMOS
-                    match = re.search(r'(DEMOS\s*=\s*\[[^\]]*(?:\{[^}]*\}[^\]]*)*\])', source, re.DOTALL)
-                    if match:
-                        old_demos = match.group(1)
+                    # Find the start and end of DEMOS (linear-time, ReDoS-safe)
+                    old_demos = _match_demos_block(source)
+                    if old_demos:
                         new_source = source.replace(old_demos, NEW_DEMOS_STR)
 
                         if new_source != source:
@@ -102,10 +128,9 @@ def update_file_demos(filepath, is_notebook=False):
         with open(filepath, 'r', encoding='utf-8') as f:
             content = f.read()
 
-        # Find and replace DEMOS block
-        match = re.search(r'(DEMOS\s*=\s*\[[^\]]*(?:\{[^}]*\}[^\]]*)*\])', content, re.DOTALL)
-        if match:
-            old_demos = match.group(1)
+        # Find and replace DEMOS block (linear-time, ReDoS-safe)
+        old_demos = _match_demos_block(content)
+        if old_demos:
             new_content = content.replace(old_demos, NEW_DEMOS_STR)
 
             if new_content != content:

MyIA.AI.Notebooks/cross-series/matching-cv/main.py

@@ -283,4 +283,5 @@ def index():
 
 
 if __name__ == '__main__':
-    app.run(debug=True)
+    debug_mode = os.getenv('FLASK_DEBUG', 'False').lower() == 'true'
+    app.run(debug=debug_mode)