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..28ec12fb9f 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 @@ -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 = [] diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/update_demos_v2.py b/MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/update_demos_v2.py index ca69bb4d6c..924516aa89 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/scripts/_archive/update_demos_v2.py +++ b/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: diff --git a/MyIA.AI.Notebooks/cross-series/matching-cv/main.py b/MyIA.AI.Notebooks/cross-series/matching-cv/main.py index 07da7ebed7..d6fc5f9cd5 100644 --- a/MyIA.AI.Notebooks/cross-series/matching-cv/main.py +++ b/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)