Pantograph/Library.lean

@@ -72,6 +72,7 @@ def createCoreState (imports: Array String): IO Core.State := do
     (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
+    (loadExts := true)
   return { env := env }
 
 @[export pantograph_parse_elab_type_m]

Pantograph/Serial.lean

@@ -63,7 +63,7 @@ def resurrectEnvironment
   (imports : Array Import)
   (map₂ : PHashMap Name ConstantInfo)
   : IO Environment := do
-  let env ← importModules imports {} 0
+  let env ← importModules imports {} 0 (loadExts := true)
   env.replay (Std.HashMap.ofList map₂.toList)
 /--
 Unpickle an `Environment` from disk.

Repl.lean

@@ -14,7 +14,7 @@ structure Context where
 structure State where
   options : Protocol.Options := {}
   nextId : Nat := 0
-  goalStates : Std.HashMap Nat GoalState := Std.HashMap.empty
+  goalStates : Std.HashMap Nat GoalState := Std.HashMap.emptyWithCapacity
 
   env : Environment
   -- Parser state
@@ -227,7 +227,7 @@ def execute (command: Protocol.Command): MainM Json := do
   reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
     let state ← getMainState
     let nGoals := state.goalStates.size
-    set { state with nextId := 0, goalStates := .empty }
+    set { state with nextId := 0, goalStates := .emptyWithCapacity }
     return { nGoals }
   stat (_: Protocol.Stat): EMainM Protocol.StatResult := do
     let state ← getMainState

Test/Environment.lean

@@ -15,11 +15,7 @@ deriving instance DecidableEq, Repr for Protocol.RecursorRule
 deriving instance DecidableEq, Repr for Protocol.RecursorInfo
 deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
 
-def test_catalog: IO LSpec.TestSeq := do
+def test_catalog (env : Environment) : IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
   let inner: CoreM LSpec.TestSeq := do
     let catalogResult ← Environment.catalog {}
     let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info =>
@@ -46,11 +42,7 @@ inductive ConstantCat where
   | ctor (info: Protocol.ConstructorInfo)
   | recursor (info: Protocol.RecursorInfo)
 
-def test_inspect: IO LSpec.TestSeq := do
+def test_inspect (env : Environment) : IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
   let testCases: List (String × ConstantCat) := [
     ("Or", ConstantCat.induct {
       numParams := 2,
@@ -97,11 +89,7 @@ def test_inspect: IO LSpec.TestSeq := do
     ) LSpec.TestSeq.done
   runCoreMSeq env inner
 
-def test_symbol_location : TestT IO Unit := do
+def test_symbol_location (env : Environment) : TestT IO Unit := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
   addTest $ ← runTestCoreM env do
     let .ok result ← (Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {})).run | fail "Inspect failed"
     checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
@@ -114,20 +102,16 @@ def test_symbol_location : TestT IO Unit := do
     checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
     checkTrue "constNames" $ constNames.contains "Nat.succ_add"
 
-def test_matcher : TestT IO Unit := do
+def test_matcher (env : Environment) : TestT IO Unit := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
   checkTrue "not matcher" $ ¬ Meta.isMatcherCore env `Nat.strongRecOn
 
-def suite: List (String × IO LSpec.TestSeq) :=
+def suite (env : Environment) : List (String × IO LSpec.TestSeq) :=
   [
-    ("Catalog", test_catalog),
+    ("Catalog", test_catalog env),
     ("Symbol Visibility", test_symbol_visibility),
-    ("Inspect", test_inspect),
+    ("Inspect", test_inspect env),
-    ("Symbol Location", runTest test_symbol_location),
+    ("Symbol Location", runTest $ test_symbol_location env),
-    ("Matcher", runTest test_matcher),
+    ("Matcher", runTest $ test_matcher env),
   ]
 
 end Pantograph.Test.Environment

Test/Main.lean

@@ -43,19 +43,23 @@ def main (args: List String) := do
     (imports := #[`Init])
     (opts := {})
     (trustLevel := 1)
+    (loadExts := true)
 
-  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
+  let suites: List (String × (Lean.Environment → List (String × IO LSpec.TestSeq))) := [
     ("Environment", Environment.suite),
-    ("Frontend", Frontend.suite env_default),
+    ("Frontend", Frontend.suite),
-    ("Integration", Integration.suite env_default),
+    ("Integration", Integration.suite),
-    ("Library", Library.suite env_default),
+    ("Library", Library.suite),
-    ("Metavar", Metavar.suite env_default),
+    ("Metavar", Metavar.suite),
-    ("Proofs", Proofs.suite env_default),
+    ("Proofs", Proofs.suite),
-    ("Delate", Delate.suite env_default),
+    ("Delate", Delate.suite),
-    ("Serial", Serial.suite env_default),
+    ("Serial", Serial.suite),
-    ("Tactic/Assign", Tactic.Assign.suite env_default),
+    ("Tactic/Assign", Tactic.Assign.suite),
-    ("Tactic/Prograde", Tactic.Prograde.suite env_default),
+    ("Tactic/Prograde", Tactic.Prograde.suite),
-    ("Tactic/Special", Tactic.Special.suite env_default),
+    ("Tactic/Special", Tactic.Special.suite),
   ]
-  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
+  let suiterunner (f : Lean.Environment → List (String × IO LSpec.TestSeq)) :=
+    f env_default
+  let tests : List (String × IO LSpec.TestSeq) := suites.foldl (init := []) λ acc (name, suite) =>
+    acc ++ (addPrefix name $ suiterunner suite)
   LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)

Test/Proofs.lean

@@ -11,7 +11,7 @@ open Pantograph
 open Lean
 
 inductive Start where
-  | copy (name: String) -- Start from some name in the environment
+  | copy (name: Name) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
 abbrev TestM := TestT $ ReaderT Protocol.Options $ Elab.TermElabM
@@ -20,7 +20,7 @@ def startProof (start: Start): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
   match start with
   | .copy name =>
-    let cInfo? := name.toName |> env.find?
+    let cInfo? := name |> env.find?
     addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
     match cInfo? with
     | .some cInfo =>
@@ -29,22 +29,8 @@ def startProof (start: Start): TestM (Option GoalState) := do
     | .none =>
       return Option.none
   | .expr expr =>
-    let syn? := parseTerm env expr
+    let expr ← parseSentence expr
-    addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
+    return .some $ ← GoalState.create (expr := expr)
-    match syn? with
-    | .error error =>
-      IO.println error
-      return Option.none
-    | .ok syn =>
-      let expr? ← elabType syn
-      addTest $ LSpec.check s!"Elaborating" expr?.isOk
-      match expr? with
-      | .error error =>
-        IO.println error
-        return Option.none
-      | .ok expr =>
-        let goal ← GoalState.create (expr := expr)
-        return Option.some goal
 
 def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
     (userName?: Option String := .none): Protocol.Goal :=
@@ -80,20 +66,14 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
     return a
 
 def test_identity: TestM Unit := do
-  let state? ← startProof (.expr "∀ (p: Prop), p → p")
+  let state0 ← GoalState.create (expr := ← parseSentence "∀ (p: Prop), p → p")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
   let tactic := "intro p h"
   let state1 ← match ← state0.tacticOn 0 tactic with
     | .success state _ => pure state
     | other => do
-      addTest $ assertUnreachable $ other.toString
+      fail other.toString
       return ()
-  let inner := "_uniq.12"
+  let inner := "_uniq.11"
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
     #[inner])
   let state1parent ← state1.withParentContext do
@@ -106,7 +86,7 @@ example: ∀ (a b: Nat), a + b = b + a := by
   rw [Nat.add_comm]
 def test_nat_add_comm (manual: Bool): TestM Unit := do
   let state? ← startProof <| match manual with
-    | false => .copy "Nat.add_comm"
+    | false => .copy `Nat.add_comm
     | true => .expr "∀ (a b: Nat), a + b = b + a"
   addTest $ LSpec.check "Start goal" state?.isSome
   let state0 ← match state? with

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.18.0
+leanprover/lean4:v4.19.0