From 25bb96460455a29630a6ac86af389a0eefd07101 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Sep 2024 11:57:39 -0700 Subject: [PATCH] test: Automatic mode testing refactor: Simplified integration test structure --- Test/Integration.lean | 224 ++++++++++++++++++++++-------------------- Test/Main.lean | 2 +- 2 files changed, 121 insertions(+), 105 deletions(-) diff --git a/Test/Integration.lean b/Test/Integration.lean index 3ccff81..b82962b 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -3,40 +3,23 @@ import LSpec import Pantograph import Repl +import Test.Common namespace Pantograph.Test.Integration open Pantograph -def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json)) - (expected: Lean.Json): MainM LSpec.TestSeq := do - let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload } - return LSpec.test name (toString result = toString expected) -def subroutine_step (cmd: String) (payload: List (String × Lean.Json)) - (expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected +def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json)) + (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do + let payload := Lean.Json.mkObj payload + let name := name?.getD s!"{cmd} {payload.compress}" + let result ← execute { cmd, payload } + return LSpec.test name (toString result = toString (Lean.toJson expected)) -def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do - -- Setup the environment for execution - let env ← Lean.importModules - (imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }]) - (opts := {}) - (trustLevel := 1) - let context: Context := { - imports := ["Init"] - } - let coreContext: Lean.Core.Context ← createCoreContext #[] - let commands: MainM LSpec.TestSeq := - steps.foldlM (λ suite step => do - let result ← step - return suite ++ result) LSpec.TestSeq.done - try - let coreM := commands.run context |>.run' {} - return Prod.fst $ (← coreM.toIO coreContext { env := env }) - catch ex => - return LSpec.check s!"Uncaught IO exception: {ex.toString}" false +abbrev Test := List (MainM LSpec.TestSeq) -def test_elab : IO LSpec.TestSeq := - subroutine_runner [ - subroutine_step "expr.echo" +def test_elab : Test := + [ + step "expr.echo" [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])] (Lean.toJson ({ type := { pp? := .some "{α : Type u} → Type u" }, @@ -44,46 +27,33 @@ def test_elab : IO LSpec.TestSeq := }: Protocol.ExprEchoResult)), ] -def test_option_modify : IO LSpec.TestSeq := +def test_option_modify : Test := let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ" let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))" let module? := Option.some "Init.Data.Nat.Basic" let options: Protocol.Options := {} - subroutine_runner [ - subroutine_step "env.inspect" - [("name", .str "Nat.add_one")] - (Lean.toJson ({ - type := { pp? }, module? }: - Protocol.EnvInspectResult)), - subroutine_step "options.set" - [("printExprAST", .bool true)] - (Lean.toJson ({ }: - Protocol.OptionsSetResult)), - subroutine_step "env.inspect" - [("name", .str "Nat.add_one")] - (Lean.toJson ({ - type := { pp?, sexp? }, module? }: - Protocol.EnvInspectResult)), - subroutine_step "options.print" - [] - (Lean.toJson ({ options with printExprAST := true }: - Protocol.Options)) + [ + step "env.inspect" [("name", .str "Nat.add_one")] + ({ type := { pp? }, module? }: Protocol.EnvInspectResult), + step "options.set" [("printExprAST", .bool true)] + ({ }: Protocol.OptionsSetResult), + step "env.inspect" [("name", .str "Nat.add_one")] + ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult), + step "options.print" [] + ({ options with printExprAST := true }: Protocol.Options), ] -def test_malformed_command : IO LSpec.TestSeq := +def test_malformed_command : Test := let invalid := "invalid" - subroutine_runner [ - subroutine_named_step "Invalid command" invalid - [("name", .str "Nat.add_one")] - (Lean.toJson ({ - error := "command", desc := s!"Unknown command {invalid}"}: - Protocol.InteractionError)), - subroutine_named_step "JSON Deserialization" "expr.echo" - [(invalid, .str "Random garbage data")] - (Lean.toJson ({ - error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}: - Protocol.InteractionError)) + [ + step invalid [("name", .str "Nat.add_one")] + ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError) + (name? := .some "Invalid Command"), + step "expr.echo" [(invalid, .str "Random garbage data")] + ({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }: + Protocol.InteractionError) + (name? := .some "JSON Deserialization") ] -def test_tactic : IO LSpec.TestSeq := +def test_tactic : Test := let goal1: Protocol.Goal := { name := "_uniq.11", target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" }, @@ -97,77 +67,123 @@ def test_tactic : IO LSpec.TestSeq := { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }} ], } - subroutine_runner [ - subroutine_step "goal.start" - [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] - (Lean.toJson ({stateId := 0, root := "_uniq.9"}: - Protocol.GoalStartResult)), - subroutine_step "goal.tactic" - [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] - (Lean.toJson ({ - nextStateId? := .some 1, - goals? := #[goal1], - }: - Protocol.GoalTacticResult)), - subroutine_step "goal.print" - [("stateId", .num 1)] - (Lean.toJson ({ - parent? := .some { pp? := .some "fun x => ?m.12 x" }, - }: - Protocol.GoalPrintResult)), - subroutine_step "goal.tactic" - [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] - (Lean.toJson ({ - nextStateId? := .some 2, - goals? := #[goal2], - }: - Protocol.GoalTacticResult)) + [ + step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] + ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult), + step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] + ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult), + step "goal.print" [("stateId", .num 1)] + ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult), + step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] + ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult), + ] +def test_automatic_mode (automatic: Bool): Test := + let varsPQ := #[ + { name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }}, + { name := "_uniq.13", userName := "q", type? := .some { pp? := .some "Prop" }} + ] + let goal1: Protocol.Goal := { + name := "_uniq.17", + target := { pp? := .some "q ∨ p" }, + vars := varsPQ ++ #[ + { name := "_uniq.16", userName := "h", type? := .some { pp? := .some "p ∨ q" }} + ], + } + let goal2l: Protocol.Goal := { + name := "_uniq.59", + userName? := .some "inl", + target := { pp? := .some "q ∨ p" }, + vars := varsPQ ++ #[ + { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true} + ], + } + let goal2r: Protocol.Goal := { + name := "_uniq.72", + userName? := .some "inr", + target := { pp? := .some "q ∨ p" }, + vars := varsPQ ++ #[ + { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true} + ], + } + let goal3l: Protocol.Goal := { + name := "_uniq.78", + userName? := .some "inl.h", + target := { pp? := .some "p" }, + vars := varsPQ ++ #[ + { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true} + ], + } + [ + step "options.set" [("automaticMode", .bool automatic)] + ({}: Protocol.OptionsSetResult), + step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] + ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult), + step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")] + ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult), + step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")] + ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult), + let goals? := if automatic then #[goal3l, goal2r] else #[goal3l] + step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")] + ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult), ] -def test_env_add_inspect : IO LSpec.TestSeq := +def test_env_add_inspect : Test := let name1 := "Pantograph.mystery" let name2 := "Pantograph.mystery2" - subroutine_runner [ - subroutine_step "env.add" + [ + step "env.add" [ ("name", .str name1), ("type", .str "Prop → Prop → Prop"), ("value", .str "λ (a b: Prop) => Or a b"), ("isTheorem", .bool false) ] - (Lean.toJson ({}: Protocol.EnvAddResult)), - subroutine_step "env.inspect" - [("name", .str name1)] - (Lean.toJson ({ + ({}: Protocol.EnvAddResult), + step "env.inspect" [("name", .str name1)] + ({ value? := .some { pp? := .some "fun a b => a ∨ b" }, type := { pp? := .some "Prop → Prop → Prop" }, }: - Protocol.EnvInspectResult)), - subroutine_step "env.add" + Protocol.EnvInspectResult), + step "env.add" [ ("name", .str name2), ("type", .str "Nat → Int"), ("value", .str "λ (a: Nat) => a + 1"), ("isTheorem", .bool false) ] - (Lean.toJson ({}: Protocol.EnvAddResult)), - subroutine_step "env.inspect" - [("name", .str name2)] - (Lean.toJson ({ + ({}: Protocol.EnvAddResult), + step "env.inspect" [("name", .str name2)] + ({ value? := .some { pp? := .some "fun a => ↑a + 1" }, type := { pp? := .some "Nat → Int" }, }: - Protocol.EnvInspectResult)) + Protocol.EnvInspectResult) ] -def suite: List (String × IO LSpec.TestSeq) := - [ - ("Elab", test_elab), - ("Option modify", test_option_modify), +def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do + -- Setup the environment for execution + let context: Context := { + imports := ["Init"] + } + let commands: MainM LSpec.TestSeq := + steps.foldlM (λ suite step => do + let result ← step + return suite ++ result) LSpec.TestSeq.done + runCoreMSeq env <| commands.run context |>.run' {} + + +def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := + let tests := [ + ("expr.echo", test_elab), + ("options.set options.print", test_option_modify), ("Malformed command", test_malformed_command), ("Tactic", test_tactic), + ("Manual Mode", test_automatic_mode false), + ("Automatic Mode", test_automatic_mode true), ("env.add env.inspect", test_env_add_inspect), ] + tests.map (fun (name, test) => (name, runTest env test)) end Pantograph.Test.Integration diff --git a/Test/Main.lean b/Test/Main.lean index 89c757a..6da6640 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -44,7 +44,7 @@ def main (args: List String) := do let suites: List (String × List (String × IO LSpec.TestSeq)) := [ ("Environment", Environment.suite), - ("Integration", Integration.suite), + ("Integration", Integration.suite env_default), ("Library", Library.suite env_default), ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default),