Add option format for proof output and test cases

This commit is contained in:
Leni Aniva 2023-05-22 14:49:56 -07:00
parent 8a448fb114
commit 111dea2093
10 changed files with 187 additions and 76 deletions

View File

@ -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 := "<Pantograph>",
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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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
```

View File

@ -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

129
Test/Proofs.lean Normal file
View File

@ -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 := "<Pantograph>",
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

10
Test/Serial.lean Normal file
View File

@ -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

3
Test/all.sh Executable file
View File

@ -0,0 +1,3 @@
#!/bin/bash
lake build test && lake env build/bin/test

View File

@ -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
}