SleanSlean

5. Format et API🔗

Choisir la commande selon la question

  • validate <dossier.json> : le dossier respecte-t-il les règles prises en charge ? La sortie contient ok: true ou une erreur avec code, event_id et object_id ; une erreur donne un code de sortie non nul.

  • replay <dossier.json> <N> : quel était l'état après les N premiers événements ?

  • view <dossier.json> agent|owner : quelles observations, décisions et relations sont visibles pour cette audience ?

  • export <dossier.json> agent|owner : produire une enveloppe versionnée avec le dossier canonique et la version de Lean. Révisez le contenu avant partage. Utilisez export-case seulement si un consommateur attend l'ancien dossier brut.

  • timeline <dossier.json> agent|owner : obtenir les états vérifiés de tous les préfixes visibles, utilisés par l'Explorer local.

  • proof <dossier.json> et proof-statement : examiner les déclarations, leur admissibilité locale à l'attestation, les dépendances du projet et l'unique énoncé de théorème fixé par le projet. Sur un commit propre, python3 tools/attest_proof.py examples/formal-claim.json n'émet kernel_checked qu'avec les empreintes du build exact et de l'export filtré pour son public. Lake, le CLI et ce script Python restent dans la chaîne de confiance ; il ne s'agit pas d'une revérification indépendante.

Les commandes qui lisent un dossier acceptent aussi - comme chemin d'entrée standard. Par exemple, depuis la racine du dépôt :

lake exe slean view examples/valid.json agent

examples/valid.json est au schéma 0.1.0. Le schéma 0.2.0 ajoute les enregistrements source réservés au propriétaire ; 0.3.0 ajoute dependency_gate_recorded avec all_of ou any_of. Dans chaque dossier, schema_version et semantics_version doivent former une paire prise en charge ; Slean ne migre pas un dossier implicitement. Consultez schema/v0.1.0.schema.json, schema/v0.2.0.schema.json et schema/v0.3.0.schema.json dans le dépôt pour les champs exacts. Les nombres décimaux exacts, comme "0.002", sont des chaînes ; null reste distinct de "0".

Si vous écrivez du Lean

L'API typée permet de construire le même type de dossier. Ces déclarations sont vérifiées lors de la compilation de ce manuel :

Slean.CaseFile : Type#check Slean.CaseFile Slean.replay (caseFile : Slean.CaseFile) (count : Nat := caseFile.events.size) : Except Slean.Diagnostic Slean.State#check Slean.replay Slean.assessExact (protocol : Slean.FrozenProtocol) (observation : Slean.Observation) : Except String String#check Slean.assessExact Slean.project (caseFile : Slean.CaseFile) (audience : String) : Slean.CaseFile#check Slean.project Slean.DependencyGate : Type#check Slean.DependencyGate

examples/Synthetic.lean contient le cas typé complet. bash tests/check.sh le compile et compare ses octets à la projection export-case agent de la fixture JSON. Un statut de preuve importé depuis JSON n'accorde jamais kernel_checked ; le CLI conserve aussi une déclaration locale concordante à declared jusqu'à ce que l'attestation sur un build propre relie son reçu aux artefacts exacts.