Merge branch 'dev' into goal/relation

2024-03-29 23:47:09 -07:00 · 2024-03-29 23:47:09 -07:00 · 113e65e193
parent 8853b17fee aeed233846
commit 113e65e193
21 changed files with 522 additions and 246 deletions
--- a/Main.lean
+++ b/Main.lean
@ -2,6 +2,7 @@ import Lean.Data.Json
 import Lean.Environment

 import Pantograph.Version
+import Pantograph.Library
 import Pantograph

 -- Main IO functions
@ -39,35 +40,6 @@ partial def loop : MainM Unit := do
    IO.println str
  loop

-namespace Lean
-
-/-- This is better than the default version since it handles `.` and doesn't
- crash the program when it fails. -/
-def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
-  let ps := (entry.splitOn "=").map String.trim
-  let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
-  let key := key.toName
-  let defValue ← getOptionDefaultValue key
-  match defValue with
-  | DataValue.ofString _ => pure $ opts.setString key val
-  | DataValue.ofBool _   =>
-    match val with
-    | "true" => pure $ opts.setBool key true
-    | "false" => pure $ opts.setBool key false
-    | _ => throw  s!"invalid Bool option value '{val}'"
-  | DataValue.ofName _   => pure $ opts.setName key val.toName
-  | DataValue.ofNat _    =>
-    match val.toNat? with
-    | none   => throw s!"invalid Nat option value '{val}'"
-    | some v => pure $ opts.setNat key v
-  | DataValue.ofInt _    =>
-    match val.toInt? with
-    | none   => throw s!"invalid Int option value '{val}'"
-    | some v => pure $ opts.setInt key v
-  | DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
-
-end Lean
-

 unsafe def main (args: List String): IO Unit := do
  -- NOTE: A more sophisticated scheme of command line argument handling is needed.
@ -76,35 +48,19 @@ unsafe def main (args: List String): IO Unit := do
    println! s!"{version}"
    return

-  Lean.enableInitializersExecution
-  Lean.initSearchPath (← Lean.findSysroot)
+  initSearch ""

-  let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
-    |>.foldlM Lean.setOptionFromString' Lean.Options.empty
-    |>.run
-  let options ← match options? with
-    | .ok options => pure options
-    | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
+  let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+    |>.toArray |> createCoreContext
  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
-
-  let env ← Lean.importModules
-    (imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false }))
-    (opts := {})
-    (trustLevel := 1)
+  let coreState ← createCoreState imports.toArray
  let context: Context := {
    imports
  }
-  let coreContext: Lean.Core.Context := {
-    currNamespace := Lean.Name.str .anonymous "Aniva"
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph>",
-    fileMap := { source := "", positions := #[0], lines := #[1] },
-    options := options
-  }
  try
    let coreM := loop.run context |>.run' {}
    IO.println "ready."
-    discard <| coreM.toIO coreContext { env := env }
+    discard <| coreM.toIO coreContext coreState
  catch ex =>
    IO.println "Uncaught IO exception"
    IO.println ex.toString
--- a/8
+++ b/8
@ -1,8 +1,8 @@
-LIB := build/lib/Pantograph.olean
-EXE := build/bin/pantograph
+LIB := ./.lake/build/lib/Pantograph.olean
+EXE := ./.lake/build/bin/pantograph
 SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain

-TEST_EXE := build/bin/test
+TEST_EXE := ./.lake/build/bin/test
 TEST_SOURCE := $(wildcard Test/*.lean)

 $(LIB) $(EXE): $(SOURCE)
@ -12,7 +12,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 	lake build test

 test: $(TEST_EXE)
-	lake env $(TEST_EXE)
+	$(TEST_EXE)

 clean:
 	lake clean
--- a/Pantograph.lean
+++ b/Pantograph.lean
@ -2,6 +2,7 @@ import Pantograph.Goal
 import Pantograph.Protocol
 import Pantograph.Serial
 import Pantograph.Environment
+import Pantograph.Library
 import Lean.Data.HashMap

 namespace Pantograph
@ -21,14 +22,6 @@ abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
 -- certain monadic features in `MainM`
 abbrev CR α := Except Protocol.InteractionError α

-def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
-  metaM.run'
-def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
-  termElabM.run' (ctx := {
-    declName? := .none,
-    errToSorry := false,
-  }) |>.run'
-
 def execute (command: Protocol.Command): MainM Lean.Json := do
  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
    match Lean.fromJson? command.payload with
@ -56,7 +49,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
      errorCommand s!"Unknown command {cmd}"
    return Lean.toJson error
  where
-  errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
  errorCommand := errorI "command"
  errorIndex := errorI "index"
  -- Command Functions
@ -70,7 +62,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    let nGoals := state.goalStates.size
    return .ok { nGoals }
  env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
-    Environment.catalog args
+    let result ← Environment.catalog args
+    return .ok result
  env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
    let state ← get
    Environment.inspect args state.options
@ -78,22 +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
-    let env ← Lean.MonadEnv.getEnv
-    let syn ← match syntax_from_str env args.expr with
-      | .error str => return .error $ errorI "parsing" str
-      | .ok syn => pure syn
-    runTermElabM (do
-      match ← syntax_to_expr syn with
-      | .error str => return .error $ errorI "elab" str
-      | .ok expr => do
-        try
-          let type ← Lean.Meta.inferType expr
-          return .ok {
-              type := (← serialize_expression (options := state.options) type),
-              expr := (← serialize_expression (options := state.options) expr)
-          }
-        catch exception =>
-          return .error $ errorI "typing" (← exception.toMessageData.toString))
+    exprEcho args.expr state.options
  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
    let state ← get
    let options := state.options
@ -115,13 +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 =>
-        (match syntax_from_str env expr with
-        | .error str => return .error <| errorI "parsing" str
-        | .ok syn => do
-          (match ← syntax_to_expr syn with
-          | .error str => return .error <| errorI "elab" str
-          | .ok expr => return .ok (← GoalState.create 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}"
@ -144,9 +120,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    | .some goalState => do
      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
        | .some tactic, .none => do
-          pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic))
+          pure ( Except.ok (← goalTactic goalState args.goalId tactic))
        | .none, .some expr => do
-          pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr))
+          pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
      match nextGoalState? with
      | .error error => return .error error
@ -178,8 +154,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
          | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
          | .some branch => pure $ target.continue branch
        | .none, .some goals =>
-          let goals := goals.map (λ name => { name := name.toName })
-          pure $ target.resume goals
+          pure $ goalResume target goals
        | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
      match nextState? with
      | .error error => return .error <| errorI "structure" error
@ -189,7 +164,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
          goalStates := state.goalStates.insert nextStateId nextGoalState,
          nextId := state.nextId + 1
        }
-        let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run'
+        let goals ← goalSerialize nextGoalState (options := state.options)
        return .ok {
          nextStateId,
          goals,
@ -204,12 +179,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    match state.goalStates.find? args.stateId with
    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
    | .some goalState => runMetaM <| do
-      goalState.restoreMetaM
-      let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
-      let parent? ← goalState.parentExpr?.mapM (λ expr => serialize_expression state.options expr)
-      return .ok {
-        root?,
-        parent?,
-      }
+      return .ok (← goalPrint goalState state.options)

 end Pantograph
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -7,14 +7,15 @@ open Pantograph

 namespace Pantograph.Environment

-def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
-  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe
+def isNameInternal (n: Lean.Name): Bool :=
+  -- Returns true if the name is an implementation detail which should not be shown to the user.
+  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
  where
  isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
    | .str _ name => name == "Lean"
    | _ => true

-def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
  let pref := match info with
  | .axiomInfo  _ => "a"
  | .defnInfo   _ => "d"
@ -26,18 +27,18 @@ def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
  | .recInfo    _ => "r"
  s!"{pref}{toString n}"

-def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
-  if is_symbol_unsafe_or_internal n info
+def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
+  if isNameInternal n || info.isUnsafe
  then Option.none
-  else Option.some <| to_compact_symbol_name n info
-def catalog (_: Protocol.EnvCatalog): CoreM (Protocol.CR Protocol.EnvCatalogResult) := do
+  else Option.some <| toCompactSymbolName n info
+def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
  let env ← Lean.MonadEnv.getEnv
  let names := env.constants.fold (init := #[]) (λ acc name info =>
-    match to_filtered_symbol name info with
+    match toFilteredSymbol name info with
    | .some x => acc.push x
    | .none => acc)
-  return .ok { symbols := names }
-def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
+  return { symbols := names }
+def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
  let env ← Lean.MonadEnv.getEnv
  let name :=  args.name.toName
  let info? := env.find? name
@ -58,16 +59,22 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Prot
    value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
    publicName? := Lean.privateToUserName? name |>.map (·.toString),
    -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
-    typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
-    valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
+    typeDependency? := if args.dependency?.getD false
+      then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n)
+      else .none,
+    valueDependency? := ← if args.dependency?.getD false
+      then info.value?.mapM (λ e => do
+        let e ← (unfoldAuxLemmas e).run'
+        pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
+      else pure (.none),
    module? := module?
  }
  let result := match info with
    | .inductInfo induct => { core with inductInfo? := .some {
          numParams := induct.numParams,
          numIndices := induct.numIndices,
-          all := induct.all.map (·.toString),
-          ctors := induct.ctors.map (·.toString),
+          all := induct.all.toArray.map (·.toString),
+          ctors := induct.ctors.toArray.map (·.toString),
          isRec := induct.isRec,
          isReflexive := induct.isReflexive,
          isNested := induct.isNested,
@ -79,7 +86,7 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Prot
          numFields := ctor.numFields,
      } }
    | .recInfo r => { core with recursorInfo? := .some {
-          all := r.all.map (·.toString),
+          all := r.all.toArray.map (·.toString),
          numParams := r.numParams,
          numIndices := r.numIndices,
          numMotives := r.numMotives,
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -0,0 +1,181 @@
+import Pantograph.Environment
+import Pantograph.Goal
+import Pantograph.Protocol
+import Pantograph.Serial
+import Pantograph.Version
+import Lean
+
+namespace Lean
+
+/-- This is better than the default version since it handles `.` and doesn't
+ crash the program when it fails. -/
+def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
+  let ps := (entry.splitOn "=").map String.trim
+  let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
+  let key := key.toName
+  let defValue ← getOptionDefaultValue key
+  match defValue with
+  | DataValue.ofString _ => pure $ opts.setString key val
+  | DataValue.ofBool _   =>
+    match val with
+    | "true" => pure $ opts.setBool key true
+    | "false" => pure $ opts.setBool key false
+    | _ => throw  s!"invalid Bool option value '{val}'"
+  | DataValue.ofName _   => pure $ opts.setName key val.toName
+  | DataValue.ofNat _    =>
+    match val.toNat? with
+    | none   => throw s!"invalid Nat option value '{val}'"
+    | some v => pure $ opts.setNat key v
+  | DataValue.ofInt _    =>
+    match val.toInt? with
+    | none   => throw s!"invalid Int option value '{val}'"
+    | some v => pure $ opts.setInt key v
+  | DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
+
+end Lean
+
+namespace Pantograph
+
+def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
+  metaM.run'
+def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
+  termElabM.run' (ctx := {
+    declName? := .none,
+    errToSorry := false,
+  }) |>.run'
+
+def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
+
+/-- Adds the given paths to Lean package search path -/
+@[export pantograph_init_search]
+unsafe def initSearch (sp: String): IO Unit := do
+  Lean.enableInitializersExecution
+  Lean.initSearchPath (← Lean.findSysroot) (sp := System.SearchPath.parse sp)
+
+/-- Creates a Core.Context object needed to run all monads -/
+@[export pantograph_create_core_context]
+def createCoreContext (options: Array String): IO Lean.Core.Context := do
+  let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run
+  let options ← match options? with
+    | .ok options => pure options
+    | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
+  return {
+    currNamespace := Lean.Name.str .anonymous "Aniva"
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0] },
+    options := options
+  }
+
+/-- Creates a Core.State object needed to run all monads -/
+@[export pantograph_create_core_state]
+def createCoreState (imports: Array String): IO Lean.Core.State := do
+  let env ← Lean.importModules
+    (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+  return { env := env }
+
+@[export pantograph_env_catalog_m]
+def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
+  Environment.catalog ({}: Protocol.EnvCatalog)
+
+@[export pantograph_mk_options]
+def mkOptions
+  (printJsonPretty: Bool)
+  (printExprPretty: Bool)
+  (printExprAST: Bool)
+  (noRepeat: Bool)
+  (printAuxDecls: Bool)
+  (printImplementationDetailHyps: Bool)
+  : Protocol.Options := {
+    printJsonPretty,
+    printExprPretty,
+    printExprAST,
+    noRepeat,
+    printAuxDecls,
+    printImplementationDetailHyps,
+  }
+
+@[export pantograph_env_inspect_m]
+def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
+    Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
+  Environment.inspect ({
+    name, value? := .some value, dependency?:= .some dependency
+  }: Protocol.EnvInspect) options
+
+@[export pantograph_env_add_m]
+def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
+    Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
+  Environment.addDecl { name, type, value, isTheorem }
+
+/-- This must be a TermElabM since the parsed expr contains extra information -/
+def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
+  let env ← Lean.MonadEnv.getEnv
+  let syn ← match syntax_from_str env s with
+    | .error str => return .error $ errorI "parsing" str
+    | .ok syn => pure syn
+  match ← syntax_to_expr syn with
+  | .error str => return .error $ errorI "elab" str
+  | .ok expr => return .ok expr
+
+@[export pantograph_expr_echo_m]
+def exprEcho (expr: String) (options: @&Protocol.Options):
+    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
+  let termElabM: Lean.Elab.TermElabM _ := do
+    let expr ← match ← exprParse expr with
+      | .error e => return .error e
+      | .ok expr => pure expr
+    try
+      let type ← Lean.Meta.inferType expr
+      return .ok {
+          type := (← serialize_expression options type),
+          expr := (← serialize_expression options expr)
+      }
+    catch exception =>
+      return .error $ errorI "typing" (← exception.toMessageData.toString)
+  runTermElabM termElabM
+
+@[export pantograph_goal_start_expr_m]
+def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
+  let termElabM: Lean.Elab.TermElabM _ := do
+    let expr ← match ← exprParse expr with
+      | .error e => return .error e
+      | .ok expr => pure $ expr
+    return .ok $ ← GoalState.create expr
+  runTermElabM termElabM
+
+@[export pantograph_goal_tactic_m]
+def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
+  runTermElabM <| GoalState.execute state goalId tactic
+
+@[export pantograph_goal_try_assign_m]
+def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
+  runTermElabM <| GoalState.tryAssign state goalId expr
+
+@[export pantograph_goal_continue]
+def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  target.continue branch
+
+@[export pantograph_goal_resume]
+def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
+  target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
+
+@[export pantograph_goal_serialize_m]
+def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
+  runMetaM <| state.serializeGoals (parent := .none) options
+
+@[export pantograph_goal_print_m]
+def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
+  let metaM := do
+    state.restoreMetaM
+    return {
+      root? := ← state.rootExpr?.mapM (λ expr => do
+        serialize_expression options (← unfoldAuxLemmas expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr => do
+        serialize_expression options (← unfoldAuxLemmas expr)),
+    }
+  runMetaM metaM
+
+
+end Pantograph
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -124,8 +124,8 @@ structure EnvInspect where
 structure InductInfo where
  numParams: Nat
  numIndices: Nat
-  all: List String
-  ctors: List String
+  all: Array String
+  ctors: Array String
  isRec:       Bool := false
  isReflexive: Bool := false
  isNested:    Bool := false
@ -138,7 +138,7 @@ structure ConstructorInfo where
  numFields: Nat
  deriving Lean.ToJson
 structure RecursorInfo where
-  all: List String
+  all: Array String
  numParams: Nat
  numIndices: Nat
  numMotives: Nat
@ -163,7 +163,7 @@ structure EnvAdd where
  name: String
  type: String
  value: String
-  isTheorem?: Bool
+  isTheorem: Bool
  deriving Lean.FromJson
 structure EnvAddResult where
  deriving Lean.ToJson
@ -221,7 +221,7 @@ structure GoalContinue where
  -- The state which is an ancestor of `target` where goals will be extracted from
  branch?: Option Nat := .none
  -- Or, the particular goals that should be brought back into scope
-  goals?: Option (List String) := .none
+  goals?: Option (Array String) := .none
  deriving Lean.FromJson
 structure GoalContinueResult where
  nextStateId: Nat
@ -230,6 +230,7 @@ structure GoalContinueResult where

 -- Remove goal states
 structure GoalDelete where
+  -- This is ok being a List because it doesn't show up in the ABI
  stateIds: List Nat
  deriving Lean.FromJson
 structure GoalDeleteResult where
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -6,17 +6,20 @@ import Lean
 import Pantograph.Protocol
 import Pantograph.Goal

-namespace Pantograph
 open Lean

+-- Symbol processing functions --
+
+def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
+
+namespace Pantograph
+
+/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
+def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+
 --- Input Functions ---

-
-/-- Read a theorem from the environment -/
-def expr_from_const (env: Environment) (name: Name): Except String Lean.Expr :=
-  match env.find? name with
-  | none       => throw s!"Symbol not found: {name}"
-  | some cInfo => return cInfo.type
 /-- Read syntax object from string -/
 def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
  Parser.runParserCategory
@ -157,7 +160,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
    | .instImplicit => " :instImplicit"
  of_name (name: Name) := name_to_ast name sanitize

-def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
+def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
  let pp := toString (← Meta.ppExpr e)
  let pp?: Option String := match options.printExprPretty with
    | true => .some pp
@ -172,7 +175,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
  }

 /-- Adapted from ppGoal -/
-def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
      : MetaM Protocol.Goal := do
  -- Options for printing; See Meta.ppGoal for details
  let showLetValues  := true
@ -242,7 +245,11 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar
  where
  of_name (n: Name) := name_to_ast n (sanitize := false)

-protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
+protected def GoalState.serializeGoals
+      (state: GoalState)
+      (parent: Option GoalState := .none)
+      (options: @&Protocol.Options := {}):
+    MetaM (Array Protocol.Goal):= do
  state.restoreMetaM
  let goals := state.goals.toArray
  let parentDecl? := parent.bind (λ parentState =>
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@ -1,5 +1,6 @@
 namespace Pantograph

-def version := "0.2.12-alpha"
+@[export pantograph_version]
+def version := "0.2.14"

 end Pantograph
--- a/README.md
+++ b/README.md
@ -1,11 +1,16 @@
 # Pantograph

-An interaction system for Lean 4.
+A Machine-to-Machine interaction system for Lean 4.

 ![Pantograph](doc/icon.svg)

+Pantograph provides interfaces to execute proofs, construct expressions, and
+examine the symbol list of a Lean project for machine learning.
+
 ## Installation

+For Nix based workflow, see below.
+
 Install `elan` and `lake`. Execute
 ``` sh
 make build/bin/pantograph
@ -20,7 +25,7 @@ LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```
 The provided `flake.nix` has a develop environment with Lean already setup.

-## Usage
+## Executable Usage

 ``` sh
 pantograph MODULES|LEAN_OPTIONS
@ -63,7 +68,7 @@ stat
 ```
 where the application of `assumption` should lead to a failure.

-## Commands
+### Commands

 See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
 - `reset`: Delete all cached expressions and proof trees
@ -82,7 +87,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
 - `goal.print {"stateId": <id>}"`: Print a goal state
 - `stat`: Display resource usage

-## Errors
+### Errors

 When an error pertaining to the execution of a command happens, the returning JSON structure is

@ -97,16 +102,38 @@ Common error forms:
  input of another is broken. For example, attempting to query a symbol not
  existing in the library or indexing into a non-existent proof state.

-## Troubleshooting
+### Troubleshooting

 If lean encounters stack overflow problems when printing catalog, execute this before running lean:
 ```sh
 ulimit -s unlimited
 ```

-## Testing
+## Library Usage
+
+`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
+with `Pantograph` which mirrors the REPL commands above. It is recommended to
+call Pantograph via this FFI since it provides a tremendous speed up.
+
+## Developing
+
+### Testing

 The tests are based on `LSpec`. To run tests,
 ``` sh
 make test
 ```
+
+## Nix based workflow
+
+The included Nix flake provides build targets for `sharedLib` and `executable`.
+The executable can be used as-is, but linking against the shared library
+requires the presence of `lean-all`.
+
+To run tests:
+``` sh
+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.
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -1,7 +1,11 @@
-import Pantograph.Protocol
 import Pantograph.Goal
+import Pantograph.Library
+import Pantograph.Protocol
+import Lean
 import LSpec

+open Lean
+
 namespace Pantograph

 namespace Protocol
@ -35,12 +39,7 @@ def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message fa
 open Lean

 def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do
-  let coreContext: Core.Context := {
-    currNamespace := Name.str .anonymous "Aniva"
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph/Test>",
-    fileMap := { source := "", positions := #[0], lines := #[1] }
-  }
+  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}" = "")
@ -53,4 +52,9 @@ def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α
    errToSorry := false,
  })

+def defaultTermElabMContext: Lean.Elab.Term.Context := {
+    declName? := some "_pantograph".toName,
+    errToSorry := false
+  }
+
 end Pantograph
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -2,25 +2,41 @@ import LSpec
 import Pantograph.Serial
 import Pantograph.Environment
 import Test.Common
+import Lean

+open Lean
 namespace Pantograph.Test.Environment

 open Pantograph
-open Lean

 deriving instance DecidableEq, Repr for Protocol.InductInfo
 deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
 deriving instance DecidableEq, Repr for Protocol.RecursorInfo
 deriving instance DecidableEq, Repr for Protocol.EnvInspectResult

-def test_symbol_visibility (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 =>
+      match (Environment.toFilteredSymbol name info).isSome && (name matches .num _ _) with
+      | false => acc
+      | true => acc.push name
+      )
+    return LSpec.check "No num symbols" (symbolsWithNum.size == 0)
+  runCoreMSeq env inner
+
+def test_symbol_visibility: IO LSpec.TestSeq := do
  let entries: List (Name × Bool) := [
    ("Nat.add_comm".toName, false),
-    ("Lean.Name".toName, true)
+    ("Lean.Name".toName, true),
+    ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
  ]
  let suite := entries.foldl (λ suites (symbol, target) =>
-    let constant := env.constants.find! symbol
-    let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target)
+    let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
    LSpec.TestSeq.append suites test) LSpec.TestSeq.done
  return suite

@ -29,13 +45,17 @@ 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,
      numIndices := 0,
-      all := ["Or"],
-      ctors := ["Or.inl", "Or.inr"],
+      all := #["Or"],
+      ctors := #["Or.inl", "Or.inr"],
    }),
    ("Except.ok", ConstantCat.ctor {
      induct := "Except",
@ -44,7 +64,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
      numFields := 1,
    }),
    ("Eq.rec", ConstantCat.recursor {
-      all := ["Eq"],
+      all := #["Eq"],
      numParams := 2,
      numIndices := 1,
      numMotives := 1,
@ -52,7 +72,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
      k := true,
    }),
    ("ForM.rec", ConstantCat.recursor {
-      all := ["ForM"],
+      all := #["ForM"],
      numParams := 3,
      numIndices := 0,
      numMotives := 1,
@ -75,13 +95,9 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
  runCoreMSeq env inner

 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 "Environment" $
-    (LSpec.group "Symbol visibility" (← test_symbol_visibility env)) ++
-    (LSpec.group "Inspect" (← test_inspect env))
+    (LSpec.group "Catalog" (← test_catalog)) ++
+    (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
+    (LSpec.group "Inspect" (← test_inspect))

 end Pantograph.Test.Environment
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -21,13 +21,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
  let context: Context := {
    imports := ["Init"]
  }
-  let coreContext: Lean.Core.Context := {
-    currNamespace := Lean.Name.str .anonymous "Aniva"
-    openDecls := [],
-    fileName := "<Test>",
-    fileMap := { source := "", positions := #[0], lines := #[1] },
-    options := Lean.Options.empty
-  }
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
  let commands: MainM LSpec.TestSeq :=
    steps.foldlM (λ suite step => do
      let result ← step
@ -39,7 +33,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
    return LSpec.check s!"Uncaught IO exception: {ex.toString}" false

 def test_option_modify : IO LSpec.TestSeq :=
-  let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
+  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 := {}
@ -148,7 +142,7 @@ def test_env : IO LSpec.TestSeq :=
    subroutine_step "env.inspect"
      [("name", .str name2)]
     (Lean.toJson ({
-       value? := .some { pp? := .some "fun a => Int.ofNat a + 1" },
+       value? := .some { pp? := .some "fun a => ↑a + 1" },
       type := { pp? := .some "Nat → Int" },
     }:
      Protocol.EnvInspectResult))
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -1,6 +1,6 @@
 import LSpec
 import Test.Environment
-import Test.Holes
+import Test.Metavar
 import Test.Integration
 import Test.Proofs
 import Test.Serial
@ -11,7 +11,7 @@ def main := do
  Lean.initSearchPath (← Lean.findSysroot)

  let suites := [
-    Holes.suite,
+    Metavar.suite,
    Integration.suite,
    Proofs.suite,
    Serial.suite,
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -2,8 +2,9 @@ import LSpec
 import Pantograph.Goal
 import Pantograph.Serial
 import Test.Common
+import Lean

-namespace Pantograph.Test.Holes
+namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean

@ -44,16 +45,8 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
 def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options

-  let coreContext: Lean.Core.Context := {
-    currNamespace := Name.append .anonymous "Aniva",
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph>",
-    fileMap := { source := "", positions := #[0], lines := #[1] }
-  }
-  let metaM := termElabM.run' (ctx := {
-    declName? := some "_pantograph",
-    errToSorry := false
-  })
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
+  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
  let coreM := metaM.run'
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
@ -93,6 +86,62 @@ def test_m_couple: TestM Unit := do
  addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[.some "2 ≤ 3", .some "3 ≤ 5"])
  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+def test_m_couple_simp: TestM Unit := do
+  let state? ← startProof "(2: Nat) ≤ 5"
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+  let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 2") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  let state1b ← match state2.continue state1 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ 2", .some "2 ≤ 5"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  let state3 ← match ← state1b.execute (goalId := 0) (tactic := "simp") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state4 ← match state3.continue state1b with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  let state5 ← match ← state4.execute (goalId := 0) (tactic := "simp") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  state5.restoreMetaM
+  let root ← match state5.rootExpr? with
+    | .some e => pure e
+    | .none =>
+      addTest $ assertUnreachable "(5 root)"
+      return ()
+  let rootStr: String := toString (← Lean.Meta.ppExpr root)
+  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 rootStr: String := toString (← Lean.Meta.ppExpr (← unfoldAuxLemmas root))
+  addTest $ LSpec.check "(5 root)" (rootStr = "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
@ -169,7 +218,7 @@ def test_partial_continuation: TestM Unit := do
      return ()
    | .ok state => pure state
  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

  -- Roundtrip
@ -183,7 +232,7 @@ def test_partial_continuation: TestM Unit := do
      return ()
    | .ok state => pure state
  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

  -- Continuation should fail if the state does not exist:
@ -204,6 +253,7 @@ def suite: IO LSpec.TestSeq := do
    (trustLevel := 1)
  let tests := [
    ("2 < 5", test_m_couple),
+    ("2 < 5", test_m_couple_simp),
    ("Proposition Generation", test_proposition_generation),
    ("Partial Continuation", test_partial_continuation)
  ]
@ -212,6 +262,6 @@ def suite: IO LSpec.TestSeq := do
    let tests ← proofRunner env tests
    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done

-  return LSpec.group "Holes" tests
+  return LSpec.group "Metavar" tests

-end Pantograph.Test.Holes
+end Pantograph.Test.Metavar
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -62,16 +62,8 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
 def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options

-  let coreContext: Lean.Core.Context := {
-    currNamespace := Name.append .anonymous "Aniva",
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph>",
-    fileMap := { source := "", positions := #[0], lines := #[1] }
-  }
-  let metaM := termElabM.run' (ctx := {
-    declName? := some "_pantograph",
-    errToSorry := false
-  })
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
+  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
  let coreM := metaM.run'
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
@ -232,13 +224,18 @@ def proof_or_comm: TestM Unit := do
  addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone

+  let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false)
+  -- This is due to delayed assignment
+  addTest $ LSpec.test "(2 parent)" (state2parent ==
+    "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
+
  let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false)
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.83))")
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))")
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
  let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
    | .success state => pure state
@ -247,7 +244,7 @@ def proof_or_comm: TestM Unit := do
      return ()
  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
  let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false)
-  addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.49)")
+  addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
  let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
    | .success state => pure state
@ -299,7 +296,7 @@ def proof_or_comm: TestM Unit := do

 def suite: IO LSpec.TestSeq := do
  let env: Lean.Environment ← Lean.importModules
-    (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
+    (imports := #[{ module := "Init".toName, runtimeOnly := false}])
    (opts := {})
    (trustLevel := 1)
  let tests := [
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -1,11 +1,12 @@
 import LSpec
 import Pantograph.Serial
 import Test.Common
+import Lean

+open Lean
 namespace Pantograph.Test.Serial

 open Pantograph
-open Lean

 deriving instance Repr, DecidableEq for Protocol.BoundExpression

@ -20,7 +21,7 @@ def test_name_to_ast: LSpec.TestSeq :=
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
  let entries: List (Name × Protocol.BoundExpression) := [
    ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
-    ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
+    ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" })
  ]
  let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
    let env ← MonadEnv.getEnv
@ -58,10 +59,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
    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 := {
-    declName? := some "_pantograph",
-    errToSorry := false
-  })
+  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
  runMetaMSeq env metaM

 -- Instance parsing
--- a/flake.lock
+++ b/flake.lock
@ -38,19 +38,22 @@
        "flake-utils": "flake-utils",
        "lean4-mode": "lean4-mode",
        "nix": "nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": [
+          "nixpkgs"
+        ],
+        "nixpkgs-old": "nixpkgs-old"
      },
      "locked": {
-        "lastModified": 1695693562,
-        "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
+        "lastModified": 1711508550,
+        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
        "owner": "leanprover",
        "repo": "lean4",
-        "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
+        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
        "type": "github"
      },
      "original": {
        "owner": "leanprover",
-        "ref": "v4.1.0",
+        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
        "repo": "lean4",
        "type": "github"
      }
@ -87,6 +90,23 @@
        "type": "github"
      }
    },
+    "lspec": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1701971219,
+        "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
+        "owner": "lurk-lab",
+        "repo": "LSpec",
+        "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "type": "github"
+      },
+      "original": {
+        "owner": "lurk-lab",
+        "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "repo": "LSpec",
+        "type": "github"
+      }
+    },
    "nix": {
      "inputs": {
        "lowdown-src": "lowdown-src",
@ -141,6 +161,23 @@
        "type": "github"
      }
    },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
    "nixpkgs-regression": {
      "locked": {
        "lastModified": 1643052045,
@ -158,22 +195,6 @@
      }
    },
    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1686089707,
-        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixpkgs-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs_3": {
      "locked": {
        "lastModified": 1697456312,
        "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=",
@ -193,7 +214,8 @@
      "inputs": {
        "flake-parts": "flake-parts",
        "lean": "lean",
-        "nixpkgs": "nixpkgs_3"
+        "lspec": "lspec",
+        "nixpkgs": "nixpkgs_2"
      }
    }
  },
--- a/flake.nix
+++ b/flake.nix
@ -4,7 +4,14 @@
  inputs = {
    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
    flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=v4.1.0";
+    lean = {
+      url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+    lspec = {
+      url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
+      flake = false;
+    };
  };

  outputs = inputs @ {
@ -12,6 +19,7 @@
    nixpkgs,
    flake-parts,
    lean,
+    lspec,
    ...
  } : flake-parts.lib.mkFlake { inherit inputs; } {
    flake = {
@ -22,17 +30,52 @@
    ];
    perSystem = { system, pkgs, ... }: let
      leanPkgs = lean.packages.${system};
+      lspecLib = leanPkgs.buildLeanPackage {
+        name = "LSpec";
+        roots = [ "Main" "LSpec" ];
+        src = "${lspec}";
+      };
      project = leanPkgs.buildLeanPackage {
        name = "Pantograph";
        roots = [ "Main" "Pantograph" ];
+        src = pkgs.lib.cleanSourceWith {
          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path) &&
+            !(pkgs.lib.hasSuffix "Makefile" path);
+        };
+      };
+      test = leanPkgs.buildLeanPackage {
+        name = "Test";
+        # NOTE: The src directory must be ./. since that is where the import
+        # root begins (e.g. `import Test.Environment` and not `import
+        # Environment`) and thats where `lakefile.lean` resides.
+        roots = [ "Test.Main" ];
+        deps = [ lspecLib project ];
+        src = pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "Pantograph" path);
+        };
      };
    in rec {
-      packages = project // {
-        inherit (leanPkgs) lean;
-        default = packages.executable;
+      packages = {
+        inherit (leanPkgs) lean lean-all;
+        inherit (project) sharedLib executable;
+        default = project.executable;
+      };
+      checks = {
+        test = pkgs.runCommand "test" {
+          buildInputs = [ test.executable leanPkgs.lean-all ];
+        } ''
+          #export LEAN_SRC_PATH="${./.}"
+          ${test.executable}/bin/test > $out
+        '';
+      };
+      devShells.default = pkgs.mkShell {
+        buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
      };
-      devShells.default = project.devShell;
    };
  };
 }
--- a/lake-manifest.json
+++ b/lake-manifest.json
@ -1,12 +1,14 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
 "packages":
- [{"git":
-   {"url": "https://github.com/lurk-lab/LSpec.git",
-    "subDir?": null,
-    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-    "opts": {},
+ [{"url": "https://github.com/lurk-lab/LSpec.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
   "name": "LSpec",
-    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-    "inherited": false}}],
- "name": "pantograph"}
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "pantograph",
+ "lakeDir": ".lake"}
--- a/lakefile.lean
+++ b/lakefile.lean
@ -4,6 +4,7 @@ open Lake DSL
 package pantograph

 lean_lib Pantograph {
+  defaultFacets := #[LeanLib.sharedFacet]
 }

@[default_target]
@ -14,7 +15,7 @@ lean_exe pantograph {
 }

 require LSpec from git
-  "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
+  "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
 lean_lib Test {
 }
 lean_exe test {
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:4.1.0
+leanprover/lean4:nightly-2024-03-27