Pantograph.lean

@@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
-    exprEcho args.expr args.type? state.options
+    exprEcho args.expr state.options
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options
@@ -93,7 +93,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none => goalStartExpr expr
+      | .some expr, .none => do
+        let expr ← match ← exprParse expr with
+          | .error e => return .error e
+          | .ok expr => pure $ expr
+        return .ok $ ← GoalState.create expr
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
@@ -148,7 +152,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         | .some branchId, .none => do
           match state.goalStates.find? branchId with
           | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
-          | .some branch => pure $ goalContinue target branch
+          | .some branch => pure $ target.continue branch
         | .none, .some goals =>
           pure $ goalResume target goals
         | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"

Pantograph/Environment.lean

@@ -69,8 +69,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       else pure (.none),
     module? := module?
   }
-  let result ← match info with
-    | .inductInfo induct => pure { core with inductInfo? := .some {
+  let result := match info with
+    | .inductInfo induct => { core with inductInfo? := .some {
           numParams := induct.numParams,
           numIndices := induct.numIndices,
           all := induct.all.toArray.map (·.toString),
@@ -79,38 +79,32 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           isReflexive := induct.isReflexive,
           isNested := induct.isNested,
       } }
-    | .ctorInfo ctor => pure { core with constructorInfo? := .some {
+    | .ctorInfo ctor => { core with constructorInfo? := .some {
           induct := ctor.induct.toString,
           cidx := ctor.cidx,
           numParams := ctor.numParams,
           numFields := ctor.numFields,
       } }
-    | .recInfo r => pure { core with recursorInfo? := .some {
+    | .recInfo r => { core with recursorInfo? := .some {
           all := r.all.toArray.map (·.toString),
           numParams := r.numParams,
           numIndices := r.numIndices,
           numMotives := r.numMotives,
           numMinors := r.numMinors,
-          rules := ← r.rules.toArray.mapM (λ rule => do
-              pure {
-                ctor := rule.ctor.toString,
-                nFields := rule.nfields,
-                rhs := ← (serialize_expression options rule.rhs).run',
-              })
           k := r.k,
       } }
-    | _ => pure core
+    | _ => core
   return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
   let env ← Lean.MonadEnv.getEnv
   let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
-    let type ← match parseTerm env args.type with
+    let type ← match syntax_from_str env args.type with
       | .ok syn => do
-        match ← elabTerm syn with
+        match ← syntax_to_expr syn with
         | .error e => return .error e
         | .ok expr => pure expr
       | .error e => return .error e
-    let value ← match parseTerm env args.value with
+    let value ← match syntax_from_str env args.value with
       | .ok syn => do
         try
           let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)

Pantograph/Library.lean

@@ -36,15 +36,13 @@ end Lean
 
 namespace Pantograph
 
-def defaultTermElabMContext: Lean.Elab.Term.Context := {
-    autoBoundImplicit := true,
-    declName? := some "_pantograph".toName,
-    errToSorry := false
-  }
 def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
   metaM.run'
 def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
-  termElabM.run' (ctx := defaultTermElabMContext) |>.run'
+  termElabM.run' (ctx := {
+    declName? := .none,
+    errToSorry := false,
+  }) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 
@@ -111,34 +109,21 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
     Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
   Environment.addDecl { name, type, value, isTheorem }
 
-def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
-  let env ← Lean.MonadEnv.getEnv
-  let syn ← match parseTerm env type with
-    | .error str => return .error $ errorI "parsing" str
-    | .ok syn => pure syn
-  match ← elabType syn with
-  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← Lean.instantiateMVars expr)
-
 /-- This must be a TermElabM since the parsed expr contains extra information -/
-def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
+def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
   let env ← Lean.MonadEnv.getEnv
-  let expectedType? ← match ← expectedType?.mapM parseElabType with
-    | .none => pure $ .none
-    | .some (.ok t) => pure $ .some t
-    | .some (.error e) => return .error e
-  let syn ← match parseTerm env expr with
+  let syn ← match syntax_from_str env s with
     | .error str => return .error $ errorI "parsing" str
     | .ok syn => pure syn
-  match ← elabTerm syn expectedType? with
+  match ← syntax_to_expr syn with
   | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← Lean.instantiateMVars expr)
+  | .ok expr => return .ok expr
 
 @[export pantograph_expr_echo_m]
-def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
+def exprEcho (expr: String) (options: @&Protocol.Options):
     Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
   let termElabM: Lean.Elab.TermElabM _ := do
-    let expr ← match ← parseElabExpr expr expectedType? with
+    let expr ← match ← exprParse expr with
       | .error e => return .error e
       | .ok expr => pure expr
     try
@@ -154,7 +139,7 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&
 @[export pantograph_goal_start_expr_m]
 def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
   let termElabM: Lean.Elab.TermElabM _ := do
-    let expr ← match ← parseElabType expr with
+    let expr ← match ← exprParse expr with
       | .error e => return .error e
       | .ok expr => pure $ expr
     return .ok $ ← GoalState.create expr

Pantograph/Protocol.lean

@@ -98,7 +98,6 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
-  type?: Option String
   deriving Lean.FromJson
 structure ExprEchoResult where
   expr: Expression
@@ -138,20 +137,12 @@ structure ConstructorInfo where
   numParams: Nat
   numFields: Nat
   deriving Lean.ToJson
-
-/-- See `Lean/Declaration.lean` -/
-structure RecursorRule where
-  ctor: String
-  nFields: Nat
-  rhs: Expression
-  deriving Lean.ToJson
 structure RecursorInfo where
   all: Array String
   numParams: Nat
   numIndices: Nat
   numMotives: Nat
   numMinors: Nat
-  rules: Array RecursorRule
   k: Bool
   deriving Lean.ToJson
 structure EnvInspectResult where

Pantograph/Serial.lean

@@ -21,22 +21,23 @@ def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do
 --- Input Functions ---
 
 /-- Read syntax object from string -/
-def parseTerm (env: Environment) (s: String): Except String Syntax :=
+def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
   Parser.runParserCategory
     (env := env)
     (catName := `term)
     (input := s)
     (fileName := "<stdin>")
 
+
 /-- Parse a syntax object. May generate additional metavariables! -/
-def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
   try
     let expr ← Elab.Term.elabType syn
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
-def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
+def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
   try
-    let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
+    let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
 
@@ -160,12 +161,14 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
   of_name (name: Name) := name_to_ast name sanitize
 
 def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
-  let pp?: Option String ← match options.printExprPretty with
-    | true => pure $ .some $ toString $ ← Meta.ppExpr e
-    | false => pure $ .none
-  let sexp?: Option String ← match options.printExprAST with
-    | true => pure $ .some $ ← serialize_expression_ast e
-    | false => pure $ .none
+  let pp := toString (← Meta.ppExpr e)
+  let pp?: Option String := match options.printExprPretty with
+    | true => .some pp
+    | false => .none
+  let sexp: String ← serialize_expression_ast e
+  let sexp?: Option String := match options.printExprAST with
+    | true => .some sexp
+    | false => .none
   return {
     pp?,
     sexp?

README.md

@@ -72,7 +72,7 @@ where the application of `assumption` should lead to a failure.
 
 See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
 - `reset`: Delete all cached expressions and proof trees
-- `expr.echo {"expr": <expr>, "type": <optional expected type>}`: Determine the type of an expression and round-trip it
+- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
 - `env.catalog`: Display a list of all safe Lean symbols in the current environment
 - `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
   given symbol; If value flag is set, the value is printed or hidden. By default
@@ -132,5 +132,8 @@ requires the presence of `lean-all`.
 
 To run tests:
 ``` sh
-nix flake check
+nix build .#checks.${system}.test
 ```
+
+For example, `${system}` could be `x86_64-linux`. Using `nix develop` drops the
+current session into a development shell with fixed Lean version.

Test/Common.lean

@@ -8,7 +8,6 @@ open Lean
 
 namespace Pantograph
 
--- Auxiliary functions
 namespace Protocol
 /-- Set internal names to "" -/
 def Goal.devolatilize (goal: Goal): Goal :=
@@ -25,9 +24,6 @@ def Goal.devolatilize (goal: Goal): Goal :=
 deriving instance DecidableEq, Repr for Expression
 deriving instance DecidableEq, Repr for Variable
 deriving instance DecidableEq, Repr for Goal
-deriving instance DecidableEq, Repr for ExprEchoResult
-deriving instance DecidableEq, Repr for InteractionError
-deriving instance DecidableEq, Repr for Option
 end Protocol
 
 def TacticResult.toString : TacticResult → String
@@ -38,16 +34,12 @@ def TacticResult.toString : TacticResult → String
   | .parseError error => s!".parseError {error}"
   | .indexError index => s!".indexError {index}"
 
-namespace Test
-
-def expectationFailure (desc: String) (error: String): LSpec.TestSeq := LSpec.test desc (LSpec.ExpectationFailure "ok _" error)
 def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
-def parseFailure (error: String) := expectationFailure "parse" error
-def elabFailure (error: String) := expectationFailure "elab" error
+open Lean
 
-def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
-  let coreContext: Core.Context ← createCoreContext options
+def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do
+  let coreContext: Core.Context ← createCoreContext #[]
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
@@ -55,8 +47,14 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
   runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
+  termElabM.run' (ctx := {
+    declName? := .none,
+    errToSorry := false,
+  })
 
-end Test
+def defaultTermElabMContext: Lean.Elab.Term.Context := {
+    declName? := some "_pantograph".toName,
+    errToSorry := false
+  }
 
 end Pantograph

Test/Environment.lean

@@ -11,7 +11,6 @@ open Pantograph
 
 deriving instance DecidableEq, Repr for Protocol.InductInfo
 deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
-deriving instance DecidableEq, Repr for Protocol.RecursorRule
 deriving instance DecidableEq, Repr for Protocol.RecursorInfo
 deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
 
@@ -70,7 +69,6 @@ def test_inspect: IO LSpec.TestSeq := do
       numIndices := 1,
       numMotives := 1,
       numMinors := 1,
-      rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
       k := true,
     }),
     ("ForM.rec", ConstantCat.recursor {
@@ -79,7 +77,6 @@ def test_inspect: IO LSpec.TestSeq := do
       numIndices := 0,
       numMotives := 1,
       numMinors := 1,
-      rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
       k := false,
     })
   ]
@@ -97,11 +94,10 @@ def test_inspect: IO LSpec.TestSeq := do
     ) LSpec.TestSeq.done
   runCoreMSeq env inner
 
-def suite: List (String × IO LSpec.TestSeq) :=
-  [
-    ("Catalog", test_catalog),
-    ("Symbol Visibility", test_symbol_visibility),
-    ("Inspect", test_inspect),
-  ]
+def suite: IO LSpec.TestSeq := do
+  return LSpec.group "Environment" $
+    (LSpec.group "Catalog" (← test_catalog)) ++
+    (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
+    (LSpec.group "Inspect" (← test_inspect))
 
 end Pantograph.Test.Environment

Test/Integration.lean

@@ -32,16 +32,6 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
   catch ex =>
     return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
 
-def test_elab : IO LSpec.TestSeq :=
-  subroutine_runner [
-    subroutine_step "expr.echo"
-      [("expr", .str "λ {α : Sort (u + 1)} => List α")]
-     (Lean.toJson ({
-       type := { pp? := .some "{α : Type u} → Type u" },
-       expr := { pp? := .some "fun {α} => List α" }
-     }: Protocol.ExprEchoResult)),
-  ]
-
 def test_option_modify : IO LSpec.TestSeq :=
   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)))"
@@ -83,22 +73,22 @@ def test_malformed_command : IO LSpec.TestSeq :=
   ]
 def test_tactic : IO LSpec.TestSeq :=
   let goal1: Protocol.Goal := {
-    name := "_uniq.11",
+    name := "_uniq.10",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
+    vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
   }
   let goal2: Protocol.Goal := {
-    name := "_uniq.14",
+    name := "_uniq.13",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
-      { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.12", userName := "y", isInaccessible? := .some false, 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"}:
+     (Lean.toJson ({stateId := 0, root := "_uniq.8"}:
       Protocol.GoalStartResult)),
     subroutine_step "goal.tactic"
       [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
@@ -110,7 +100,7 @@ def test_tactic : IO LSpec.TestSeq :=
     subroutine_step "goal.print"
       [("stateId", .num 1)]
      (Lean.toJson ({
-       parent? := .some { pp? := .some "fun x => ?m.12 x" },
+       parent? := .some { pp? := .some "fun x => ?m.11 x" },
      }:
       Protocol.GoalPrintResult)),
     subroutine_step "goal.tactic"
@@ -122,7 +112,7 @@ def test_tactic : IO LSpec.TestSeq :=
       Protocol.GoalTacticResult))
   ]
 
-def test_env_add_inspect : IO LSpec.TestSeq :=
+def test_env : IO LSpec.TestSeq :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
   subroutine_runner [
@@ -158,14 +148,13 @@ def test_env_add_inspect : IO LSpec.TestSeq :=
       Protocol.EnvInspectResult))
   ]
 
-def suite: List (String × IO LSpec.TestSeq) :=
-  [
-    ("Elab", test_elab),
-    ("Option modify", test_option_modify),
-    ("Malformed command", test_malformed_command),
-    ("Tactic", test_tactic),
-    ("env.add env.inspect", test_env_add_inspect),
-  ]
+def suite: IO LSpec.TestSeq := do
+
+  return LSpec.group "Integration" $
+    (LSpec.group "Option modify" (← test_option_modify)) ++
+    (LSpec.group "Malformed command" (← test_malformed_command)) ++
+    (LSpec.group "Tactic" (← test_tactic)) ++
+    (LSpec.group "Env" (← test_env))
 
 
 end Pantograph.Test.Integration

Test/Library.lean

@@ -1,38 +0,0 @@
-import LSpec
-import Lean
-import Pantograph.Library
-import Test.Common
-
-open Lean
-open Pantograph
-
-namespace Pantograph.Test.Library
-
-def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
-  let inner: CoreM LSpec.TestSeq := do
-    let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
-    let tests := LSpec.TestSeq.done
-    let echoResult ← exprEcho prop_and_proof (options := {})
-    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
-      type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
-    }))
-    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
-    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
-      type := {
-        pp? := "(p : Prop) ×' p",
-        sexp? := "((:c PSigma) (:sort 0) (:lambda p (:sort 0) 0))",
-      },
-      expr := {
-        pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
-        sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
-      }
-    }))
-    return tests
-  runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("expr_echo", test_expr_echo env),
-  ]
-
-end Pantograph.Test.Library

Test/Main.lean

@@ -1,53 +1,21 @@
 import LSpec
 import Test.Environment
-import Test.Integration
-import Test.Library
 import Test.Metavar
+import Test.Integration
 import Test.Proofs
 import Test.Serial
 
--- Test running infrastructure
-
-namespace Pantograph.Test
-
-def addPrefix (pref: String) (tests: List (String × α)): List (String  × α) :=
-  tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
-
-/-- Runs test in parallel. Filters test name if given -/
-def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
-  let tests: List (String × IO LSpec.TestSeq) := match filter with
-    | .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
-    | .none => tests
-  let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
-    return (name, ← EIO.asTask task))
-  let all := tasks.foldl (λ acc (name, task) =>
-    let v: Except IO.Error LSpec.TestSeq := Task.get task
-    match v with
-    | .ok case => acc ++ (LSpec.group name case)
-    | .error e => acc ++ (expectationFailure name e.toString)
-    ) LSpec.TestSeq.done
-  return all
-
-end Pantograph.Test
-
 open Pantograph.Test
 
-/-- Main entry of tests; Provide an argument to filter tests by prefix -/
-def main (args: List String) := do
-  let name_filter := args.head?
+def main := do
   Lean.initSearchPath (← Lean.findSysroot)
-  let env_default: Lean.Environment ← Lean.importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
 
-  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
-    ("Environment", Environment.suite),
-    ("Integration", Integration.suite),
-    ("Library", Library.suite env_default),
-    ("Metavar", Metavar.suite env_default),
-    ("Proofs", Proofs.suite env_default),
-    ("Serial", Serial.suite env_default),
+  let suites := [
+    Metavar.suite,
+    Integration.suite,
+    Proofs.suite,
+    Serial.suite,
+    Environment.suite
   ]
-  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
-  LSpec.lspecIO (← runTestGroup name_filter tests)
+  let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
+  LSpec.lspecIO $ all

Test/Metavar.lean

@@ -17,12 +17,12 @@ def addTest (test: LSpec.TestSeq): TestM Unit := do
 def test_instantiate_mvar: TestM Unit := do
   let env ← Lean.MonadEnv.getEnv
   let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
-  let syn ← match parseTerm env value with
+  let syn ← match syntax_from_str env value with
     | .ok s => pure $ s
     | .error e => do
       addTest $ assertUnreachable e
       return ()
-  let expr ← match ← elabTerm syn with
+  let expr ← match ← syntax_to_expr syn with
     | .ok expr => pure $ expr
     | .error e => do
       addTest $ assertUnreachable e
@@ -36,14 +36,14 @@ def test_instantiate_mvar: TestM Unit := do
 
 def startProof (expr: String): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
-  let syn? := parseTerm env expr
+  let syn? := syntax_from_str env expr
   addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
   match syn? with
   | .error error =>
     IO.println error
     return Option.none
   | .ok syn =>
-    let expr? ← elabType syn
+    let expr? ← syntax_to_expr_type syn
     addTest $ LSpec.check s!"Elaborating" expr?.isOk
     match expr? with
     | .error error =>
@@ -268,7 +268,11 @@ def test_partial_continuation: TestM Unit := do
   return ()
 
 
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+def suite: IO LSpec.TestSeq := do
+  let env: Lean.Environment ← Lean.importModules
+    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
   let tests := [
     ("Instantiate", test_instantiate_mvar),
     ("2 < 5", test_m_couple),
@@ -276,6 +280,11 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Proposition Generation", test_proposition_generation),
     ("Partial Continuation", test_partial_continuation)
   ]
-  tests.map (fun (name, test) => (name, proofRunner env test))
+  let tests ← tests.foldlM (fun acc tests => do
+    let (name, tests) := tests
+    let tests ← proofRunner env tests
+    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
+
+  return LSpec.group "Metavar" tests
 
 end Pantograph.Test.Metavar

Test/Proofs.lean

@@ -32,14 +32,14 @@ def startProof (start: Start): TestM (Option GoalState) := do
     | .none =>
       return Option.none
   | .expr expr =>
-    let syn? := parseTerm env expr
+    let syn? := syntax_from_str env expr
     addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
     match syn? with
     | .error error =>
       IO.println error
       return Option.none
     | .ok syn =>
-      let expr? ← elabType syn
+      let expr? ← syntax_to_expr_type syn
       addTest $ LSpec.check s!"Elaborating" expr?.isOk
       match expr? with
       | .error error =>
@@ -293,7 +293,12 @@ def proof_or_comm: TestM Unit := do
       ]
     }
 
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+
+def suite: IO LSpec.TestSeq := do
+  let env: Lean.Environment ← Lean.importModules
+    (imports := #[{ module := "Init".toName, runtimeOnly := false}])
+    (opts := {})
+    (trustLevel := 1)
   let tests := [
     ("Nat.add_comm", proof_nat_add_comm false),
     ("Nat.add_comm manual", proof_nat_add_comm true),
@@ -301,6 +306,11 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("arithmetic", proof_arith),
     ("Or.comm", proof_or_comm)
   ]
-  tests.map (fun (name, test) => (name, proofRunner env test))
+  let tests ← tests.foldlM (fun acc tests => do
+    let (name, tests) := tests
+    let tests ← proofRunner env tests
+    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
+
+  return LSpec.group "Proofs" tests
 
 end Pantograph.Test.Proofs

Test/Serial.lean

@@ -51,18 +51,12 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
 def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
     ("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
-    ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
-    -- This tests `autoBoundImplicit`
-    ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))")
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
     let env ← MonadEnv.getEnv
-    let s ← match parseTerm env source with
-      | .ok s => pure s
-      | .error e => return parseFailure e
-    let expr ← match (← elabTerm s) with
-      | .ok expr => pure expr
-      | .error e => return elabFailure e
+    let s := syntax_from_str env source |>.toOption |>.get!
+    let expr := (← syntax_to_expr s) |>.toOption |>.get!
     let test := LSpec.check source ((← serialize_expression_ast expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   let metaM := termElabM.run' (ctx := defaultTermElabMContext)
@@ -73,18 +67,22 @@ def test_instance (env: Environment): IO LSpec.TestSeq := do
   let metaM: MetaM LSpec.TestSeq := do
     let env ← MonadEnv.getEnv
     let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
-    let s := parseTerm env source |>.toOption |>.get!
-    let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
+    let s := syntax_from_str env source |>.toOption |>.get!
+    let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
     return LSpec.TestSeq.done
   runMetaMSeq env metaM
 
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("name_to_ast", do pure test_name_to_ast),
-    ("Expression binder", test_expr_to_binder env),
-    ("Sexp from symbol", test_sexp_of_symbol env),
-    ("Sexp from expr", test_sexp_of_expr env),
-    ("Instance", test_instance env),
-  ]
+def suite: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+
+  return LSpec.group "Serialization" $
+    (LSpec.group "name_to_ast" test_name_to_ast) ++
+    (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
+    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) ++
+    (LSpec.group "Sexp from expr" (← test_sexp_of_expr env)) ++
+    (LSpec.group "Instance" (← test_instance env))
 
 end Pantograph.Test.Serial