"""
Installation automatique des composants manquants
"""
import subprocess
import sys
import os
import platform
import shutil
import tempfile
import urllib.request
from pathlib import Path
from typing import Optional
# Delai maximal accorde a une sonde de version. Le shim elan est la sonde la plus
# lente mesuree : 30 essais sous charge nominale donnent 0,58 s au maximum. Les
# echecs observes sous timeout=5 arrivent en salves de charge, donc bien au-dela
# du cout nominal. 30 s borne l'attente pathologique sans mordre le cas nominal.
PROBE_TIMEOUT_S = 30
class LeanInstaller:
"""Installateur automatique pour l'environnement Lean 4"""
def __init__(self):
self.system = platform.system()
self.is_windows = self.system == "Windows"
self.is_macos = self.system == "Darwin"
self.is_linux = self.system == "Linux"
self.results = []
def log(self, message: str, level: str = "INFO"):
"""Log un message"""
prefix = {"INFO": "[*]", "OK": "[+]", "ERROR": "[!]", "WARN": "[~]"}.get(level, "[*]")
print(f"{prefix} {message}")
self.results.append((level, message))
def probe_present(self, binary: str, description: str) -> Optional[bool]:
"""Sonde la presence d'un binaire.
Rend True (present), False (absent), ou None : la sonde a ECHOUE
(delai depasse, erreur d'execution) et n'a rien etabli -- ni presence,
ni absence.
Sur Linux, elan n'exporte pas toujours son repertoire dans le PATH du
noyau : la sonde passe par `source ~/.elan/env`. Le code 127
("commande introuvable") est la seule reponse qui vaut absence reelle.
"""
if self.is_linux:
try:
result = subprocess.run(
["bash", "-c", f"source ~/.elan/env 2>/dev/null && {binary} --version"],
capture_output=True, text=True, timeout=PROBE_TIMEOUT_S, encoding="utf-8"
)
except subprocess.TimeoutExpired:
self.log(f"{description} : aucune reponse en {PROBE_TIMEOUT_S} s -- "
"sonde en echec, ce n'est PAS une absence", "WARN")
return None
except OSError as exc:
self.log(f"{description} : sonde impossible ({type(exc).__name__}) -- "
"ce n'est PAS une absence", "WARN")
return None
if result.returncode == 0:
return True
if result.returncode != 127:
self.log(f"{description} : sonde sans reponse exploitable "
f"(code {result.returncode}) -- ce n'est PAS une absence", "WARN")
return None
return False
return bool(shutil.which(binary))
def run_command(self, cmd: list, description: str, timeout: int = 300, shell: bool = False, check_elan_env: bool = False) -> bool:
"""Execute une commande et retourne True si succes"""
self.log(f"{description}...")
try:
# Sur Linux, sourcer .elan/env si demande
if self.is_linux and check_elan_env:
bash_cmd = f"source ~/.elan/env 2>/dev/null && {' '.join(cmd)}"
cmd = ["bash", "-c", bash_cmd]
if shell and self.is_windows:
result = subprocess.run(cmd, capture_output=True, text=True, timeout=timeout, shell=True, encoding="utf-8")
else:
result = subprocess.run(cmd, capture_output=True, text=True, timeout=timeout, encoding="utf-8")
if result.returncode == 0:
self.log(f"{description} - OK", "OK")
return True
else:
stderr = result.stderr[:200] if result.stderr else ""
if stderr:
self.log(f"{description} - Erreur: {stderr}", "ERROR")
return False
except subprocess.TimeoutExpired:
self.log(f"{description} - Timeout apres {timeout}s", "ERROR")
return False
except Exception as e:
self.log(f"{description} - Exception: {e}", "ERROR")
return False
def install_elan(self) -> bool:
"""Installe elan (gestionnaire de versions Lean)"""
# Verifier si deja installe (avec .elan/env sur Linux)
present = self.probe_present("elan", "elan")
if present is True:
self.log("elan deja installe", "OK")
return True
if present is None:
self.log("elan : non mesure (sonde en echec) -- installation NON tentee, "
"re-executez cette cellule avant de conclure a une absence", "WARN")
return None
self.log("Installation de elan...")
if self.is_windows:
return self._install_elan_windows()
else:
return self._install_elan_unix()
def _install_elan_windows(self) -> bool:
"""Installation elan sur Windows via PowerShell"""
try:
script_url = "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1"
with tempfile.NamedTemporaryFile(mode='w', suffix='.ps1', delete=False) as f:
script_path = f.name
self.log(f"Telechargement du script elan depuis {script_url}")
urllib.request.urlretrieve(script_url, script_path)
self.log("Execution du script d'installation (cela peut prendre quelques minutes)...")
escaped_path = script_path.replace("'", "''")
ps_command = f"& '{escaped_path}' -NoPrompt:$true -DefaultToolchain none"
cmd = ["powershell", "-ExecutionPolicy", "Bypass", "-Command", ps_command]
result = subprocess.run(cmd, capture_output=True, text=True, timeout=600, encoding="utf-8")
os.unlink(script_path)
if result.returncode == 0:
elan_bin = Path.home() / ".elan" / "bin"
if elan_bin.exists():
os.environ["PATH"] = str(elan_bin) + os.pathsep + os.environ.get("PATH", "")
self.log("elan installe avec succes", "OK")
return True
self.log(f"Erreur installation elan: {result.stderr[:300]}", "ERROR")
return False
except Exception as e:
self.log(f"Exception lors de l'installation elan: {e}", "ERROR")
return False
def _install_elan_unix(self) -> bool:
"""Installation elan sur Linux/macOS"""
try:
cmd = ["sh", "-c", "curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none"]
result = subprocess.run(cmd, capture_output=True, text=True, timeout=600, encoding="utf-8")
if result.returncode == 0:
elan_bin = Path.home() / ".elan" / "bin"
if elan_bin.exists():
os.environ["PATH"] = str(elan_bin) + os.pathsep + os.environ.get("PATH", "")
self.log("elan installe avec succes", "OK")
return True
self.log(f"Erreur: {result.stderr[:200]}", "ERROR")
return False
except Exception as e:
self.log(f"Exception: {e}", "ERROR")
return False
def install_lean4(self) -> bool:
"""Installe Lean 4 stable via elan"""
# Verifier si deja installe (avec .elan/env sur Linux)
present = self.probe_present("lean", "Lean 4")
if present is True:
self.log("Lean 4 deja installe", "OK")
return True
if present is None:
self.log("Lean 4 : non mesure (sonde en echec) -- installation NON tentee, "
"re-executez cette cellule avant de conclure a une absence", "WARN")
return None
# Verifier que elan est disponible
elan_path = shutil.which("elan")
if not elan_path and self.is_linux:
elan_bin = Path.home() / ".elan" / "bin" / "elan"
if elan_bin.exists():
elan_path = str(elan_bin)
if not elan_path:
self.log("elan non trouve - installez elan d'abord", "ERROR")
return False
self.log("Installation de Lean 4 (stable) via elan...")
self.log("Cela peut prendre plusieurs minutes (telechargement ~200MB)...")
return self.run_command(
[elan_path, "default", "leanprover/lean4:stable"],
"Installation Lean 4 stable",
timeout=600,
check_elan_env=True
)
def install_lean4_jupyter(self) -> bool:
"""Installe le module lean4_jupyter via pip"""
try:
import lean4_jupyter
self.log("lean4_jupyter deja installe", "OK")
return True
except ImportError:
pass
return self.run_command(
[sys.executable, "-m", "pip", "install", "lean4-jupyter", "--quiet"],
"Installation lean4_jupyter via pip",
timeout=120
)
def register_jupyter_kernel(self) -> bool:
"""Enregistre le kernel Lean dans Jupyter"""
# Verifier si un kernel lean existe deja
try:
result = subprocess.run([sys.executable, "-m", "jupyter", "kernelspec", "list"], capture_output=True, text=True, timeout=PROBE_TIMEOUT_S, encoding="utf-8")
if "lean" in result.stdout.lower():
self.log("Un kernel Lean est deja enregistre", "OK")
return True
except subprocess.TimeoutExpired:
self.log(f"Kernel Jupyter : aucune reponse en {PROBE_TIMEOUT_S} s -- "
"sonde en echec, enregistrement NON tente", "WARN")
return None
except OSError as exc:
self.log(f"Kernel Jupyter : sonde impossible ({type(exc).__name__}) -- "
"enregistrement NON tente", "WARN")
return None
self.log("Enregistrement du kernel Jupyter...")
try:
result = subprocess.run(
[sys.executable, "-m", "lean4_jupyter", "install"],
capture_output=True, text=True, timeout=60, encoding="utf-8"
)
if result.returncode == 0:
self.log("Kernel enregistre avec succes", "OK")
return True
else:
self.log(f"Avertissement: kernel non enregistre ({result.stderr[:100]})", "WARN")
self.log("Verifiez si un autre kernel lean existe deja", "WARN")
return False
except Exception as e:
self.log(f"Avertissement: {e}", "WARN")
return False
def install_all(self) -> bool:
"""Installe tous les composants manquants"""
print("=" * 60)
print(" INSTALLATION AUTOMATIQUE DES COMPOSANTS LEAN 4")
print("=" * 60)
print()
steps = [
("1/4", "elan", self.install_elan),
("2/4", "Lean 4", self.install_lean4),
("3/4", "lean4_jupyter", self.install_lean4_jupyter),
("4/4", "Kernel Jupyter", self.register_jupyter_kernel),
]
critical_failures = []
warnings = []
indeterminate = []
for step_num, name, func in steps:
print(f"\n--- Etape {step_num}: {name} ---")
success = func()
if success is None:
# Sonde en echec : ni installe, ni etabli manquant. Ne compte
# ni comme succes ni comme echec -- installer ne repond pas a
# une question qu'on n'a pas reussi a poser.
indeterminate.append(name)
elif not success:
# Kernel Jupyter est optionnel si un autre kernel lean existe
if name == "Kernel Jupyter":
warnings.append(name)
else:
critical_failures.append(name)
print("\n" + "=" * 60)
if indeterminate:
print(f"[~] Composant(s) non mesure(s) : {', '.join(indeterminate)}")
print(" Sonde(s) en echec : ni present(s) ni absent(s). Rien n'a ete")
print(" installe pour eux -- re-executez cette cellule.")
if not critical_failures and not indeterminate:
print("[OK] Installation terminee avec succes !")
if warnings:
print(f"\nAvertissements: {', '.join(warnings)}")
print("(Un kernel Lean alternatif existe probablement)")
print("\nIMPORTANT: Redemarrez le kernel Jupyter pour prendre en compte les changements.")
print(" Kernel > Restart Kernel")
return True
elif critical_failures:
print(f"[!] Installation incomplete: {', '.join(critical_failures)}")
print("\nPour une installation manuelle, voir la section 'Installation manuelle' ci-dessous.")
return False
else:
return False
# Verifier si l'installation est necessaire
try:
if not ALL_COMPONENTS_OK:
print("Des composants manquants ont ete detectes.")
print("Lancement de l'installation automatique...\n")
installer = LeanInstaller()
INSTALLATION_SUCCESS = installer.install_all()
elif INDETERMINATE_COMPONENTS:
print("=" * 60)
print("[~] AUCUN COMPOSANT N'EST ETABLI MANQUANT")
print("=" * 60)
print(f"\nSonde(s) sans reponse : {', '.join(INDETERMINATE_COMPONENTS)}")
print("Un echec de sonde n'est PAS une absence : ces composants n'ont pas pu")
print("etre mesures, et rien n'a ete installe pour eux.")
print(f"\nRe-executez la cellule de diagnostic (section 2), puis cette cellule.")
INSTALLATION_SUCCESS = True
else:
print("=" * 60)
print("[OK] TOUS LES COMPOSANTS SONT DEJA INSTALLES")
print("=" * 60)
print("\nVotre environnement Lean 4 est pret a l'emploi.")
print("Vous pouvez passer aux notebooks suivants.")
print("\n Notebooks Lean:")
print(" - Lean-02-Dependent-Types-Lean.ipynb")
print(" - Lean-03-Propositions-Proofs-Lean.ipynb")
print(" - Lean-04-Quantifiers-Lean.ipynb")
print(" - Lean-05-Tactics-Lean.ipynb")
print(" - Lean-06-Mathlib-Essentials-Lean.ipynb")
print(" - Lean-07-LLM-Integration-Lean-Python.ipynb")
print(" - Lean-08-Agentic-Proving-Python.ipynb")
print("=" * 60)
INSTALLATION_SUCCESS = True
except NameError:
print("[!] Executez d'abord la cellule de diagnostic (section 2) avant l'installation.")