Main.lean

@@ -2,7 +2,6 @@ import Lean.Data.Json
 import Lean.Environment
 
 import Pantograph.Version
-import Pantograph.Library
 import Pantograph
 
 -- Main IO functions
@@ -40,6 +39,35 @@ 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.
@@ -48,19 +76,35 @@ unsafe def main (args: List String): IO Unit := do
     println! s!"{version}"
     return
 
-  initSearch ""
+  Lean.enableInitializersExecution
+  Lean.initSearchPath (← Lean.findSysroot)
 
-  let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+  let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
-    |>.toArray |> createCoreContext
+    |>.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 imports:= args.filter (λ s => ¬ (s.startsWith "--"))
-  let coreState ← createCoreState imports.toArray
+
+  let env ← Lean.importModules
+    (imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
   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 coreState
+    discard <| coreM.toIO coreContext { env := env }
   catch ex =>
     IO.println "Uncaught IO exception"
     IO.println ex.toString

Makefile

@@ -1,8 +1,8 @@
-LIB := ./.lake/build/lib/Pantograph.olean
+LIB := build/lib/Pantograph.olean
-EXE := ./.lake/build/bin/pantograph
+EXE := build/bin/pantograph
 SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
 
-TEST_EXE := ./.lake/build/bin/test
+TEST_EXE := 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)
-	$(TEST_EXE)
+	lake env $(TEST_EXE)
 
 clean:
 	lake clean

Pantograph.lean

@@ -2,7 +2,6 @@ import Pantograph.Goal
 import Pantograph.Protocol
 import Pantograph.Serial
 import Pantograph.Environment
-import Pantograph.Library
 import Lean.Data.HashMap
 
 namespace Pantograph
@@ -22,6 +21,14 @@ 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
@@ -49,6 +56,7 @@ 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
@@ -62,8 +70,7 @@ 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
-    let result ← Environment.catalog args
+    Environment.catalog args
-    return .ok result
   env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
     let state ← get
     Environment.inspect args state.options
@@ -71,7 +78,22 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
-    exprEcho args.expr state.options
+    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))
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options
@@ -93,11 +115,13 @@ 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 => do
+      | .some expr, .none =>
-        let expr ← match ← exprParse expr with
+        (match syntax_from_str env expr with
-          | .error e => return .error e
+        | .error str => return .error <| errorI "parsing" str
-          | .ok expr => pure $ expr
+        | .ok syn => do
-        return .ok $ ← GoalState.create expr
+          (match ← syntax_to_expr syn with
+          | .error str => return .error <| errorI "elab" str
+          | .ok expr => return .ok (← GoalState.create expr)))
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
@@ -120,9 +144,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 (← goalTactic goalState args.goalId tactic))
+          pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic))
         | .none, .some expr => do
-          pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
+          pure ( Except.ok (← runTermElabM <| GoalState.tryAssign 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
@@ -154,7 +178,8 @@ 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 =>
-          pure $ goalResume target goals
+          let goals := goals.map (λ name => { name := name.toName })
+          pure $ target.resume goals
         | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
       match nextState? with
       | .error error => return .error <| errorI "structure" error
@@ -164,7 +189,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           goalStates := state.goalStates.insert nextStateId nextGoalState,
           nextId := state.nextId + 1
         }
-        let goals ← goalSerialize nextGoalState (options := state.options)
+        let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run'
         return .ok {
           nextStateId,
           goals,
@@ -179,6 +204,10 @@ 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
-      return .ok (← goalPrint goalState state.options)
+      goalState.restoreMetaM
+      let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
+      return .ok {
+        root?,
+      }
 
 end Pantograph

Pantograph/Environment.lean

@@ -7,15 +7,16 @@ open Pantograph
 
 namespace Pantograph.Environment
 
-def isNameInternal (n: Lean.Name): Bool :=
+abbrev CR α := Except Protocol.InteractionError α
-  -- 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
+def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
+  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe
   where
   isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
     | .str _ name => name == "Lean"
     | _ => true
 
-def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
   let pref := match info with
   | .axiomInfo  _ => "a"
   | .defnInfo   _ => "d"
@@ -27,18 +28,18 @@ def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
   | .recInfo    _ => "r"
   s!"{pref}{toString n}"
 
-def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
+def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
-  if isNameInternal n || info.isUnsafe
+  if is_symbol_unsafe_or_internal n info
   then Option.none
-  else Option.some <| toCompactSymbolName n info
+  else Option.some <| to_compact_symbol_name n info
-def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
+def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := do
   let env ← Lean.MonadEnv.getEnv
   let names := env.constants.fold (init := #[]) (λ acc name info =>
-    match toFilteredSymbol name info with
+    match to_filtered_symbol name info with
     | .some x => acc.push x
     | .none => acc)
-  return { symbols := names }
+  return .ok { symbols := names }
-def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
+def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR Protocol.EnvInspectResult) := do
   let env ← Lean.MonadEnv.getEnv
   let name :=  args.name.toName
   let info? := env.find? name
@@ -59,22 +60,16 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     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
+    typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
-      then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n)
+    valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
-      else .none,
-    valueDependency? := ← if args.dependency?.getD false
-      then info.value?.mapM (λ e => do
-        let e ← unfoldAuxLemmas e
-        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.toArray.map (·.toString),
+          all := induct.all.map (·.toString),
-          ctors := induct.ctors.toArray.map (·.toString),
+          ctors := induct.ctors.map (·.toString),
           isRec := induct.isRec,
           isReflexive := induct.isReflexive,
           isNested := induct.isNested,
@@ -86,7 +81,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           numFields := ctor.numFields,
       } }
     | .recInfo r => { core with recursorInfo? := .some {
-          all := r.all.toArray.map (·.toString),
+          all := r.all.map (·.toString),
           numParams := r.numParams,
           numIndices := r.numIndices,
           numMotives := r.numMotives,
@@ -95,7 +90,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       } }
     | _ => core
   return .ok result
-def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
+def addDecl (args: Protocol.EnvAdd): CoreM (CR Protocol.EnvAddResult) := do
   let env ← Lean.MonadEnv.getEnv
   let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
     let type ← match syntax_from_str env args.type with

Pantograph/Goal.lean

@@ -1,4 +1,3 @@
-import Pantograph.Protocol
 import Lean
 
 def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
@@ -21,9 +20,6 @@ structure GoalState where
   -- The id of the goal in the parent
   parentGoalId: Nat := 0
 
-  -- Parent state metavariable source
-  parentMVar: Option MVarId
-
 abbrev M := Elab.TermElabM
 
 protected def GoalState.create (expr: Expr): M GoalState := do
@@ -40,7 +36,6 @@ protected def GoalState.create (expr: Expr): M GoalState := do
     savedState,
     root,
     newMVars := SSet.insert .empty root,
-    parentMVar := .none,
   }
 protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
 
@@ -119,11 +114,10 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
         return acc.insert mvarId
       ) SSet.empty
     return .success {
-      root := state.root,
+      state with
       savedState := nextSavedState
       newMVars,
       parentGoalId := goalId,
-      parentMVar := .some goal,
     }
 
 protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
@@ -170,11 +164,10 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
         Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
         let nextSavedState ← MonadBacktrack.saveState
         return .success {
-          root := state.root,
+          state with
           savedState := nextSavedState,
           newMVars := newMVars.toSSet,
           parentGoalId := goalId,
-          parentMVar := .some goal,
         }
     catch exception =>
       return .failure #[← exception.toMessageData.toString]
@@ -210,8 +203,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
   else
     target.resume (goals := branch.goals)
 
-protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
+protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
-  let expr ← goalState.mctx.eAssignment.find? goalState.root
+  let expr := goalState.mctx.eAssignment.find! goalState.root
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   if expr.hasMVar then
     -- Must not assert that the goal state is empty here. We could be in a branch goal.
@@ -219,16 +212,6 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
     .none
   else
     assert! goalState.goals.isEmpty
-    return expr
+    .some expr
-protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
-  let parent ← goalState.parentMVar
-  let expr := goalState.mctx.eAssignment.find! parent
-  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  return expr
-protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
-  let expr ← goalState.mctx.eAssignment.find? mvar
-  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  return expr
-
 
 end Pantograph

Pantograph/Library.lean

@@ -1,181 +0,0 @@
-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 ← unfoldAuxLemmas (← 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

Pantograph/Protocol.lean

@@ -124,8 +124,8 @@ structure EnvInspect where
 structure InductInfo where
   numParams: Nat
   numIndices: Nat
-  all: Array String
+  all: List String
-  ctors: Array String
+  ctors: List 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: Array String
+  all: List 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 (Array String) := .none
+  goals?: Option (List String) := .none
   deriving Lean.FromJson
 structure GoalContinueResult where
   nextStateId: Nat
@@ -230,7 +230,6 @@ 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
@@ -241,9 +240,7 @@ structure GoalPrint where
   deriving Lean.FromJson
 structure GoalPrintResult where
   -- The root expression
-  root?: Option Expression := .none
+  root?: Option Expression
-  -- The filling expression of the parent goal
-  parent?: Option Expression
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL
@@ -253,8 +250,6 @@ structure GoalDiag where
   printNewMVars: Bool := false
   -- Print all mvars
   printAll: Bool := false
-  instantiate: Bool := true
 
-abbrev CR α := Except InteractionError α
 
 end Pantograph.Protocol

Pantograph/Serial.lean

@@ -6,20 +6,17 @@ import Lean
 import Pantograph.Protocol
 import Pantograph.Goal
 
-open Lean
-
--- Symbol processing functions --
-
-def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
-
 namespace Pantograph
-
+open Lean
-/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM 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
@@ -160,7 +157,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
@@ -175,7 +172,7 @@ def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol
   }
 
 /-- 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
@@ -245,11 +242,7 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
   where
   of_name (n: Name) := name_to_ast n (sanitize := false)
 
-protected def GoalState.serializeGoals
+protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
-      (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 =>
@@ -283,6 +276,9 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
   mctx.decls.forM (fun mvarId decl => do
     if goals.contains mvarId || mvarId == root then
       pure ()
+    -- Always print the root goal
+    else if mvarId == goalState.root then
+      printMVar (pref := ">") mvarId decl
     -- Print the remainig ones that users don't see in Lean
     else if options.printAll then
       let pref := if goalState.newMVars.contains mvarId then "~" else " "
@@ -295,17 +291,11 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
     printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
       if options.printContext then
         decl.lctx.fvarIdToDecl.forM printFVar
-      let type ← if options.instantiate
+      let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
-        then instantiateMVars decl.type
-        else pure $ decl.type
-      let type_sexp ← serialize_expression_ast type (sanitize := false)
       IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
       if options.printValue then
         if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
-          let value ← if options.instantiate
+          IO.println s!"  = {← Meta.ppExpr value}"
-            then instantiateMVars value
-            else pure $ value
-          IO.println s!" := {← Meta.ppExpr value}"
     printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
       IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
     userNameToString : Name → String

Pantograph/Version.lean

@@ -1,6 +1,5 @@
 namespace Pantograph
 
-@[export pantograph_version]
+def version := "0.2.10-alpha"
-def version := "0.2.14"
 
 end Pantograph

README.md

@@ -1,16 +1,11 @@
 # Pantograph
 
-A Machine-to-Machine interaction system for Lean 4.
+An 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
@@ -25,7 +20,7 @@ LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```
 The provided `flake.nix` has a develop environment with Lean already setup.
 
-## Executable Usage
+## Usage
 
 ``` sh
 pantograph MODULES|LEAN_OPTIONS
@@ -68,7 +63,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
@@ -87,7 +82,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
 
@@ -102,38 +97,16 @@ 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
 ```
 
-## Library Usage
+## Testing
-
-`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.

Test/Common.lean

@@ -1,11 +1,7 @@
-import Pantograph.Goal
-import Pantograph.Library
 import Pantograph.Protocol
-import Lean
+import Pantograph.Goal
 import LSpec
 
-open Lean
-
 namespace Pantograph
 
 namespace Protocol
@@ -39,7 +35,12 @@ 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 ← createCoreContext #[]
+  let coreContext: Core.Context := {
+    currNamespace := Name.str .anonymous "Aniva"
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph/Test>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
@@ -52,9 +53,4 @@ def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α
     errToSorry := false,
   })
 
-def defaultTermElabMContext: Lean.Elab.Term.Context := {
-    declName? := some "_pantograph".toName,
-    errToSorry := false
-  }
-
 end Pantograph

Test/Environment.lean

@@ -2,41 +2,25 @@ 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_catalog: IO LSpec.TestSeq := do
+def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
-  let inner: CoreM LSpec.TestSeq := do
-    let catalogResult ← Environment.catalog {}
-    let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info =>
-      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 test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
+    let constant := env.constants.find! symbol
+    let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target)
     LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   return suite
 
@@ -45,17 +29,13 @@ inductive ConstantCat where
   | ctor (info: Protocol.ConstructorInfo)
   | recursor (info: Protocol.RecursorInfo)
 
-def test_inspect: IO LSpec.TestSeq := do
+def test_inspect (env: Environment): IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
   let testCases: List (String × ConstantCat) := [
     ("Or", ConstantCat.induct {
       numParams := 2,
       numIndices := 0,
-      all := #["Or"],
+      all := ["Or"],
-      ctors := #["Or.inl", "Or.inr"],
+      ctors := ["Or.inl", "Or.inr"],
     }),
     ("Except.ok", ConstantCat.ctor {
       induct := "Except",
@@ -64,7 +44,7 @@ def test_inspect: IO LSpec.TestSeq := do
       numFields := 1,
     }),
     ("Eq.rec", ConstantCat.recursor {
-      all := #["Eq"],
+      all := ["Eq"],
       numParams := 2,
       numIndices := 1,
       numMotives := 1,
@@ -72,7 +52,7 @@ def test_inspect: IO LSpec.TestSeq := do
       k := true,
     }),
     ("ForM.rec", ConstantCat.recursor {
-      all := #["ForM"],
+      all := ["ForM"],
       numParams := 3,
       numIndices := 0,
       numMotives := 1,
@@ -95,9 +75,13 @@ def test_inspect: 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 "Catalog" (← test_catalog)) ++
+    (LSpec.group "Symbol visibility" (← test_symbol_visibility env)) ++
-    (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
+    (LSpec.group "Inspect" (← test_inspect env))
-    (LSpec.group "Inspect" (← test_inspect))
 
 end Pantograph.Test.Environment

Test/Holes.lean

@@ -2,9 +2,8 @@ import LSpec
 import Pantograph.Goal
 import Pantograph.Serial
 import Test.Common
-import Lean
 
-namespace Pantograph.Test.Metavar
+namespace Pantograph.Test.Holes
 open Pantograph
 open Lean
 
@@ -13,27 +12,6 @@ abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
 def addTest (test: LSpec.TestSeq): TestM Unit := do
   set $ (← get) ++ test
 
--- Tests that all delay assigned mvars are instantiated
-def test_instantiate_mvar: TestM Unit := do
-  let env ← Lean.MonadEnv.getEnv
-  let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
-  let syn ← match syntax_from_str env value with
-    | .ok s => pure $ s
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let expr ← match ← syntax_to_expr syn with
-    | .ok expr => pure $ expr
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let t ← Lean.Meta.inferType expr
-  addTest $ LSpec.check "typing" ((toString (← serialize_expression_ast 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
   let env ← Lean.MonadEnv.getEnv
   let syn? := syntax_from_str env expr
@@ -66,8 +44,16 @@ 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 ← createCoreContext #[]
+  let coreContext: Lean.Core.Context := {
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+    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 coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
@@ -107,63 +93,6 @@ 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 unfoldedRoot ←  unfoldAuxLemmas root
-  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
@@ -240,7 +169,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 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Roundtrip
@@ -254,7 +183,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 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Continuation should fail if the state does not exist:
@@ -274,9 +203,7 @@ def suite: IO LSpec.TestSeq := do
     (opts := {})
     (trustLevel := 1)
   let tests := [
-    ("Instantiate", test_instantiate_mvar),
     ("2 < 5", test_m_couple),
-    ("2 < 5", test_m_couple_simp),
     ("Proposition Generation", test_proposition_generation),
     ("Partial Continuation", test_partial_continuation)
   ]
@@ -285,6 +212,6 @@ def suite: IO LSpec.TestSeq := do
     let tests ← proofRunner env tests
     return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
 
-  return LSpec.group "Metavar" tests
+  return LSpec.group "Holes" tests
 
-end Pantograph.Test.Metavar
+end Pantograph.Test.Holes

Test/Integration.lean

@@ -21,7 +21,13 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
   let context: Context := {
     imports := ["Init"]
   }
-  let coreContext: Lean.Core.Context ← createCoreContext #[]
+  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 commands: MainM LSpec.TestSeq :=
     steps.foldlM (λ suite step => do
       let result ← step
@@ -33,7 +39,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 = n.succ"
+  let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
   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 := {}
@@ -97,12 +103,6 @@ def test_tactic : IO LSpec.TestSeq :=
        goals? := #[goal1],
      }:
       Protocol.GoalTacticResult)),
-    subroutine_step "goal.print"
-      [("stateId", .num 1)]
-     (Lean.toJson ({
-       parent? := .some { pp? := .some "fun x => ?m.11 x" },
-     }:
-      Protocol.GoalPrintResult)),
     subroutine_step "goal.tactic"
       [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      (Lean.toJson ({
@@ -142,7 +142,7 @@ def test_env : IO LSpec.TestSeq :=
     subroutine_step "env.inspect"
       [("name", .str name2)]
      (Lean.toJson ({
-       value? := .some { pp? := .some "fun a => ↑a + 1" },
+       value? := .some { pp? := .some "fun a => Int.ofNat a + 1" },
        type := { pp? := .some "Nat → Int" },
      }:
       Protocol.EnvInspectResult))

Test/Main.lean

@@ -1,6 +1,6 @@
 import LSpec
 import Test.Environment
-import Test.Metavar
+import Test.Holes
 import Test.Integration
 import Test.Proofs
 import Test.Serial
@@ -11,7 +11,7 @@ def main := do
   Lean.initSearchPath (← Lean.findSysroot)
 
   let suites := [
-    Metavar.suite,
+    Holes.suite,
     Integration.suite,
     Proofs.suite,
     Serial.suite,

Test/Proofs.lean

@@ -62,8 +62,16 @@ 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 ← createCoreContext #[]
+  let coreContext: Lean.Core.Context := {
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+    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 coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
@@ -202,8 +210,6 @@ def proof_or_comm: TestM Unit := do
     | .none => do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
-  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
-  addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
 
   let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
     | .success state => pure state
@@ -212,8 +218,6 @@ def proof_or_comm: TestM Unit := do
       return ()
   addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
-  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
-  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
   let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
     | .success state => pure state
     | other => do
@@ -221,21 +225,12 @@ def proof_or_comm: TestM Unit := do
       return ()
   addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[branchGoal "inl" "p", branchGoal "inr" "q"])
-  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.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
@@ -243,8 +238,6 @@ def proof_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       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.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
@@ -296,7 +289,7 @@ def proof_or_comm: TestM Unit := do
 
 def suite: IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
-    (imports := #[{ module := "Init".toName, runtimeOnly := false}])
+    (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
     (opts := {})
     (trustLevel := 1)
   let tests := [

Test/Serial.lean

@@ -1,12 +1,11 @@
 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
 
@@ -21,7 +20,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", "n.succ ≤ m")], target := "n ≤ m" })
+    ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
   ]
   let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
@@ -59,7 +58,10 @@ 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 := defaultTermElabMContext)
+  let metaM := termElabM.run' (ctx := {
+    declName? := some "_pantograph",
+    errToSorry := false
+  })
   runMetaMSeq env metaM
 
 -- Instance parsing

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1709336216,
+        "lastModified": 1696343447,
-        "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
+        "narHash": "sha256-B2xAZKLkkeRFG5XcHHSXXcP7To9Xzr59KXeZiRf4vdQ=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
+        "rev": "c9afaba3dfa4085dbd2ccb38dfade5141e33d9d4",
         "type": "github"
       },
       "original": {
@@ -38,20 +38,19 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2",
+        "nixpkgs": "nixpkgs_2"
-        "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
-        "lastModified": 1711508550,
+        "lastModified": 1695693562,
-        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
+        "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
+        "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
+        "ref": "v4.1.0",
         "repo": "lean4",
         "type": "github"
       }
@@ -88,23 +87,6 @@
         "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",
@@ -144,11 +126,11 @@
     "nixpkgs-lib": {
       "locked": {
         "dir": "lib",
-        "lastModified": 1709237383,
+        "lastModified": 1696019113,
-        "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
+        "narHash": "sha256-X3+DKYWJm93DRSdC5M6K5hLqzSya9BjibtBsuARoPco=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
+        "rev": "f5892ddac112a1e9b3612c39af1b72987ee5783a",
         "type": "github"
       },
       "original": {
@@ -159,23 +141,6 @@
         "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,
@@ -210,11 +175,11 @@
     },
     "nixpkgs_3": {
       "locked": {
-        "lastModified": 1711703276,
+        "lastModified": 1697456312,
-        "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
+        "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
+        "rev": "ca012a02bf8327be9e488546faecae5e05d7d749",
         "type": "github"
       },
       "original": {
@@ -228,7 +193,6 @@
       "inputs": {
         "flake-parts": "flake-parts",
         "lean": "lean",
-        "lspec": "lspec",
         "nixpkgs": "nixpkgs_3"
       }
     }

flake.nix

@@ -4,14 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean = {
+    lean.url = "github:leanprover/lean4?ref=v4.1.0";
-      url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
-      # Do not follow input's nixpkgs since it could cause build failures
-    };
-    lspec = {
-      url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
-      flake = false;
-    };
   };
 
   outputs = inputs @ {
@@ -19,7 +12,6 @@
     nixpkgs,
     flake-parts,
     lean,
-    lspec,
     ...
   } : flake-parts.lib.mkFlake { inherit inputs; } {
     flake = {
@@ -30,52 +22,17 @@
     ];
     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 = ./.;
-          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 = {
+      packages = project // {
-        inherit (leanPkgs) lean lean-all;
+        inherit (leanPkgs) lean;
-        inherit (project) sharedLib executable;
+        default = packages.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;
     };
   };
 }

lake-manifest.json

@@ -1,14 +1,12 @@
-{"version": 7,
+{"version": 6,
- "packagesDir": ".lake/packages",
+ "packagesDir": "lake-packages",
  "packages":
- [{"url": "https://github.com/lurk-lab/LSpec.git",
+ [{"git":
-   "type": "git",
+   {"url": "https://github.com/lurk-lab/LSpec.git",
-   "subDir": null,
+    "subDir?": null,
-   "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-   "name": "LSpec",
+    "opts": {},
-   "manifestFile": "lake-manifest.json",
+    "name": "LSpec",
-   "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-   "inherited": false,
+    "inherited": false}}],
-   "configFile": "lakefile.lean"}],
+ "name": "pantograph"}
- "name": "pantograph",
- "lakeDir": ".lake"}

lakefile.lean

@@ -4,7 +4,6 @@ open Lake DSL
 package pantograph
 
 lean_lib Pantograph {
-  defaultFacets := #[LeanLib.sharedFacet]
 }
 
 @[default_target]
@@ -15,7 +14,7 @@ lean_exe pantograph {
 }
 
 require LSpec from git
-  "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
+  "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
 lean_lib Test {
 }
 lean_exe test {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-03-27
+leanprover/lean4:4.1.0