From 111dea209341cd89a38dfec30e9249bcc61249aa Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 May 2023 14:49:56 -0700 Subject: [PATCH] Add option format for proof output and test cases --- Examples/Proof.lean | 58 ------------------ Main.lean | 7 ++- Pantograph/Commands.lean | 2 +- Pantograph/Meta.lean | 10 +-- README.md | 18 ++++++ Test/Main.lean | 17 ++++-- Test/Proofs.lean | 129 +++++++++++++++++++++++++++++++++++++++ Test/Serial.lean | 10 +++ Test/all.sh | 3 + lakefile.lean | 9 +-- 10 files changed, 187 insertions(+), 76 deletions(-) delete mode 100644 Examples/Proof.lean create mode 100644 Test/Proofs.lean create mode 100644 Test/Serial.lean create mode 100755 Test/all.sh diff --git a/Examples/Proof.lean b/Examples/Proof.lean deleted file mode 100644 index bafe406..0000000 --- a/Examples/Proof.lean +++ /dev/null @@ -1,58 +0,0 @@ -import Lean -import Pantograph.Meta -import Pantograph.Serial -import Pantograph.Symbols - -open Pantograph - -/- -Example of using the internal API to execute tactics! --/ - -def serialise (result: Meta.TacticResult): String := match result with - | .invalid message => s!"Invalid: {message}" - | .success 0 _ => s!"Completed!" - | .success nextId _ => s!"Success: {nextId}" - | .failure messages => s!"Failures: {messages}" - -def start_proof: IO Meta.ProofTree := do - let imports := ["Init"] - let env: Lean.Environment ← Lean.importModules - (imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false })) - (opts := {}) - (trustLevel := 1) - let name := str_to_name "Nat.add_comm" - let state := Meta.createProofTree - (name := str_to_name "aa") env - (coreContext := { - currNamespace := str_to_name "Aniva", - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] } - }) - let s := "∀ (n m : Nat), n + m = m + n" - let syn: Lean.Syntax := Serial.syntax_from_str env s |>.toOption |>.get! - IO.println "Created syntax" - let expr: Lean.Expr := (← Meta.ProofM.syntax_to_expr syn |>.run' state) |>.toOption |>.get! - IO.println "Created expr" - --let expr := env.find? name |>.get! |>.type - let (_, state) ← Meta.ProofM.start expr |>.run state - return state - -def execute_proof: IO Unit := do - let state ← start_proof - IO.println "Proof state started!" - let tactic := "intro n m" - let (result, state) ← Meta.ProofM.execute 0 tactic |>.run state - IO.println s! "Executed {tactic}, Response: [{serialise result}]" - let tactic := "assumption" -- should fail - let (result, state) ← Meta.ProofM.execute 1 tactic |>.run state - IO.println s! "Executed {tactic}, Response: [{serialise result}]" - let tactic := "rw [Nat.add_comm]" - let (result, state) ← Meta.ProofM.execute 1 tactic |>.run state - IO.println s! "Executed {tactic}, Response: [{serialise result}]" - -unsafe def main : IO Unit := do - Lean.enableInitializersExecution - Lean.initSearchPath (← Lean.findSysroot) - execute_proof diff --git a/Main.lean b/Main.lean index 40bb875..e1e87e6 100644 --- a/Main.lean +++ b/Main.lean @@ -210,10 +210,11 @@ open Pantograph unsafe def loop : Subroutine Unit := do let command ← (← IO.getStdin).getLine + if command.trim.length = 0 then return () match parse_command command with - | .error _ => - -- Halt execution if command is empty - return () + | .error error => + let error := Lean.toJson ({ error := "json", desc := error }: Commands.InteractionError) + IO.println (toString error) | .ok command => let ret ← execute command IO.println <| toString <| ret diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index a4d6a8e..5bdf4fd 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -68,7 +68,7 @@ structure ProofTactic where deriving Lean.FromJson structure ProofTacticResultSuccess where goals: Array String - nextId: Nat + nextId: Option Nat deriving Lean.ToJson structure ProofTacticResultFailure where errorMessages: Array String -- Error messages generated by tactic diff --git a/Pantograph/Meta.lean b/Pantograph/Meta.lean index ccda3d6..486f937 100644 --- a/Pantograph/Meta.lean +++ b/Pantograph/Meta.lean @@ -109,15 +109,17 @@ def execute_tactic (env: Lean.Environment) (state: Lean.Elab.Tactic.SavedState) | .none => return .error #[s!"Invalid goalId {goalId}"] | .some mvarId => try + Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing let unsolvedGoals ← Lean.Elab.Tactic.run mvarId tac if (← getThe Lean.Core.State).messages.hasErrors then let messages := (← getThe Lean.Core.State).messages.getErrorMessages |>.toList.toArray let errors ← (messages.map Lean.Message.data).mapM fun md => md.toString return .error errors else + unsolvedGoals.forM Lean.instantiateMVarDeclMVars let nextState : Lean.Elab.Tactic.SavedState := { term := (← Lean.Elab.Term.saveState), - tactic := { goals := unsolvedGoals} + tactic := { goals := unsolvedGoals } } return .ok nextState catch ex => @@ -134,7 +136,7 @@ inductive TacticResult where -- Invalid id | invalid (message: String): TacticResult -- Goes to next state - | success (nextId: Nat) (goals: Array String) + | success (nextId: Option Nat) (goals: Array String) -- Fails with messages | failure (messages: Array String) @@ -153,7 +155,7 @@ def ProofM.execute (stateId: Nat) (goalId: Nat) (tactic: String): ProofM TacticR let goals ← ProofM.runTermElabM' <| extract_goals nextState if goals.size = 0 then - return .success 0 #[] + return .success .none #[] else -- Create next proof state node let proofState: ProofState := { @@ -163,7 +165,7 @@ def ProofM.execute (stateId: Nat) (goalId: Nat) (tactic: String): ProofM TacticR } modify fun s => { s with states := s.states.push proofState } - return .success nextId goals + return .success (.some nextId) goals end Pantograph.Meta diff --git a/README.md b/README.md index b60886e..617552d 100644 --- a/README.md +++ b/README.md @@ -57,6 +57,15 @@ proof.printTree {"treeId": 0} ``` where the application of `assumption` should lead to a failure. +``` +create {"imports": ["Init"]} +proof.start {"id": 0, "expr": "∀ (p q: Prop), p ∨ q → q ∨ p"} +proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro p q h"} +proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "cases h"} +proof.tactic {"treeId": 0, "stateId": 2, "goalId": 0, "tactic": "apply Or.inr"} +proof.tactic {"treeId": 0, "stateId": 2, "goalId": 0, "tactic": "apply Or.inl"} +``` + ## Troubleshooting If lean encounters stack overflow problems when printing catalog, execute this before running lean: @@ -64,3 +73,12 @@ If lean encounters stack overflow problems when printing catalog, execute this b ulimit -s unlimited ``` Due to a current bug in Lean (which existed in Lean 3), [the default value of structures are not honoured when parsing Json's](https://github.com/leanprover/lean4/issues/2225). + + +## Testing + +The tests are based on `LSpec`. To run tests, +``` sh +test/all.sh +``` + diff --git a/Test/Main.lean b/Test/Main.lean index 5f5fb23..22d8984 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,8 +1,17 @@ import LSpec import Pantograph.Symbols +import Test.Proofs +import Test.Serial -open Pantograph +open Pantograph.Test -def main := do - LSpec.lspecIO $ - LSpec.test "Symbol parsing" (Lean.Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run") +unsafe def main := do + Lean.enableInitializersExecution + Lean.initSearchPath (← Lean.findSysroot) + + let suites := [ + test_serial, + test_proofs + ] + let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done + LSpec.lspecIO $ all diff --git a/Test/Proofs.lean b/Test/Proofs.lean new file mode 100644 index 0000000..f145a27 --- /dev/null +++ b/Test/Proofs.lean @@ -0,0 +1,129 @@ +import LSpec +import Pantograph.Meta +import Pantograph.Serial + +namespace Pantograph.Test +open Pantograph + +inductive Start where + | copy (name: String) -- Start from some name in the environment + | expr (expr: String) -- Start from some expression + +def start_proof (start: Start): IO (LSpec.TestSeq × Option Meta.ProofTree) := do + let imports := ["Init"] + let env: Lean.Environment ← Lean.importModules + (imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false })) + (opts := {}) + (trustLevel := 1) + let state := Meta.createProofTree + (name := str_to_name "TestExample") env + (coreContext := { + currNamespace := str_to_name "Aniva", + openDecls := [], -- No 'open' directives needed + fileName := "", + fileMap := { source := "", positions := #[0], lines := #[1] } + }) + let mut testSeq := LSpec.TestSeq.done + match start with + | .copy name => + let cInfo? := str_to_name name |> env.find? + testSeq := testSeq ++ LSpec.check s!"Symbol exists {name}" cInfo?.isSome + match cInfo? with + | .some cinfo => + let (_, state) ← Meta.ProofM.start cinfo.type |>.run state + return (testSeq, Option.some state) + | .none => + return (testSeq, Option.none) + | .expr expr => + let syn? := Serial.syntax_from_str env expr + testSeq := testSeq ++ LSpec.check s!"Parsing {expr}" (syn?.isOk) + match syn? with + | .error error => + IO.println error + return (testSeq, Option.none) + | .ok syn => + let expr? := (← Meta.ProofM.syntax_to_expr syn |>.run' state) + testSeq := testSeq ++ LSpec.check s!"Elaborating" expr?.isOk + match expr? with + | .error error => + IO.println error + return (testSeq, Option.none) + | .ok expr => + let (_, state) ← Meta.ProofM.start expr |>.run state + return (testSeq, Option.some state) + +deriving instance DecidableEq, Repr for Meta.TacticResult + +def proof_step (stateId: Nat) (goalId: Nat) (tactic: String) + (expected: Meta.TacticResult) : Meta.ProofM LSpec.TestSeq := do + let result: Meta.TacticResult ← Meta.ProofM.execute stateId goalId tactic + match expected, result with + | .success (.some i) #[], .success (.some _) goals => + -- If the goals are omitted but the next state is specified, we imply that + -- the tactic succeeded. + let expected := .success (.some i) goals + return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected) + | _, _ => + return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected) + +def proof_runner (start: Start) (steps: List (Meta.ProofM LSpec.TestSeq)): IO LSpec.TestSeq := do + let (testSeq, state?) ← start_proof start + match state? with + | .none => return testSeq + | .some state => steps.foldlM (fun tests m => do pure $ tests ++ (← m)) testSeq |>.run' state + +example: ∀ (a b: Nat), a + b = b + a := by + intro n m + rw [Nat.add_comm] +def proof_nat_add_comm: IO LSpec.TestSeq := + let goal1 := "n m : Nat\n⊢ n + m = m + n" + proof_runner (.copy "Nat.add_comm") [ + proof_step 0 0 "intro n m" + (.success (.some 1) #[goal1]), + proof_step 1 0 "assumption" + (.failure #[s!"tactic 'assumption' failed\n{goal1}"]), + proof_step 1 0 "rw [Nat.add_comm]" + (.success .none #[]) + ] +def proof_nat_add_comm_manual: IO LSpec.TestSeq := do + let goal1 := "n m : Nat\n⊢ n + m = m + n" + proof_runner (.expr "∀ (a b: Nat), a + b = b + a") [ + proof_step 0 0 "intro n m" + (.success (.some 1) #[goal1]), + proof_step 1 0 "assumption" + (.failure #[s!"tactic 'assumption' failed\n{goal1}"]), + proof_step 1 0 "rw [Nat.add_comm]" + (.success .none #[]) + ] + +example: ∀ (p q: Prop), p ∨ q → q ∨ p := by + intro p q h + cases h + apply Or.inr + assumption + apply Or.inl + assumption +def proof_or_comm: IO LSpec.TestSeq := do + proof_runner (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") [ + proof_step 0 0 "intro p q h" + (.success (.some 1) #["p q : Prop\nh : p ∨ q\n⊢ q ∨ p"]), + proof_step 1 0 "cases h" + (.success (.some 2) #[]), + proof_step 2 0 "apply Or.inr" + (.success (.some 3) #[]), + proof_step 3 0 "assumption" + (.success .none #[]), + proof_step 2 1 "apply Or.inl" + (.success (.some 4) #[]), + proof_step 4 0 "assumption" + (.success .none #[]) + ] + +def test_proofs : IO LSpec.TestSeq := do + return LSpec.group "proofs" $ + (LSpec.group "Nat.add_comm" $ (← proof_nat_add_comm)) ++ + (LSpec.group "Nat.add_comm manual" $ (← proof_nat_add_comm_manual)) ++ + (LSpec.group "Or.comm" $ (← proof_or_comm)) + +end Pantograph.Test + diff --git a/Test/Serial.lean b/Test/Serial.lean new file mode 100644 index 0000000..ce4114a --- /dev/null +++ b/Test/Serial.lean @@ -0,0 +1,10 @@ +import LSpec +import Pantograph.Symbols + +namespace Pantograph.Test + +def test_serial: IO LSpec.TestSeq := do + return LSpec.group "Serialisation" $ + LSpec.test "Symbol parsing" (Lean.Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run") + +end Pantograph.Test diff --git a/Test/all.sh b/Test/all.sh new file mode 100755 index 0000000..9d940bd --- /dev/null +++ b/Test/all.sh @@ -0,0 +1,3 @@ +#!/bin/bash + +lake build test && lake env build/bin/test diff --git a/lakefile.lean b/lakefile.lean index 83efa04..458c2ac 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -19,15 +19,12 @@ lean_exe pantograph { require LSpec from git "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41" +lean_lib Test { + -- add library configuration options here +} lean_exe test { root := `Test.Main -- Somehow solves the native symbol not found problem supportInterpreter := true } - -lean_exe examples_proof { - root := `Examples.Proof - -- Somehow solves the native symbol not found problem - supportInterpreter := true -}