1. Commencer par un cas vérifié🔗

Préparer la copie locale

Il vous faut une copie autorisée de ce dépôt et elan, qui fournit Lean et Lake. Suivez les instructions officielles d'installation de Lean si ces outils ne sont pas installés. Le fichier lean-toolchain du dépôt sélectionne Lean 4.28.0. Cette prévisualisation n'est pas encore une installation publique anonyme.

Ouvrez un terminal à la racine du dépôt, là où se trouvent lakefile.toml et examples/valid.json, puis exécutez :

lake build
lake exe slean validate examples/valid.json

Résultat attendu de validate :

{"case_id":"synthetic-decision-1","events":10,"ok":true}

events: 10 compte les entrées du journal complet, dont deux réservées au propriétaire. Cela ne représente ni dix expériences ni dix résultats confirmés.

Lire le résultat plutôt que le seul « ok »

Affichez la vue destinée à un agent :

lake exe slean view examples/valid.json agent

Dans le JSON renvoyé, repérez observations[0] (status: "measured", value: "0.002", unit: "ratio") et decisions[0] (result: "promote"). La valeur reste une chaîne décimale pour éviter un arrondi implicite. L'événement qui fixe la règle est event-1 ; l'observation est event-4, l'évaluation event-6 et la décision event-7.

Vous avez ainsi répondu à une question précise : la promotion annoncée suit-elle une observation antérieure conforme au protocole figé ? Pour cet exemple synthétique, oui. Le chapitre suivant montre les liens et le calcul que Slean vérifie. La réussite de validate ne certifie pas le capteur, le fichier d'artefact ou la vérité de l'affirmation.

Voir un refus concret

Exécutez une copie de l'exemple dont l'unité de mesure a été modifiée :

lake exe slean validate examples/unit-mismatch.json

La commande sort avec un code non nul et affiche :

{"error":{"code":"metric_unit","event_id":"event-4","message":"observation metric or unit differs from frozen protocol","object_id":"observation-1"},"ok":false}

event_id situe l'échec dans le journal ; metric_unit indique que la métrique ou l'unité de l'observation ne correspond plus au protocole. Vous pouvez maintenant lire la décision pour distinguer une erreur de dossier d'un résultat simplement inconnu.