Installer et vérifier

Accès

Le dépôt de Slean est privé pour l’instant. L’accès est donné sur demande.

Prérequis

• Lean, installé avec elan.
• Python 3.11 ou plus récent. Le moteur n’a aucune dépendance.

Vérifier la bibliothèque

À la racine du dépôt :

lake build

Cette commande fait vérifier par le noyau de Lean le cœur de Slean et les 84 lois de la bibliothèque, en une vingtaine de secondes. Seuls les axiomes standard sont utilisés.

Lancer les tests du moteur

cd engine
python3 -m unittest discover -s tests

Ces tests vérifient le moteur, et l’accord entre le moteur et les définitions Lean.

Vérifier une première loi

python3 -m slean check 184 1 0,1

La question posée : dans la règle 184, la densité de largeur 1 qui vaut 0 pour une case vide et 1 pour une voiture est-elle conservée ? Autrement dit, le nombre de voitures change-t-il ? Le moteur répond par un verdict au format JSON, certified ici, avec le courant trouvé, puis imprime le théorème Lean correspondant. Avec une affirmation fausse, comme python3 -m slean check 30 1 0,1, le verdict est refuted et le théorème contient le contre-exemple.

Le courant imprimé peut différer de celui de la page Le trafic d’une constante : les deux sont valables.