19 changed files with 378 additions and 343 deletions
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -4,7 +4,6 @@ import Pantograph.Protocol
 import Pantograph.Serial
 import Lean.Environment
 import Lean.Replay
-import Lean.Util.Path

 open Lean
 open Pantograph
@ -131,19 +130,17 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
      } }
    | _ => pure core
  let result ← if args.source?.getD false then
-      try
-        let sourceUri? ← module?.bindM (Server.documentUriFromModule? ·)
+      let srcSearchPath ← initSrcSearchPath
+      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
      let declRange? ← findDeclarationRanges? name
      let sourceStart? := declRange?.map (·.range.pos)
      let sourceEnd? := declRange?.map (·.range.endPos)
      .pure {
        result with
-          sourceUri? := sourceUri?.map (toString ·),
+        sourceUri?,
        sourceStart?,
        sourceEnd?,
      }
-      catch _e =>
-        .pure result
    else
      .pure result
  return result
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -260,7 +260,6 @@ protected def GoalState.tryTacticM
    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
    (guardMVarErrors : Bool := false)
    : Elab.TermElabM TacticResult := do
-  assert! ¬ (← goal.isAssigned)
  let prevMessageLength := state.coreState.messages.toList.length
  try
    let nextState ← state.step goal tacticM guardMVarErrors
@ -290,6 +289,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
    (fileName := ← getFileName) with
    | .ok stx => pure $ stx
    | .error error => return .parseError error
+  assert! ¬ (← goal.isAssigned)
  state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true

 protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -69,10 +69,9 @@ def createCoreContext (options: Array String): IO Core.Context := do
@[export pantograph_create_core_state]
 def createCoreState (imports: Array String): IO Core.State := do
  let env ← Lean.importModules
-    (imports := imports.map (λ str => { module := str.toName }))
+    (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
    (opts := {})
    (trustLevel := 1)
-    (loadExts := true)
  return { env := env }

@[export pantograph_parse_elab_type_m]
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -361,8 +361,8 @@ structure FrontendProcess where
  readHeader : Bool := false
  -- Alter the REPL environment after the compilation units.
  inheritEnv : Bool := false
-  -- collect tactic invocations and output to a given file
-  invocations?: Option String := .none
+  -- collect tactic invocations
+  invocations: Bool := false
  -- collect `sorry`s
  sorrys: Bool := false
  -- collect type errors
@ -383,8 +383,8 @@ structure CompilationUnit where
  -- String boundaries of compilation units
  boundary: (Nat × Nat)
  messages: Array String := #[]
-  -- Number of tactic invocations
-  nInvocations?: Option Nat := .none
+  -- Tactic invocations
+  invocations?: Option (List InvokedTactic) := .none
  goalStateId?: Option Nat := .none
  goals?: Option (Array Goal) := .none
  -- Code segments which generated the goals
@ -396,12 +396,6 @@ structure CompilationUnit where
 structure FrontendProcessResult where
  units: List CompilationUnit
  deriving Lean.ToJson
-structure FrontendDataUnit where
-  invocations? : Option (List Protocol.InvokedTactic) := .none
-  deriving Lean.ToJson
-structure FrontendData where
-  units : List FrontendDataUnit
-  deriving Lean.ToJson

 abbrev FallibleT := ExceptT InteractionError

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

@[export pantograph_version]
-def version := "0.3.2"
+def version := "0.3.1"

 end Pantograph
--- a/Repl.lean
+++ b/Repl.lean
@ -5,16 +5,16 @@ namespace Pantograph.Repl

 open Lean

+set_option trace.Pantograph.Frontend.MetaTranslate true
+
 structure Context where
  coreContext : Core.Context
-  -- If true, the environment will change after running `CoreM`
-  inheritEnv : Bool := false

 /-- Stores state of the REPL -/
 structure State where
  options : Protocol.Options := {}
  nextId : Nat := 0
-  goalStates : Std.HashMap Nat GoalState := Std.HashMap.emptyWithCapacity
+  goalStates : Std.HashMap Nat GoalState := Std.HashMap.empty

  env : Environment
  -- Parser state
@ -30,9 +30,6 @@ instance : MonadEnv MainM where
  getEnv := return (← get).env
  modifyEnv f := modify fun s => { s with env := f s.env  }

-def withInheritEnv [Monad m] [MonadWithReaderOf Context m] [MonadLift MainM m] { α } (z : m α) : m α := do
-  withTheReader Context ({ · with inheritEnv := true }) z
-
 def newGoalState (goalState: GoalState) : MainM Nat := do
  let state ← get
  let stateId := state.nextId
@ -65,7 +62,7 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
      Except.ok <$> coreM
    catch ex =>
      let desc ← ex.toMessageData.toString
-      return Except.error ({ error := "exception", desc } : Protocol.InteractionError)
+      return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
    finally
      for {msg, ..} in (← getTraceState).traces do
        IO.eprintln (← msg.format.toIO)
@ -76,13 +73,14 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
    | Except.error (Exception.error _ msg)   => Protocol.throw $ { error := "core", desc := ← msg.toString }
    | Except.error (Exception.internal id _) => Protocol.throw $ { error := "internal", desc := (← id.getName).toString }
    | Except.ok a                            => pure a
-  if (← read).inheritEnv && result matches .ok _ then
-    setEnv state'.env
+  if result matches .ok _ then
+    modifyEnv λ _ => state'.env
  liftExcept result

 def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
  liftExcept $ ← runCoreM coreM.run

+
 def liftMetaM { α } (metaM : MetaM α): EMainM α :=
  runCoreM metaM.run'
 def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name := [])
@ -100,7 +98,7 @@ def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name
 section Frontend

 structure CompilationUnit where
-  -- Environment immediately before the unit
+  -- Should be the penultimate environment, but this is ok
  env : Environment
  boundary : Nat × Nat
  invocations : List Protocol.InvokedTactic
@ -108,7 +106,7 @@ structure CompilationUnit where
  messages : Array String
  newConstants : List Name

-def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
  let options := (← getMainState).options
  let (fileName, file) ← match args.fileName?, args.file? with
    | .some fileName, .none => do
@ -125,7 +123,7 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP
  let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
    Frontend.mapCompilationSteps λ step => do
    let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-    let invocations: Option (List Protocol.InvokedTactic) ← if args.invocations?.isSome then
+    let invocations: Option (List Protocol.InvokedTactic) ← if args.invocations then
        Frontend.collectTacticsFromCompilationStep step
      else
        pure []
@ -152,10 +150,6 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP
    if let .some scope := state'.commandState.scopes.head? then
      -- modify the scope
      set { ← getMainState with scope }
-  if let .some fileName := args.invocations? then
-    let units := li.map λ unit => { invocations? := .some unit.invocations }
-    let data : Protocol.FrontendData := { units }
-    IO.FS.writeFile fileName (toJson data |>.compress)
  let units ← li.mapM λ step => withEnv step.env do
    let newConstants? := if args.newConstants then
        .some $ step.newConstants.toArray.map λ name => name.toString
@ -171,11 +165,11 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP
        let stateId ← newGoalState state
        let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
        pure (.some stateId, .some goals, .some srcBoundaries)
-    let nInvocations? := if args.invocations?.isSome then .some step.invocations.length else .none
+    let invocations? := if args.invocations then .some step.invocations else .none
    return {
      boundary := step.boundary,
      messages := step.messages,
-      nInvocations?,
+      invocations?,
      goalStateId?,
      goals?,
      goalSrcBoundaries?,
@ -231,7 +225,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 := .emptyWithCapacity }
+    set { state with nextId := 0, goalStates := .empty }
    return { nGoals }
  stat (_: Protocol.Stat): EMainM Protocol.StatResult := do
    let state ← getMainState
@ -248,7 +242,7 @@ def execute (command: Protocol.Command): MainM Json := do
  env_inspect (args: Protocol.EnvInspect): EMainM Protocol.EnvInspectResult := do
    let state ← getMainState
    runCoreM' $ Environment.inspect args state.options
-  env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := withInheritEnv do
+  env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := do
    runCoreM' $ Environment.addDecl args.name (args.levels?.getD #[]) args.type? args.value args.isTheorem
  env_save (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
    let env ← MonadEnv.getEnv
@ -408,5 +402,7 @@ def execute (command: Protocol.Command): MainM Json := do
    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
    let id ← newGoalState goalState
    return { id }
+  frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+    frontend_process_inner args

 end Pantograph.Repl
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -69,8 +69,6 @@ end Condensed

 def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
 def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
-def GoalState.tacticOn' (state: GoalState) (goalId: Nat) (tactic: TSyntax `tactic) :=
-  state.tryTacticM (state.get! goalId) (Elab.Tactic.evalTactic tactic) true

 def TacticResult.toString : TacticResult → String
  | .success state _messages => s!".success ({state.goals.length} goals)"
--- a/Test/Delate.lean
+++ b/Test/Delate.lean
@ -51,7 +51,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
    ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
-    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.20) (:mv _uniq.21) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"),
+    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
  ]
  entries.foldlM (λ suites (source, levels, target) =>
    let termElabM := do
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -15,7 +15,11 @@ deriving instance DecidableEq, Repr for Protocol.RecursorRule
 deriving instance DecidableEq, Repr for Protocol.RecursorInfo
 deriving instance DecidableEq, Repr for Protocol.EnvInspectResult

-def test_catalog (env : Environment) : IO LSpec.TestSeq := do
+def test_catalog: 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 =>
@ -42,7 +46,11 @@ inductive ConstantCat where
  | ctor (info: Protocol.ConstructorInfo)
  | recursor (info: Protocol.RecursorInfo)

-def test_inspect (env : Environment) : IO LSpec.TestSeq := do
+def test_inspect: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
  let testCases: List (String × ConstantCat) := [
    ("Or", ConstantCat.induct {
      numParams := 2,
@ -89,29 +97,37 @@ def test_inspect (env : Environment) : IO LSpec.TestSeq := do
    ) LSpec.TestSeq.done
  runCoreMSeq env inner

-def test_symbol_location (env : Environment) : TestT IO Unit := do
+def test_symbol_location : 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"

    -- Extraction of source doesn't work for symbols in `Init` for some reason
    checkTrue "file" result.sourceUri?.isNone
-    checkEq "sourceStart" (result.sourceStart?.map (·.column)) <| .some 0
-    checkEq "sourceEnd" (result.sourceEnd?.map (·.column)) <| .some 88
+    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
+    checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
    let { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩
-    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero", "Init.Grind.Tactics"]
+    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
    checkTrue "constNames" $ constNames.contains "Nat.succ_add"

-def test_matcher (env : Environment) : TestT IO Unit := do
+def test_matcher : TestT IO Unit := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
  checkTrue "not matcher" $ ¬ Meta.isMatcherCore env `Nat.strongRecOn

-def suite (env : Environment) : List (String × IO LSpec.TestSeq) :=
+def suite: List (String × IO LSpec.TestSeq) :=
  [
-    ("Catalog", test_catalog env),
+    ("Catalog", test_catalog),
    ("Symbol Visibility", test_symbol_visibility),
-    ("Inspect", test_inspect env),
-    ("Symbol Location", runTest $ test_symbol_location env),
-    ("Matcher", runTest $ test_matcher env),
+    ("Inspect", test_inspect),
+    ("Symbol Location", runTest test_symbol_location),
+    ("Matcher", runTest test_matcher),
  ]

 end Pantograph.Test.Environment
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -17,59 +17,53 @@ deriving instance Lean.ToJson for Protocol.GoalStart
 deriving instance Lean.ToJson for Protocol.GoalPrint
 deriving instance Lean.ToJson for Protocol.GoalTactic
 deriving instance Lean.ToJson for Protocol.FrontendProcess
-deriving instance Lean.ToJson for Protocol.FrontendDataUnit
-deriving instance Lean.ToJson for Protocol.FrontendData
-
-abbrev TestM α := TestT MainM α
-abbrev Test := TestM Unit

 def step { α β } [Lean.ToJson α] [Lean.ToJson β] (cmd: String) (payload: α)
-    (expected: β) (name? : Option String := .none) : TestM Unit := do
+    (expected: β) (name? : Option String := .none): MainM LSpec.TestSeq := do
  let payload := Lean.toJson payload
  let name := name?.getD s!"{cmd} {payload.compress}"
  let result ← Repl.execute { cmd, payload }
-  checkEq name result.compress (Lean.toJson expected).compress
-def stepFile { α } [Lean.ToJson α] (name : String) (path : String)
-    (expected : α) : TestM Unit := do
-  let content ← IO.FS.readFile path
-  let payload? : Except String Lean.Json := Lean.Json.parse content
-  match payload? with
-  | .ok payload =>
-    let expected := Lean.toJson expected
-    checkEq name payload.compress expected.compress
-  | .error e => fail s!"{name} {e}"
+  return LSpec.test name (result.pretty = (Lean.toJson expected).pretty)
+
+abbrev Test := List (MainM LSpec.TestSeq)

 def test_expr_echo : Test :=
+  [
    step "expr.echo"
     ({ expr := "λ {α : Sort (u + 1)} => List α", levels? := .some #["u"]}: Protocol.ExprEcho)
     ({
       type := { pp? := .some "{α : Type u} → Type u" },
       expr := { pp? := .some "fun {α} => List α" }
-   }: Protocol.ExprEchoResult)
+     }: Protocol.ExprEchoResult),
+  ]

-def test_option_modify : Test := do
+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 := {}
+  [
    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
-   ({ type := { pp? }, module? }: Protocol.EnvInspectResult)
+     ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
    step "options.set" ({ printExprAST? := .some true } : Protocol.OptionsSet)
-   ({ }: Protocol.OptionsSetResult)
+     ({ }: Protocol.OptionsSetResult),
    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
-   ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult)
+     ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
    step "options.print" ({} : Protocol.OptionsPrint)
-   ({ options with printExprAST := true }: Protocol.Options)
-
-def test_malformed_command : Test := do
+     ({ options with printExprAST := true }: Protocol.Options),
+  ]
+def test_malformed_command : Test :=
  let invalid := "invalid"
+  [
    step invalid ({ name := "Nat.add_one" }: Protocol.EnvInspect)
     ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
-   (name? := .some "Invalid Command")
+     (name? := .some "Invalid Command"),
    step "expr.echo" (Lean.Json.mkObj [(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 : Test := do
+      Protocol.InteractionError)
+    (name? := .some "JSON Deserialization")
+  ]
+def test_tactic : Test :=
  let varX := { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}
  let goal1: Protocol.Goal := {
    name := "_uniq.11",
@ -84,39 +78,43 @@ def test_tactic : Test := do
      { name := "_uniq.13", userName := "y", type? := .some { pp? := .some "Prop" }}
    ],
  }
+  [
    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p" }: Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult)
+     ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
    step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
     ({
       root? := .some { pp? := "fun x => ?m.11"},
       parent? := .some { pp? := .some "fun x => ?m.11" },
-   }: Protocol.GoalPrintResult)
+     }: Protocol.GoalPrintResult),
    step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
     ({ messages? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
-    Protocol.GoalTacticResult)
+      Protocol.GoalTacticResult),
    step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult),
+  ]
 example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
  simp
-def test_tactic_timeout : Test := do
+def test_tactic_timeout : Test :=
+  [
    step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.355" }: Protocol.GoalStartResult)
+     ({ stateId := 0, root := "_uniq.319" }: Protocol.GoalStartResult),
    -- timeout of 10 milliseconds
    step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet)
-   ({ }: Protocol.OptionsSetResult)
+     ({ }: Protocol.OptionsSetResult),
    step "goal.tactic" ({ stateId := 0, expr? := .some "by\nsleep 1000; simp" }: Protocol.GoalTactic)
-   ({ error := "internal", desc := "interrupt" }: Protocol.InteractionError)
+     ({ error := "internal", desc := "interrupt" }: Protocol.InteractionError),
    -- ensure graceful recovery
    step "options.set" ({ timeout? := .some 0 } : Protocol.OptionsSet)
-   ({ }: Protocol.OptionsSetResult)
+     ({ }: Protocol.OptionsSetResult),
    step "goal.tactic" ({ stateId := 0, tactic? := .some "simp" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 1, goals? := .some #[], }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 1, goals? := .some #[], }: Protocol.GoalTacticResult),
+  ]

-def test_automatic_mode (automatic: Bool): Test := do
+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" }}
@ -152,34 +150,38 @@ def test_automatic_mode (automatic: Bool): Test := do
      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
    ],
  }
+  [
    step "options.set" ({automaticMode? := .some automatic}: Protocol.OptionsSet)
-   ({}: Protocol.OptionsSetResult)
+     ({}: Protocol.OptionsSetResult),
    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p"} : Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult)
+     ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro p q h" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
    step "goal.tactic" ({ stateId := 1, tactic? := .some "cases h" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
    let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
    step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
+  ]

-def test_env_add_inspect : Test := do
+def test_env_add_inspect : Test :=
  let name1 := "Pantograph.mystery"
  let name2 := "Pantograph.mystery2"
  let name3 := "Pantograph.mystery3"
+  [
    step "env.add"
      ({
        name := name1,
        value := "λ (a b: Prop) => Or a b",
        isTheorem := false
      }: Protocol.EnvAdd)
-   ({}: Protocol.EnvAddResult)
+     ({}: Protocol.EnvAddResult),
    step "env.inspect" ({name := name1, value? := .some true} : Protocol.EnvInspect)
     ({
       value? := .some { pp? := .some "fun a b => a ∨ b" },
       type := { pp? := .some "Prop → Prop → Prop" },
-   }: Protocol.EnvInspectResult)
+     }:
+      Protocol.EnvInspectResult),
    step "env.add"
      ({
        name := name2,
@ -187,12 +189,13 @@ def test_env_add_inspect : Test := do
        value := "λ (a: Nat) => a + 1",
        isTheorem := false
      }: Protocol.EnvAdd)
-   ({}: Protocol.EnvAddResult)
+     ({}: Protocol.EnvAddResult),
    step "env.inspect" ({name := name2, value? := .some true} : Protocol.EnvInspect)
     ({
       value? := .some { pp? := .some "fun a => ↑a + 1" },
       type := { pp? := .some "Nat → Int" },
-   }: Protocol.EnvInspectResult)
+     }:
+      Protocol.EnvInspectResult),
    step "env.add"
      ({
        name := name3,
@ -201,34 +204,30 @@ def test_env_add_inspect : Test := do
        value := "λ (α : Type u) (x : α) => (x, x)",
        isTheorem := false
      }: Protocol.EnvAdd)
-   ({}: Protocol.EnvAddResult)
+     ({}: Protocol.EnvAddResult),
    step "env.inspect" ({name := name3} : Protocol.EnvInspect)
     ({
       type := { pp? := .some "(α : Type u) → α → α × α" },
-   }: Protocol.EnvInspectResult)
+     }:
+      Protocol.EnvInspectResult),
+  ]

 example : ∀ (p: Prop), p → p := by
  intro p h
  exact h

-def test_frontend_process : Test := do
+def test_frontend_process : Test :=
  let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
  let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
-  IO.FS.withTempDir λ tempdir => do
-  let filename := s!"{tempdir}/invocations.jsonl"
+  [
    step "frontend.process"
      ({
        file? := .some file,
-      invocations? := .some filename,
+        invocations := true,
      }: Protocol.FrontendProcess)
     ({
       units := [{
         boundary := (0, file.utf8ByteSize),
-       nInvocations? := .some 2,
-     }],
-   }: Protocol.FrontendProcessResult)
-  stepFile (α := Protocol.FrontendData) "invocations" filename
-    { units := [{
         invocations? := .some [
           {
             goalBefore := "⊢ ∀ (p q : Prop), p → p ∨ q",
@ -243,14 +242,17 @@ def test_frontend_process : Test := do
             usedConstants := #["Or.inl"],
           },
         ]
-    } ] }
+       }],
+    }: Protocol.FrontendProcessResult),
+  ]

 example : 1 + 2 = 3 := rfl
 example (p: Prop): p → p := by simp

-def test_frontend_process_sorry : Test := do
+def test_frontend_process_sorry : Test :=
  let solved := "example : 1 + 2 = 3 := rfl\n"
  let withSorry := "example (p: Prop): p → p := sorry"
+  [
    let file := s!"{solved}{withSorry}"
    let goal1: Protocol.Goal := {
      name := "_uniq.6",
@ -272,15 +274,17 @@ def test_frontend_process_sorry : Test := do
         goalSrcBoundaries? := .some #[(57, 62)],
         messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
       }],
-   }: Protocol.FrontendProcessResult)
+     }: Protocol.FrontendProcessResult),
+  ]

-def test_import_open : Test := do
+def test_import_open : Test :=
  let header := "import Init\nopen Nat\nuniverse u"
  let goal1: Protocol.Goal := {
-    name := "_uniq.77",
+    name := "_uniq.67",
    target := { pp? := .some "n + 1 = n.succ" },
-    vars := #[{ name := "_uniq.76", userName := "n", type? := .some { pp? := .some "Nat" }}],
+    vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}],
  }
+  [
    step "frontend.process"
      ({
        file? := .some header,
@ -292,19 +296,21 @@ def test_import_open : Test := do
         { boundary := (12, 21) },
         { boundary := (21, header.utf8ByteSize) },
       ],
-   }: Protocol.FrontendProcessResult)
+     }: Protocol.FrontendProcessResult),
    step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.75" }: Protocol.GoalStartResult)
+     ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult),
    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
-   ({ nextStateId? := .some 2, goals? := .some #[], }: Protocol.GoalTacticResult)
+     ({ nextStateId? := .some 2, goals? := .some #[], }: Protocol.GoalTacticResult),
    step "goal.start" ({ expr := "∀ (x : Sort u), Sort (u + 1)"} : Protocol.GoalStart)
-   ({ stateId := 3, root := "_uniq.5" }: Protocol.GoalStartResult)
+     ({ stateId := 3, root := "_uniq.5" }: Protocol.GoalStartResult),
+  ]

 /-- Ensure there cannot be circular references -/
-def test_frontend_process_circular : Test := do
+def test_frontend_process_circular : Test :=
  let withSorry := "theorem mystery : 1 + 2 = 2 + 3 := sorry"
+  [
    let goal1: Protocol.Goal := {
      name := "_uniq.2",
      target := { pp? := .some "1 + 2 = 2 + 3" },
@ -323,15 +329,17 @@ def test_frontend_process_circular : Test := do
         goalSrcBoundaries? := .some #[(35, 40)],
         messages := #["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],
       }],
-   }: Protocol.FrontendProcessResult)
+     }: Protocol.FrontendProcessResult),
    step "goal.tactic" ({ stateId := 0, tactic? := .some "exact?" }: Protocol.GoalTactic)
     ({ messages? := .some #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."] }
-   : Protocol.GoalTacticResult)
+     : Protocol.GoalTacticResult),
+  ]

-def runTestSuite (env : Lean.Environment) (steps : Test): IO LSpec.TestSeq := do
+def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
  -- Setup the environment for execution
  let coreContext ← createCoreContext #[]
-  let mainM : MainM LSpec.TestSeq := runTest steps
+  let mainM : MainM LSpec.TestSeq :=
+    steps.foldlM (λ suite step => do return suite ++ (← step)) LSpec.TestSeq.done
  mainM.run { coreContext } |>.run' { env }

 def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
@ -349,7 +357,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
    ("frontend.process import", test_import_open),
    ("frontend.process circular", test_frontend_process_circular),
  ]
-  tests.map (fun (name, test) => (name, runTestSuite env test))
+  tests.map (fun (name, test) => (name, runTest env test))


 end Pantograph.Test.Integration
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -43,23 +43,19 @@ def main (args: List String) := do
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
-    (loadExts := true)

-  let suites: List (String × (Lean.Environment → List (String × IO LSpec.TestSeq))) := [
+  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
    ("Environment", Environment.suite),
-    ("Frontend", Frontend.suite),
-    ("Integration", Integration.suite),
-    ("Library", Library.suite),
-    ("Metavar", Metavar.suite),
-    ("Proofs", Proofs.suite),
-    ("Delate", Delate.suite),
-    ("Serial", Serial.suite),
-    ("Tactic/Assign", Tactic.Assign.suite),
-    ("Tactic/Prograde", Tactic.Prograde.suite),
-    ("Tactic/Special", Tactic.Special.suite),
+    ("Frontend", Frontend.suite env_default),
+    ("Integration", Integration.suite env_default),
+    ("Library", Library.suite env_default),
+    ("Metavar", Metavar.suite env_default),
+    ("Proofs", Proofs.suite env_default),
+    ("Delate", Delate.suite env_default),
+    ("Serial", Serial.suite env_default),
+    ("Tactic/Assign", Tactic.Assign.suite env_default),
+    ("Tactic/Prograde", Tactic.Prograde.suite env_default),
+    ("Tactic/Special", Tactic.Special.suite env_default),
  ]
-  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)
+  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
  LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -25,8 +25,8 @@ def test_instantiate_mvar: TestM Unit := do
      addTest $ assertUnreachable e
      return ()
  let t ← Lean.Meta.inferType expr
-  checkEq "typing" (toString (← serializeExpressionSexp t))
-    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"
+  addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) =
+    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
  return ()

 def startProof (expr: String): TestM (Option GoalState) := do
@ -118,9 +118,8 @@ def test_m_couple_simp: TestM Unit := do
  let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
  addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
-  let n := state1.goals[2]!
  addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
-    #[#[toString n.name], #[toString n.name], #[]])
+    #[#["_uniq.38"], #["_uniq.38"], #[]])

  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
    | .success state _ => pure state
@ -159,10 +158,10 @@ def test_m_couple_simp: TestM Unit := do
      addTest $ assertUnreachable "(5 root)"
      return ()
  let rootStr: String := toString (← Lean.Meta.ppExpr root)
-  checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
+  addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
  let unfoldedRoot ←  unfoldAuxLemmas root
-  checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot))
-    "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
+  addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
+    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
  return ()

 def test_proposition_generation: TestM Unit := do
@ -259,7 +258,7 @@ def test_partial_continuation: TestM Unit := do

  -- Continuation should fail if the state does not exist:
  match state0.resume coupled_goals with
-  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.44, _uniq.45, _uniq.42, _uniq.51] are not in scope")
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
  -- Continuation should fail if some goals have not been solved
  match state2.continue state1 with
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -11,7 +11,7 @@ open Pantograph
 open Lean

 inductive Start where
-  | copy (name: Name) -- Start from some name in the environment
+  | copy (name: String) -- 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 |> env.find?
+    let cInfo? := name.toName |> env.find?
    addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
    match cInfo? with
    | .some cInfo =>
@ -29,8 +29,22 @@ def startProof (start: Start): TestM (Option GoalState) := do
    | .none =>
      return Option.none
  | .expr expr =>
-    let expr ← parseSentence expr
-    return .some $ ← GoalState.create (expr := expr)
+    let syn? := parseTerm 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
+      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 :=
@ -66,15 +80,21 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
    return a

 def test_identity: TestM Unit := do
-  let rootTarget ← Elab.Term.elabTerm (← `(term|∀ (p: Prop), p → p)) .none
-  let state0 ← GoalState.create (expr := rootTarget)
-  let state1 ← match ← state0.tacticOn' 0 (← `(tactic|intro p h)) with
+  let state? ← startProof (.expr "∀ (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
-      fail other.toString
+      addTest $ assertUnreachable $ other.toString
      return ()
-  let inner := "_uniq.11"
-  addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
+  let inner := "_uniq.12"
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
    #[inner])
  let state1parent ← state1.withParentContext do
    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
@ -86,7 +106,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
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -7,6 +7,9 @@ open Lean

 namespace Pantograph.Test.Serial

+def tempPath : IO System.FilePath := do
+  Prod.snd <$> IO.FS.createTempFile
+
 structure MultiState where
  coreContext : Core.Context
  env: Environment
@ -32,7 +35,7 @@ def test_environment_pickling : TestM Unit := do
  let coreDst : Core.State := { env := ← getEnv }

  let name := `mystery
-  IO.FS.withTempFile λ _ envPicklePath => do
+  let envPicklePath ← tempPath
  let ((), _) ← runCoreM coreSrc do
    let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
    let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default
@ -53,10 +56,13 @@ def test_environment_pickling : TestM Unit := do
    let anotherName := `mystery2
    checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone

+  IO.FS.removeFile envPicklePath
+
 def test_goal_state_pickling_simple : TestM Unit := do
  let coreSrc : Core.State := { env := ← getEnv }
  let coreDst : Core.State := { env := ← getEnv }
-  IO.FS.withTempFile λ _ statePath => do
+  let statePath ← tempPath
+
  let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
  let stateGenerate : MetaM GoalState := runTermElabMInMeta do
    GoalState.create type
@ -72,6 +78,8 @@ def test_goal_state_pickling_simple : TestM Unit := do
    let types ← metaM.run'
    checkTrue "Goals" $ types[0]!.equal type

+  IO.FS.removeFile statePath
+
 structure Test where
  name : String
  routine: TestM Unit
--- a/Test/Tactic/Prograde.lean
+++ b/Test/Tactic/Prograde.lean
@ -131,6 +131,10 @@ def test_define_root_expr : TestT Elab.TermElabM Unit := do
  let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
  addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")

+--set_option pp.all true
+--#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
+--def test_define_root_expr : TestT Elab.TermElabM Unit := do
+
 def test_have_proof : TestT Elab.TermElabM Unit := do
  let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
  let state0 ← GoalState.create rootExpr
--- a/doc/repl.md
+++ b/doc/repl.md
@ -52,9 +52,9 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
  state. The user is responsible to ensure the sender/receiver instances share
  the same environment.
 * `frontend.process { ["fileName": <fileName>,] ["file": <str>], readHeader: <bool>, inheritEnv: <bool>, invocations:
-  <string>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
+  <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
  Executes the Lean frontend on a file, collecting the tactic invocations
-  (`"invocations": output-path`), the sorrys and type errors into goal states
+  (`"invocations": true`), the sorrys and type errors into goal states
  (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
  `sorrys`, this command additionally outputs the position of each captured
  `sorry`. Conditionally inherit the environment from executing the file.
--- a/flake.lock
+++ b/flake.lock
@ -5,11 +5,11 @@
        "nixpkgs-lib": "nixpkgs-lib"
      },
      "locked": {
-        "lastModified": 1749398372,
-        "narHash": "sha256-tYBdgS56eXYaWVW3fsnPQ/nFlgWi/Z2Ymhyu21zVM98=",
+        "lastModified": 1743550720,
+        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
        "owner": "hercules-ci",
        "repo": "flake-parts",
-        "rev": "9305fe4e5c2a6fcf5ba6a3ff155720fbe4076569",
+        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
        "type": "github"
      },
      "original": {
@ -44,11 +44,11 @@
        ]
      },
      "locked": {
-        "lastModified": 1750275702,
-        "narHash": "sha256-CpwSdtwvrQCR+ZfXZweFHJMG583EYijCRGEeGrgBsjU=",
+        "lastModified": 1743534244,
+        "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=",
        "owner": "lenianiva",
        "repo": "lean4-nix",
-        "rev": "95a315f6e7d5e463090ae4977d5e2e6c3b4ef0d0",
+        "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d",
        "type": "github"
      },
      "original": {
@ -59,11 +59,11 @@
    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1750151854,
-        "narHash": "sha256-3za+1J9FifMetO7E/kwgyW+dp+8pPBNlWKfcBovnn6M=",
+        "lastModified": 1743975612,
+        "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=",
        "owner": "nixos",
        "repo": "nixpkgs",
-        "rev": "ad5c70bcc5cc5178205161b7a7d61a6e80f6d244",
+        "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928",
        "type": "github"
      },
      "original": {
@ -75,11 +75,11 @@
    },
    "nixpkgs-lib": {
      "locked": {
-        "lastModified": 1748740939,
-        "narHash": "sha256-rQaysilft1aVMwF14xIdGS3sj1yHlI6oKQNBRTF40cc=",
+        "lastModified": 1743296961,
+        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
        "owner": "nix-community",
        "repo": "nixpkgs.lib",
-        "rev": "656a64127e9d791a334452c6b6606d17539476e2",
+        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
        "type": "github"
      },
      "original": {
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.20.1
+leanprover/lean4:v4.18.0