Main.lean

@@ -2,14 +2,13 @@ import Lean.Data.Json
 import Lean.Environment
 
 import Pantograph.Version
-import Pantograph.Library
 import Pantograph
 
 -- Main IO functions
 open Pantograph
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
-def parseCommand (s: String): Except String Protocol.Command := do
+def parse_command (s: String): Except String Commands.Command := do
   let s := s.trim
   match s.get? 0 with
   | .some '{' => -- Parse in Json mode
@@ -23,13 +22,13 @@ def parseCommand (s: String): Except String Protocol.Command := do
       return { cmd := s.take offset, payload := payload }
   | .none => throw "Command is empty"
 
-partial def loop : MainM Unit := do
+unsafe def loop : MainM Unit := do
   let state ← get
   let command ← (← IO.getStdin).getLine
   if command.trim.length = 0 then return ()
-  match parseCommand command with
+  match parse_command command with
   | .error error =>
-    let error  := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
+    let error  := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
     IO.println error.compress
   | .ok command =>
@@ -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 := Pantograph.str_to_name key
+  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,40 @@ 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_to_name str, 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' {}
+    let termElabM := loop.run context |>.run' {}
+    let metaM := termElabM.run' (ctx := {
+      declName? := some "_pantograph",
+      errToSorry := false
+    })
+    let coreM := metaM.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,20 +1,17 @@
-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)
-	lake build pantograph
+	lake build
 
 $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 	lake build test
 
 test: $(TEST_EXE)
-	$(TEST_EXE)
+	lake env $(TEST_EXE)
 
-clean:
+.PHONY: test
-	lake clean
-
-.PHONY: test clean

Pantograph.lean

@@ -1,9 +1,8 @@
-import Pantograph.Goal
+import Pantograph.Commands
-import Pantograph.Protocol
 import Pantograph.Serial
-import Pantograph.Environment
+import Pantograph.Symbols
-import Pantograph.Library
+import Pantograph.Tactic
-import Lean.Data.HashMap
+import Pantograph.SemihashMap
 
 namespace Pantograph
 
@@ -12,17 +11,16 @@ structure Context where
 
 /-- Stores state of the REPL -/
 structure State where
-  options: Protocol.Options := {}
+  options: Commands.Options := {}
-  nextId: Nat := 0
+  goalStates: SemihashMap GoalState := SemihashMap.empty
-  goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
 
-/-- Main state monad for executing commands -/
+-- State monad
-abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
+abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
--- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
+-- For some reason writing `CommandM α := MainM (Except ... α)` disables certain
--- certain monadic features in `MainM`
+-- monadic features in `MainM`
-abbrev CR α := Except Protocol.InteractionError α
+abbrev CR α := Except Commands.InteractionError α
 
-def execute (command: Protocol.Command): MainM Lean.Json := do
+def execute (command: Commands.Command): MainM Lean.Json := do
   let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
     match Lean.fromJson? command.payload with
     | .ok args => do
@@ -31,48 +29,79 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       | .error ierror => return Lean.toJson ierror
     | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
   match command.cmd with
-  | "reset"         => run reset
+  | "reset"          => run reset
-  | "stat"          => run stat
+  | "stat"           => run stat
-  | "expr.echo"     => run expr_echo
+  | "expr.echo"      => run expr_echo
-  | "env.catalog"   => run env_catalog
+  | "lib.catalog"    => run lib_catalog
-  | "env.inspect"   => run env_inspect
+  | "lib.inspect"    => run lib_inspect
-  | "env.add"       => run env_add
+  | "options.set"    => run options_set
-  | "options.set"   => run options_set
+  | "options.print"  => run options_print
-  | "options.print" => run options_print
+  | "goal.start"     => run goal_start
-  | "goal.start"    => run goal_start
+  | "goal.tactic"    => run goal_tactic
-  | "goal.tactic"   => run goal_tactic
+  | "goal.delete"    => run goal_delete
-  | "goal.continue" => run goal_continue
-  | "goal.delete"   => run goal_delete
-  | "goal.print"    => run goal_print
   | cmd =>
-    let error: Protocol.InteractionError :=
+    let error: Commands.InteractionError :=
       errorCommand s!"Unknown command {cmd}"
     return Lean.toJson error
   where
+  errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
   errorCommand := errorI "command"
   errorIndex := errorI "index"
   -- Command Functions
-  reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
+  reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do
     let state ← get
     let nGoals := state.goalStates.size
-    set { state with nextId := 0, goalStates := Lean.HashMap.empty }
+    set { state with goalStates := SemihashMap.empty }
     return .ok { nGoals }
-  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
+  stat (_: Commands.Stat): MainM (CR Commands.StatResult) := do
     let state ← get
     let nGoals := state.goalStates.size
     return .ok { nGoals }
-  env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
+  lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do
-    let result ← Environment.catalog args
+    let env ← Lean.MonadEnv.getEnv
-    return .ok result
+    let names := env.constants.fold (init := #[]) (λ acc name info =>
-  env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
+      match to_filtered_symbol name info with
+      | .some x => acc.push x
+      | .none => acc)
+    return .ok { symbols := names }
+  lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do
     let state ← get
-    Environment.inspect args state.options
+    let env ← Lean.MonadEnv.getEnv
-  env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
+    let name := str_to_name args.name
-    Environment.addDecl args
+    let info? := env.find? name
-  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
+    match info? with
+    | none => return .error $ errorIndex s!"Symbol not found {args.name}"
+    | some info =>
+      let module? := env.getModuleIdxFor? name >>=
+        (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
+      let value? := match args.value?, info with
+        | .some true, _ => info.value?
+        | .some false, _ => .none
+        | .none, .defnInfo _ => info.value?
+        | .none, _ => .none
+      return .ok {
+        type := ← serialize_expression state.options info.type,
+        value? := ← value?.mapM (λ v => serialize_expression state.options v),
+        module? := module?
+      }
+  expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do
     let state ← get
-    exprEcho args.expr state.options
+    let env ← Lean.MonadEnv.getEnv
-  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
+    match syntax_from_str env args.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 => 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: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
     let state ← get
     let options := state.options
     set { state with
@@ -81,104 +110,65 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
         printExprPretty := args.printExprPretty?.getD options.printExprPretty,
         printExprAST := args.printExprAST?.getD options.printExprAST,
-        noRepeat := args.noRepeat?.getD options.noRepeat,
+        proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta,
         printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
         printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
       }
     }
     return .ok {  }
-  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
+  options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
     return .ok (← get).options
-  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
+  goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
-    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
+    let expr?: Except _ Lean.Expr ← (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 expr))
       | .none, .some copyFrom =>
-        (match env.find? <| copyFrom.toName with
+        (match env.find? <| str_to_name copyFrom with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
-        | .some cInfo => return .ok (← GoalState.create cInfo.type))
+        | .some cInfo => return .ok cInfo.type)
-      | _, _ =>
+      | .none, .none =>
-        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
+        return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
+      | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
     match expr? with
     | .error error => return .error error
-    | .ok goalState =>
+    | .ok expr =>
-      let stateId := state.nextId
+      let goalState ← GoalState.create expr
-      set { state with
+      let (goalStates, goalId) := state.goalStates.insert goalState
-        goalStates := state.goalStates.insert stateId goalState,
+      set { state with goalStates }
-        nextId := state.nextId + 1
+      return .ok { goalId }
-      }
+  goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do
-      return .ok { stateId, root := goalState.root.name.toString }
-  goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
     let state ← get
-    match state.goalStates.find? args.stateId with
+    match state.goalStates.get? args.goalId with
-    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
+    | .none => return .error $ errorIndex s!"Invalid goal index {args.goalId}"
-    | .some goalState => do
+    | .some goalState =>
-      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
+      let result ← GoalState.execute goalState args.tactic |>.run state.options
-        | .some tactic, .none => do
+      match result with
-          pure ( Except.ok (← goalTactic goalState args.goalId tactic))
+      | .success goals =>
-        | .none, .some expr => do
+        if goals.isEmpty then
-          pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
+          return .ok {}
-        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
+        else
-      match nextGoalState? with
+          -- Append all goals
-      | .error error => return .error error
+          let (goalStates, goalIds, sGoals) := Array.foldl (λ acc itr =>
-      | .ok (.success nextGoalState) =>
+            let (map, indices, serializedGoals) := acc
-        let nextStateId := state.nextId
+            let (goalState, sGoal) := itr
-        set { state with
+            let (map, index) := map.insert goalState
-          goalStates := state.goalStates.insert state.nextId nextGoalState,
+            (map, index :: indices, sGoal :: serializedGoals)
-          nextId := state.nextId + 1,
+            ) (state.goalStates, [], []) goals
-        }
+          set { state with goalStates }
-        let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
+          return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray }
-        return .ok {
+      | .failure messages =>
-          nextStateId? := .some nextStateId,
-          goals? := .some goals,
-        }
-      | .ok (.parseError message) =>
-        return .ok { parseError? := .some message }
-      | .ok (.indexError goalId) =>
-        return .error $ errorIndex s!"Invalid goal id index {goalId}"
-      | .ok (.failure messages) =>
         return .ok { tacticErrors? := .some messages }
-  goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
+  goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do
     let state ← get
-    match state.goalStates.find? args.target with
+    let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates
-    | .none => return .error $ errorIndex s!"Invalid state index {args.target}"
-    | .some target => do
-      let nextState? ← match args.branch?, args.goals? with
-        | .some branchId, .none => do
-          match state.goalStates.find? branchId with
-          | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
-          | .some branch => pure $ target.continue branch
-        | .none, .some goals =>
-          pure $ goalResume target goals
-        | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
-      match nextState? with
-      | .error error => return .error <| errorI "structure" error
-      | .ok nextGoalState =>
-        let nextStateId := state.nextId
-        set { state with
-          goalStates := state.goalStates.insert nextStateId nextGoalState,
-          nextId := state.nextId + 1
-        }
-        let goals ← goalSerialize nextGoalState (options := state.options)
-        return .ok {
-          nextStateId,
-          goals,
-        }
-  goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
-    let state ← get
-    let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
     set { state with goalStates }
     return .ok {}
-  goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
-    let state ← get
-    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)
 
 end Pantograph

Pantograph/Commands.lean

@@ -6,7 +6,7 @@ its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
 
-namespace Pantograph.Protocol
+namespace Pantograph.Commands
 
 
 /-- Main Option structure, placed here to avoid name collision -/
@@ -18,10 +18,9 @@ structure Options where
   printExprPretty: Bool    := true
   -- When enabled, print the raw AST of expressions
   printExprAST: Bool       := false
-  -- When enabled, the types and values of persistent variables in a goal
+  -- When enabled, the types and values of persistent variables in a proof goal
-  -- are not shown unless they are new to the proof step. Reduces overhead.
+  -- are not shown unless they are new to the proof step. Reduces overhead
-  -- NOTE: that this assumes the type and assignment of variables can never change.
+  proofVariableDelta: Bool := false
-  noRepeat: Bool := false
   -- See `pp.auxDecls`
   printAuxDecls: Bool      := false
   -- See `pp.implementationDetailHyps`
@@ -44,19 +43,15 @@ structure Expression where
   deriving Lean.ToJson
 
 structure Variable where
-  /-- The internal name used in raw expressions -/
+  name: String
-  name: String := ""
-  /-- The name displayed to the user -/
-  userName: String
   /-- Does the name contain a dagger -/
   isInaccessible?: Option Bool := .none
   type?: Option Expression  := .none
   value?: Option Expression := .none
   deriving Lean.ToJson
 structure Goal where
-  name: String := ""
+  /-- String case id -/
-  /-- Name of the metavariable -/
+  caseName?: Option String  := .none
-  userName?: Option String  := .none
   /-- Is the goal in conversion mode -/
   isConversion: Bool        := false
   /-- target expression type -/
@@ -79,9 +74,6 @@ structure InteractionError where
   desc: String
   deriving Lean.ToJson
 
-def errorIndex (desc: String): InteractionError := { error := "index", desc }
-def errorExpr (desc: String): InteractionError := { error := "expr", desc }
-
 
 --- Individual command and return types ---
 
@@ -105,67 +97,22 @@ structure ExprEchoResult where
   deriving Lean.ToJson
 
 -- Print all symbols in environment
-structure EnvCatalog where
+structure LibCatalog where
   deriving Lean.FromJson
-structure EnvCatalogResult where
+structure LibCatalogResult where
   symbols: Array String
   deriving Lean.ToJson
-
 -- Print the type of a symbol
-structure EnvInspect where
+structure LibInspect where
   name: String
   -- If true/false, show/hide the value expressions; By default definitions
   -- values are shown and theorem values are hidden.
   value?: Option Bool := .some false
-  -- If true, show the type and value dependencies
-  dependency?: Option Bool := .some false
   deriving Lean.FromJson
--- See `InductiveVal`
+structure LibInspectResult where
-structure InductInfo where
-  numParams: Nat
-  numIndices: Nat
-  all: Array String
-  ctors: Array String
-  isRec:       Bool := false
-  isReflexive: Bool := false
-  isNested:    Bool := false
-  deriving Lean.ToJson
--- See `ConstructorVal`
-structure ConstructorInfo where
-  induct: String
-  cidx: Nat
-  numParams: Nat
-  numFields: Nat
-  deriving Lean.ToJson
-structure RecursorInfo where
-  all: Array String
-  numParams: Nat
-  numIndices: Nat
-  numMotives: Nat
-  numMinors: Nat
-  k: Bool
-  deriving Lean.ToJson
-structure EnvInspectResult where
   type: Expression
-  isUnsafe: Bool            := false
   value?: Option Expression := .none
-  module?: Option String    := .none
+  module?: Option String
-  -- If the name is private, displays the public facing name
-  publicName?: Option String := .none
-  typeDependency?: Option (Array String) := .none
-  valueDependency?: Option (Array String) := .none
-  inductInfo?:      Option InductInfo      := .none
-  constructorInfo?: Option ConstructorInfo := .none
-  recursorInfo?:    Option RecursorInfo    := .none
-  deriving Lean.ToJson
-
-structure EnvAdd where
-  name: String
-  type: String
-  value: String
-  isTheorem: Bool
-  deriving Lean.FromJson
-structure EnvAddResult where
   deriving Lean.ToJson
 
 /-- Set options; See `Options` struct above for meanings -/
@@ -173,7 +120,7 @@ structure OptionsSet where
   printJsonPretty?: Option Bool
   printExprPretty?: Option Bool
   printExprAST?: Option Bool
-  noRepeat?: Option Bool
+  proofVariableDelta?: Option Bool
   printAuxDecls?: Option Bool
   printImplementationDetailHyps?: Option Bool
   deriving Lean.FromJson
@@ -185,76 +132,32 @@ abbrev OptionsPrintResult := Options
 
 structure GoalStart where
   -- Only one of the fields below may be populated.
-  expr: Option String     -- Directly parse in an expression
+  expr: Option String     -- Proof expression
-  copyFrom: Option String -- Copy the type from a theorem in the environment
+  copyFrom: Option String -- Theorem name
   deriving Lean.FromJson
 structure GoalStartResult where
-  stateId: Nat := 0
+  goalId: Nat := 0 -- Proof tree id
-  -- Name of the root metavariable
-  root: String
   deriving Lean.ToJson
 structure GoalTactic where
   -- Identifiers for tree, state, and goal
-  stateId: Nat
+  goalId: Nat
-  goalId: Nat := 0
+  tactic: String
-  -- One of the fields here must be filled
-  tactic?: Option String := .none
-  expr?: Option String := .none
   deriving Lean.FromJson
 structure GoalTacticResult where
-  -- The next goal state id. Existence of this field shows success
+  -- Existence of this field shows success
-  nextStateId?: Option Nat          := .none
-  -- If the array is empty, it shows the goals have been fully resolved.
   goals?: Option (Array Goal)          := .none
-
+  -- Next proof state id, if successful
-  -- Existence of this field shows tactic execution failure
+  goalIds?: Option (Array Nat)          := .none
+  -- Existence of this field shows failure
   tacticErrors?: Option (Array String) := .none
-
-  -- Existence of this field shows the tactic parsing has failed
-  parseError?: Option String := .none
-  deriving Lean.ToJson
-structure GoalContinue where
-  -- State from which the continuation acquires the context
-  target: Nat
-
-  -- One of the following must be supplied
-  -- 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
-  deriving Lean.FromJson
-structure GoalContinueResult where
-  nextStateId: Nat
-  goals: (Array Goal)
   deriving Lean.ToJson
 
--- Remove goal states
+-- Remove a bunch of goals.
 structure GoalDelete where
-  -- This is ok being a List because it doesn't show up in the ABI
+  goalIds: List Nat
-  stateIds: List Nat
   deriving Lean.FromJson
 structure GoalDeleteResult where
   deriving Lean.ToJson
 
-structure GoalPrint where
-  stateId: Nat
-  deriving Lean.FromJson
-structure GoalPrintResult where
-  -- The root expression
-  root?: Option Expression := .none
-  -- The filling expression of the parent goal
-  parent?: Option Expression := .none
-  deriving Lean.ToJson
 
--- Diagnostic Options, not available in REPL
+end Pantograph.Commands
-structure GoalDiag where
-  printContext: Bool := true
-  printValue: Bool := true
-  printNewMVars: Bool := false
-  -- Print all mvars
-  printAll: Bool := false
-  instantiate: Bool := true
-
-abbrev CR α := Except InteractionError α
-
-end Pantograph.Protocol

Pantograph/Environment.lean

@@ -1,130 +0,0 @@
-import Pantograph.Protocol
-import Pantograph.Serial
-import Lean
-
-open Lean
-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
-  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 :=
-  let pref := match info with
-  | .axiomInfo  _ => "a"
-  | .defnInfo   _ => "d"
-  | .thmInfo    _ => "t"
-  | .opaqueInfo _ => "o"
-  | .quotInfo   _ => "q"
-  | .inductInfo _ => "i"
-  | .ctorInfo   _ => "c"
-  | .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
-  then Option.none
-  else Option.some <| to_compact_symbol_name 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
-    | .some x => acc.push x
-    | .none => acc)
-  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
-  let info ← match info? with
-    | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
-    | some info => pure info
-  let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
-  let value? := match args.value?, info with
-    | .some true, _ => info.value?
-    | .some false, _ => .none
-    | .none, .defnInfo _ => info.value?
-    | .none, _ => .none
-  -- Information common to all symbols
-  let core := {
-    type := ← (serialize_expression options info.type).run',
-    isUnsafe := info.isUnsafe,
-    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,
-    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),
-          ctors := induct.ctors.toArray.map (·.toString),
-          isRec := induct.isRec,
-          isReflexive := induct.isReflexive,
-          isNested := induct.isNested,
-      } }
-    | .ctorInfo ctor => { core with constructorInfo? := .some {
-          induct := ctor.induct.toString,
-          cidx := ctor.cidx,
-          numParams := ctor.numParams,
-          numFields := ctor.numFields,
-      } }
-    | .recInfo r => { core with recursorInfo? := .some {
-          all := r.all.toArray.map (·.toString),
-          numParams := r.numParams,
-          numIndices := r.numIndices,
-          numMotives := r.numMotives,
-          numMinors := r.numMinors,
-          k := r.k,
-      } }
-    | _ => core
-  return .ok result
-def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
-  let env ← Lean.MonadEnv.getEnv
-  let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
-    let type ← match syntax_from_str env args.type with
-      | .ok syn => do
-        match ← syntax_to_expr syn with
-        | .error e => return .error e
-        | .ok expr => pure expr
-      | .error e => return .error e
-    let value ← match syntax_from_str env args.value with
-      | .ok syn => do
-        try
-          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
-          Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
-          let expr ← instantiateMVars expr
-          pure $ expr
-        catch ex => return .error (← ex.toMessageData.toString)
-      | .error e => return .error e
-    pure $ .ok (type, value)
-  let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
-    | .ok t => pure t
-    | .error e => return .error $ Protocol.errorExpr e
-  let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
-    (name := args.name.toName)
-    (levelParams := [])
-    (type := type)
-    (value := value)
-    (hints := Lean.mkReducibilityHintsRegularEx 1)
-    (safety := Lean.DefinitionSafety.safe)
-    (all := [])
-  let env' ← match env.addDecl constant with
-    | .error e => do
-      let options ← Lean.MonadOptions.getOptions
-      let desc ← (e.toMessageData options).toString
-      return .error $ { error := "kernel", desc }
-    | .ok env' => pure env'
-  Lean.MonadEnv.modifyEnv (λ _ => env')
-  return .ok {}
-
-end Pantograph.Environment

Pantograph/Goal.lean

@@ -1,230 +0,0 @@
-import Pantograph.Protocol
-import Lean
-
-def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
-  {
-    msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
-  }
-
-
-namespace Pantograph
-open Lean
-
-structure GoalState where
-  savedState : Elab.Tactic.SavedState
-
-  -- The root hole which is the search target
-  root: MVarId
-  -- New metavariables acquired in this state
-  newMVars: SSet MVarId
-
-  -- 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
-  -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
-  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
-
-  --Elab.Term.synthesizeSyntheticMVarsNoPostponing
-  --let expr ← instantiateMVars expr
-  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
-  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
-  let root := goal.mvarId!
-  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
-  return {
-    savedState,
-    root,
-    newMVars := SSet.insert .empty root,
-    parentMVar := .none,
-  }
-protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
-
-protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
-  state.savedState.term.restore
-  m
-
-protected def GoalState.mctx (state: GoalState): MetavarContext :=
-  state.savedState.term.meta.meta.mctx
-protected def GoalState.env (state: GoalState): Environment :=
-  state.savedState.term.meta.core.env
-private def GoalState.mvars (state: GoalState): SSet MVarId :=
-  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
-private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
-  state.savedState.term.restore
-def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
-  state.savedState.term.meta.restore
-
-/-- Inner function for executing tactic on goal state -/
-def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
-    M (Except (Array String) Elab.Tactic.SavedState):= do
-  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
-    state.restore
-    Elab.Tactic.setGoals [goal]
-    try
-      Elab.Tactic.evalTactic stx
-      if (← getThe Core.State).messages.hasErrors then
-        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-        let errors ← (messages.map Message.data).mapM fun md => md.toString
-        return .error errors
-      else
-        return .ok (← MonadBacktrack.saveState)
-    catch exception =>
-      return .error #[← exception.toMessageData.toString]
-  tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
-
-/-- Response for executing a tactic -/
-inductive TacticResult where
-  -- Goes to next state
-  | success (state: GoalState)
-  -- Tactic failed with messages
-  | failure (messages: Array String)
-  -- Could not parse tactic
-  | parseError (message: String)
-  -- The goal index is out of bounds
-  | indexError (goalId: Nat)
-
-/-- Execute tactic on given state -/
-protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
-    M TacticResult := do
-  state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure $ goal
-    | .none => return .indexError goalId
-  let tactic ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `tactic)
-    (input := tactic)
-    (fileName := "<stdin>") with
-    | .ok stx => pure $ stx
-    | .error error => return .parseError error
-  match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
-  | .error errors =>
-    return .failure errors
-  | .ok nextSavedState =>
-    -- Assert that the definition of metavariables are the same
-    let nextMCtx := nextSavedState.term.meta.meta.mctx
-    let prevMCtx := state.savedState.term.meta.meta.mctx
-    -- Generate a list of mvarIds that exist in the parent state; Also test the
-    -- assertion that the types have not changed on any mvars.
-    let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
-      if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
-        assert! prevMVarDecl.type == mvarDecl.type
-        return acc
-      else
-        return acc.insert mvarId
-      ) SSet.empty
-    return .success {
-      root := state.root,
-      savedState := nextSavedState
-      newMVars,
-      parentGoalId := goalId,
-      parentMVar := .some goal,
-    }
-
-protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
-  state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  let expr ← match Parser.runParserCategory
-    (env := state.env)
-    (catName := `term)
-    (input := expr)
-    (fileName := "<stdin>") with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  let tacticM:  Elab.Tactic.TacticM TacticResult := do
-    state.savedState.restore
-    Elab.Tactic.setGoals [goal]
-    try
-      let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
-      -- Attempt to unify the expression
-      let goalType ← goal.getType
-      let exprType ← Meta.inferType expr
-      if !(← Meta.isDefEq goalType exprType) then
-        return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
-      goal.checkNotAssigned `GoalState.tryAssign
-      goal.assign expr
-      if (← getThe Core.State).messages.hasErrors then
-        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-        let errors ← (messages.map Message.data).mapM fun md => md.toString
-        return .failure errors
-      else
-        let prevMCtx := state.savedState.term.meta.meta.mctx
-        let nextMCtx ← getMCtx
-        -- Generate a list of mvarIds that exist in the parent state; Also test the
-        -- assertion that the types have not changed on any mvars.
-        let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
-          if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
-            assert! prevMVarDecl.type == mvarDecl.type
-            return acc
-          else
-            return mvarId :: acc
-          ) []
-        -- The new goals are the newMVars that lack an assignment
-        Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
-        let nextSavedState ← MonadBacktrack.saveState
-        return .success {
-          root := state.root,
-          savedState := nextSavedState,
-          newMVars := newMVars.toSSet,
-          parentGoalId := goalId,
-          parentMVar := .some goal,
-        }
-    catch exception =>
-      return .failure #[← exception.toMessageData.toString]
-  tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-
-/--
-Brings into scope a list of goals
--/
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
-  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
-    .error s!"Goals not in scope"
-  else
-    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
-    let unassigned := goals.filter (λ goal =>
-      let mctx := state.mctx
-      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
-    .ok {
-      state with
-      savedState := {
-        term := state.savedState.term,
-        tactic := { goals := unassigned },
-      },
-    }
-
-/--
-Brings into scope all goals from `branch`
--/
-protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
-  if !target.goals.isEmpty then
-    .error s!"Target state has unresolved goals"
-  else if target.root != branch.root then
-    .error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
-  else
-    target.resume (goals := branch.goals)
-
-protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
-  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.
-    --assert! ¬goalState.goals.isEmpty
-    .none
-  else
-    assert! goalState.goals.isEmpty
-    return 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
-
-
-end Pantograph

Pantograph/Library.lean

@@ -1,179 +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 ← 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 => serialize_expression options expr),
-      parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr),
-    }
-  runMetaM metaM
-
-
-end Pantograph

Pantograph/SemihashMap.lean

@@ -0,0 +1,149 @@
+
+namespace Pantograph.SemihashMap
+
+structure Imp (β: Type u) where
+  data: Array (Option β)
+
+  -- Number of elements currently in use
+  size: Nat
+
+  -- Next index that has never been touched
+  allocFront: Nat
+
+  -- Deallocated indices
+  deallocs: Array Nat
+
+  -- Number of valid entries in `deallocs` array
+  lastDealloc: Nat
+
+namespace Imp
+
+structure WF (m: Imp β): Prop where
+  capacity: m.data.size = m.deallocs.size
+  front_dealloc: ∀ i: Fin m.deallocs.size, (i < m.allocFront) → (m.deallocs.get i) < m.allocFront
+  front_data: ∀ i: Fin m.data.size, (i ≥ m.allocFront) → (m.data.get i).isNone
+
+def empty (capacity := 16): Imp β :=
+  {
+    data := mkArray capacity .none,
+    size := 0,
+    allocFront := 0,
+    deallocs := mkArray capacity 0,
+    lastDealloc := 0,
+  }
+
+private theorem list_get_replicate (x: α) (i: Fin (List.replicate n x).length):
+    List.get (List.replicate n x) i = x := by
+  sorry
+
+theorem empty_wf : WF (empty n: Imp β) := by
+  unfold empty
+  apply WF.mk
+  case capacity =>
+    conv =>
+      lhs
+      congr
+      simp
+    conv =>
+      rhs
+      congr
+      simp
+    simp
+  case front_dealloc =>
+    simp_all
+    intro i
+    intro a
+    contradiction
+  case front_data =>
+    simp_all
+    intro i
+    unfold Imp.data at i
+    simp at i
+    conv =>
+      lhs
+      unfold Array.get
+      unfold mkArray
+      simp [List.replicate]
+      rewrite [list_get_replicate]
+
+-- FIXME: Merge this with the well-formed versions below so proof and code can
+-- mesh seamlessly.
+@[inline] def insert (map: Imp β) (v: β): (Imp β × Nat) :=
+  match map.lastDealloc with
+  | 0 => -- Capacity is full, buffer expansion is required
+    if map.size == map.data.size then
+      let nextIndex := map.data.size
+      let extendCapacity := map.size
+      let result: Imp β := {
+        data := (map.data.append #[Option.some v]).append (mkArray extendCapacity .none),
+        size := map.size + 1,
+        allocFront := map.size + 1,
+        deallocs := mkArray (map.data.size + 1 + extendCapacity) 0,
+        lastDealloc := 0,
+      }
+      (result, nextIndex)
+    else
+      let nextIndex := map.size
+      let result: Imp β := {
+        map
+        with
+        data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
+        size := map.size + 1,
+        allocFront := map.allocFront + 1,
+      }
+      (result, nextIndex)
+  | (.succ k) => -- Allocation list has space
+    let nextIndex := map.deallocs.get! k
+    let result: Imp β := {
+      map with
+      data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
+      size := map.size + 1,
+      lastDealloc := map.lastDealloc - 1
+    }
+    (result, nextIndex)
+
+@[inline] def remove (map: Imp β) (index: Fin (map.size)): Imp β :=
+  have h: index.val < map.data.size := by sorry
+  match map.data.get ⟨index.val, h⟩ with
+  | .none => map
+  | .some _ =>
+    {
+      map with
+      data := map.data.set ⟨index, sorry⟩ .none,
+      size := map.size - 1,
+      deallocs := map.deallocs.set ⟨map.lastDealloc, sorry⟩ index,
+      lastDealloc := map.lastDealloc + 1,
+    }
+
+/-- Retrieval is efficient -/
+@[inline] def get? (map: Imp β) (index: Fin (map.size)): Option β :=
+  have h: index.val < map.data.size := by sorry
+  map.data.get ⟨index.val, h⟩
+@[inline] def capacity (map: Imp β): Nat := map.data.size
+
+end Imp
+
+
+/--
+This is like a hashmap but you cannot control the keys.
+-/
+def _root_.Pantograph.SemihashMap β := {m: Imp β // m.WF}
+
+@[inline] def empty (capacity := 16): SemihashMap β :=
+  ⟨ Imp.empty capacity, Imp.empty_wf ⟩
+@[inline] def insert (map: SemihashMap β) (v: β): (SemihashMap β × Nat) :=
+  let ⟨imp, pre⟩ := map
+  let ⟨result, id⟩ := imp.insert v
+  ( ⟨ result, sorry ⟩, id)
+@[inline] def remove (map: SemihashMap β) (index: Nat): SemihashMap β :=
+  let ⟨imp, pre⟩ := map
+  let result := imp.remove ⟨index, sorry⟩
+  ⟨ result, sorry ⟩
+@[inline] def get? (map: SemihashMap β) (index: Nat): Option β :=
+  let ⟨imp, _⟩ := map
+  imp.get? ⟨index, sorry⟩
+@[inline] def size (map: SemihashMap β): Nat :=
+  let ⟨imp, _⟩ := map
+  imp.size
+
+end Pantograph.SemihashMap

Pantograph/Serial.lean

@@ -3,8 +3,7 @@ All serialisation functions
 -/
 import Lean
 
-import Pantograph.Protocol
+import Pantograph.Commands
-import Pantograph.Goal
 
 namespace Pantograph
 open Lean
@@ -26,154 +25,172 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
     (fileName := "<stdin>")
 
 
-/-- Parse a syntax object. May generate additional metavariables! -/
 def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
   try
     let expr ← Elab.Term.elabType syn
+    -- Immediately synthesise all metavariables if we need to leave the elaboration context.
+    -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
+    --Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    let expr ← instantiateMVars expr
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
 def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
   try
     let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
+    -- Immediately synthesise all metavariables if we need to leave the elaboration context.
+    -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
+    --Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    let expr ← instantiateMVars expr
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
 
 
 --- Output Functions ---
 
-def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
+def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do
   Meta.forallTelescope expr fun arr body => do
     let binders ← arr.mapM fun fvar => do
       return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
     return { binders, target := toString (← Meta.ppExpr body) }
 
-def name_to_ast (name: Name) (sanitize: Bool := true): String :=
+private def name_to_ast: Lean.Name → String
-  let internal := name.isInaccessibleUserName || name.hasMacroScopes
+  | .anonymous
-  if sanitize && internal then "_"
+  | .num _ _ => ":anon"
-  else toString name |> enclose_if_escaped
+  | n@(.str _ _) => toString n
-  where
+
-  enclose_if_escaped (n: String) :=
+private def level_depth: Level → Nat
-    let quote := "\""
+  | .zero => 0
-    if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
+  | .succ l => 1 + (level_depth l)
+  | .max u v | .imax u v => 1 + max (level_depth u) (level_depth v)
+  | .param _ | .mvar _ => 0
+
+theorem level_depth_max_imax (u v: Level): (level_depth (Level.max u v) = level_depth (Level.imax u v)) := by
+  constructor
+theorem level_max_depth_decrease (u v: Level): (level_depth u < level_depth (Level.max u v)) := by
+  have h1: level_depth (Level.max u v) = 1 + Nat.max (level_depth u) (level_depth v) := by constructor
+  rewrite [h1]
+  simp_arith
+  conv =>
+    rhs
+    apply Nat.max_def
+  sorry
+theorem level_offset_decrease (u v: Level): (level_depth u ≤ level_depth (Level.max u v).getLevelOffset) := sorry
 
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
+def serialize_sort_level_ast (level: Level): String :=
   let k := level.getOffset
   let u := level.getLevelOffset
   let u_str := match u with
     | .zero => "0"
     | .succ _ => panic! "getLevelOffset should not return .succ"
     | .max v w =>
-      let v := serialize_sort_level_ast v sanitize
+      let v := serialize_sort_level_ast v
-      let w := serialize_sort_level_ast w sanitize
+      let w := serialize_sort_level_ast w
       s!"(:max {v} {w})"
     | .imax v w =>
-      let v := serialize_sort_level_ast v sanitize
+      let v := serialize_sort_level_ast v
-      let w := serialize_sort_level_ast w sanitize
+      let w := serialize_sort_level_ast w
       s!"(:imax {v} {w})"
     | .param name =>
-      let name := name_to_ast name sanitize
+      let name := name_to_ast name
       s!"{name}"
     | .mvar id =>
-      let name := name_to_ast id.name sanitize
+      let name := name_to_ast id.name
       s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
+  termination_by serialize_sort_level_ast level => level_depth level
+  decreasing_by
+  . sorry
 
 /--
  Completely serializes an expression tree. Json not used due to compactness
 -/
-partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
+def serialize_expression_ast (expr: Expr): MetaM String := do
-  self expr
+  match expr with
+  | .bvar deBruijnIndex =>
+    -- This is very common so the index alone is shown. Literals are handled below.
+    -- The raw de Bruijn index should never appear in an unbound setting. In
+    -- Lean these are handled using a `#` prefix.
+    return s!"{deBruijnIndex}"
+  | .fvar fvarId =>
+    let name := (← fvarId.getDecl).userName
+    return s!"(:fv {name})"
+  | .mvar mvarId =>
+    let name := name_to_ast mvarId.name
+    return s!"(:mv {name})"
+  | .sort level =>
+    let level := serialize_sort_level_ast level
+    return s!"(:sort {level})"
+  | .const declName _ =>
+    -- The universe level of the const expression is elided since it should be
+    -- inferrable from surrounding expression
+    return s!"(:c {declName})"
+  | .app fn arg =>
+    let fn' ← serialize_expression_ast fn
+    let arg' ← serialize_expression_ast arg
+    return s!"({fn'} {arg'})"
+  | .lam binderName binderType body binderInfo =>
+    let binderName' := name_to_ast binderName
+    let binderType' ← serialize_expression_ast binderType
+    let body' ← serialize_expression_ast body
+    let binderInfo' := binder_info_to_ast binderInfo
+    return s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
+  | .forallE binderName binderType body binderInfo =>
+    let binderName' := name_to_ast binderName
+    let binderType' ← serialize_expression_ast binderType
+    let body' ← serialize_expression_ast body
+    let binderInfo' := binder_info_to_ast binderInfo
+    return s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
+  | .letE name type value body _ =>
+    -- Dependent boolean flag diacarded
+    let name' := name_to_ast name
+    let type' ← serialize_expression_ast type
+    let value' ← serialize_expression_ast value
+    let body' ← serialize_expression_ast body
+    return s!"(:let {name'} {type'} {value'} {body'})"
+  | .lit v =>
+    -- To not burden the downstream parser who needs to handle this, the literal
+    -- is wrapped in a :lit sexp.
+    let v' := match v with
+      | .natVal val => toString val
+      | .strVal val => s!"\"{val}\""
+    return s!"(:lit {v'})"
+  | .mdata _ expr =>
+    -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
+    -- It may become necessary to incorporate the metadata.
+    return (← serialize_expression_ast expr)
+  | .proj typeName idx struct =>
+    let struct' ← serialize_expression_ast struct
+    return s!"(:proj {typeName} {idx} {struct'})"
+
   where
-  self (e: Expr): MetaM String :=
-    match e with
-    | .bvar deBruijnIndex =>
-      -- This is very common so the index alone is shown. Literals are handled below.
-      -- The raw de Bruijn index should never appear in an unbound setting. In
-      -- Lean these are handled using a `#` prefix.
-      pure s!"{deBruijnIndex}"
-    | .fvar fvarId =>
-      let name := of_name fvarId.name
-      pure s!"(:fv {name})"
-    | .mvar mvarId =>
-      let name := of_name mvarId.name
-      pure s!"(:mv {name})"
-    | .sort level =>
-      let level := serialize_sort_level_ast level sanitize
-      pure s!"(:sort {level})"
-    | .const declName _ =>
-      -- The universe level of the const expression is elided since it should be
-      -- inferrable from surrounding expression
-      pure s!"(:c {declName})"
-    | .app _ _ => do
-      let fn' ← self e.getAppFn
-      let args := (← e.getAppArgs.mapM self) |>.toList
-      let args := " ".intercalate args
-      pure s!"({fn'} {args})"
-    | .lam binderName binderType body binderInfo => do
-      let binderName' := of_name binderName
-      let binderType' ← self binderType
-      let body' ← self body
-      let binderInfo' := binder_info_to_ast binderInfo
-      pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
-    | .forallE binderName binderType body binderInfo => do
-      let binderName' := of_name binderName
-      let binderType' ← self binderType
-      let body' ← self body
-      let binderInfo' := binder_info_to_ast binderInfo
-      pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
-    | .letE name type value body _ => do
-      -- Dependent boolean flag diacarded
-      let name' := name_to_ast name
-      let type' ← self type
-      let value' ← self value
-      let body' ← self body
-      pure s!"(:let {name'} {type'} {value'} {body'})"
-    | .lit v =>
-      -- To not burden the downstream parser who needs to handle this, the literal
-      -- is wrapped in a :lit sexp.
-      let v' := match v with
-        | .natVal val => toString val
-        | .strVal val => s!"\"{val}\""
-      pure s!"(:lit {v'})"
-    | .mdata _ inner =>
-      -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
-      -- It may become necessary to incorporate the metadata.
-      self inner
-    | .proj typeName idx inner => do
-      let env ← getEnv
-      let fieldName := getStructureFields env typeName |>.get! idx
-      let projectorName := getProjFnForField? env typeName fieldName |>.get!
-      let e := Expr.app (.const  projectorName []) inner
-      self e
   -- Elides all unhygenic names
   binder_info_to_ast : Lean.BinderInfo → String
     | .default => ""
     | .implicit => " :implicit"
     | .strictImplicit => " :strictImplicit"
     | .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: Commands.Options) (e: Expr): MetaM Commands.Expression := do
   let pp := toString (← Meta.ppExpr e)
   let pp?: Option String := match options.printExprPretty with
-    | true => .some pp
+      | true => .some pp
-    | false => .none
+      | false => .none
-  let sexp: String ← serialize_expression_ast e
+  let sexp: String := (← serialize_expression_ast e)
   let sexp?: Option String := match options.printExprAST with
-    | true => .some sexp
+      | true => .some sexp
-    | false => .none
+      | false => .none
   return {
     pp?,
     sexp?
   }
 
 /-- Adapted from ppGoal -/
-def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
-      : MetaM Protocol.Goal := do
+      : MetaM Commands.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
   let ppAuxDecls     := options.printAuxDecls
@@ -181,32 +198,29 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
   let lctx           := mvarDecl.lctx
   let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
   Meta.withLCtx lctx mvarDecl.localInstances do
-    let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
+    let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do
       match localDecl with
-      | .cdecl _ fvarId userName _ _ _ =>
+      | .cdecl _ _ varName _ _ _ =>
-        let userName := userName.simpMacroScopes
+        let varName := varName.simpMacroScopes
         return {
-          name := of_name fvarId.name,
+          name := toString varName,
-          userName:= of_name userName.simpMacroScopes,
         }
-      | .ldecl _ fvarId userName _ _ _ _ => do
+      | .ldecl _ _ varName _ _ _ _ => do
         return {
-          name := of_name fvarId.name,
+          name := toString varName,
-          userName := toString userName.simpMacroScopes,
         }
-    let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
+    let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do
       match localDecl with
-      | .cdecl _ fvarId userName type _ _ =>
+      | .cdecl _ _ varName type _ _ =>
-        let userName := userName.simpMacroScopes
+        let varName := varName.simpMacroScopes
         let type ← instantiateMVars type
         return {
-          name := of_name fvarId.name,
+          name := toString varName,
-          userName:= of_name userName,
+          isInaccessible? := .some varName.isInaccessibleUserName
-          isInaccessible? := .some userName.isInaccessibleUserName
           type? := .some (← serialize_expression options type)
         }
-      | .ldecl _ fvarId userName type val _ _ => do
+      | .ldecl _ _ varName type val _ _ => do
-        let userName := userName.simpMacroScopes
+        let varName := varName.simpMacroScopes
         let type ← instantiateMVars type
         let value? ← if showLetValues then
           let val ← instantiateMVars val
@@ -214,9 +228,8 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
         else
           pure $ .none
         return {
-          name := of_name fvarId.name,
+          name := toString varName,
-          userName:= of_name userName,
+          isInaccessible? := .some varName.isInaccessibleUserName
-          isInaccessible? := .some userName.isInaccessibleUserName
           type? := .some (← serialize_expression options type)
           value? := value?
         }
@@ -226,87 +239,21 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
       if skip then
         return acc
       else
-        let nameOnly := options.noRepeat && (parentDecl?.map
+        let nameOnly := options.proofVariableDelta && (parentDecl?.map
           (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
         let var ← match nameOnly with
           | true => ppVarNameOnly localDecl
           | false => ppVar localDecl
         return var::acc
     return {
-      name := of_name goal.name,
+      caseName? := match mvarDecl.userName with
-      userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
+        | Name.anonymous => .none
-      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
+        | name => .some <| toString name,
+      isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
       target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
     }
-  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
-  state.restoreMetaM
-  let goals := state.goals.toArray
-  let parentDecl? := parent.bind (λ parentState =>
-    let parentGoal := parentState.goals.get! state.parentGoalId
-    parentState.mctx.findDecl? parentGoal)
-  goals.mapM fun goal => do
-    match state.mctx.findDecl? goal with
-    | .some mvarDecl =>
-      let serializedGoal ← serialize_goal options goal mvarDecl (parentDecl? := parentDecl?)
-      pure serializedGoal
-    | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
-/-- Print the metavariables in a readable format -/
-protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
-  goalState.restoreMetaM
-  let savedState := goalState.savedState
-  let goals := savedState.tactic.goals
-  let mctx ← getMCtx
-  let root := goalState.root
-  -- Print the root
-  match mctx.decls.find? root with
-  | .some decl => printMVar ">" root decl
-  | .none => IO.println s!">{root.name}: ??"
-  goals.forM (fun mvarId => do
-    if mvarId != root then
-      match mctx.decls.find? mvarId with
-      | .some decl => printMVar "⊢" mvarId decl
-      | .none => IO.println s!"⊢{mvarId.name}: ??"
-  )
-  let goals := goals.toSSet
-  mctx.decls.forM (fun mvarId decl => do
-    if goals.contains mvarId || mvarId == root then
-      pure ()
-    -- 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 " "
-      printMVar pref mvarId decl
-    else
-      pure ()
-      --IO.println s!" {mvarId.name}{userNameToString decl.userName}"
-  )
-  where
-    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
-      if options.printContext then
-        decl.lctx.fvarIdToDecl.forM printFVar
-      let type ← if options.instantiate
-        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
-            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
-      | .anonymous => ""
-      | other => s!"[{other}]"
 
 end Pantograph

Pantograph/Symbols.lean

@@ -0,0 +1,38 @@
+/-
+ - Manages the visibility status of symbols
+ -/
+import Lean.Declaration
+
+namespace Pantograph
+
+def str_to_name (s: String): Lean.Name :=
+  (s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous
+
+def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
+  let nameDeduce: Bool := match n.getRoot with
+  | .str _ name => name.startsWith "_" ∨ name == "Lean"
+  | _ => true
+  let stemDeduce: Bool := match n with
+  | .anonymous => true
+  | .str _ name => name.startsWith "_"
+  | .num _ _ => true
+  nameDeduce ∨ stemDeduce ∨ info.isUnsafe
+
+def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+  let pref := match info with
+  | .axiomInfo  _ => "axiom"
+  | .defnInfo   _ => "defn"
+  | .thmInfo    _ => "thm"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo   _ => "quot"
+  | .inductInfo _ => "induct"
+  | .ctorInfo   _ => "ctor"
+  | .recInfo    _ => "rec"
+  s!"{pref}|{toString n}"
+
+def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
+  if is_symbol_unsafe_or_internal n info
+  then Option.none
+  else Option.some <| to_compact_symbol_name n info
+
+end Pantograph

Pantograph/Tactic.lean

@@ -0,0 +1,102 @@
+import Lean
+
+import Pantograph.Symbols
+import Pantograph.Serial
+
+/-
+The proof state manipulation system
+
+A proof state is launched by providing
+1. Environment: `Environment`
+2. Expression: `Expr`
+The expression becomes the first meta variable in the saved tactic state
+`Elab.Tactic.SavedState`.
+From this point on, any proof which extends
+`Elab.Term.Context` and
+-/
+
+def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
+  {
+    msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
+  }
+
+
+namespace Pantograph
+open Lean
+
+structure GoalState where
+  mvarId: MVarId
+  savedState : Elab.Tactic.SavedState
+
+abbrev M := Elab.TermElabM
+
+def GoalState.create (expr: Expr): M GoalState := do
+  let expr ← instantiateMVars expr
+  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
+  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
+  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
+  return {
+    savedState := savedState,
+    mvarId := goal.mvarId!
+  }
+
+def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) :
+    M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do
+  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do
+    state.restore
+    Elab.Tactic.setGoals [goal]
+    try
+      Elab.Tactic.evalTactic stx
+      if (← getThe Core.State).messages.hasErrors then
+        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        return .error errors
+      else
+        return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals)
+    catch exception =>
+      return .error #[← exception.toMessageData.toString]
+  match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `tactic)
+    (input := tactic)
+    (fileName := "<stdin>") with
+  | Except.error err => return .error #[err]
+  | Except.ok stx    => tacticM stx { elaborator := .anonymous } |>.run' state.tactic
+
+/-- Response for executing a tactic -/
+inductive TacticResult where
+  -- Goes to next state
+  | success (goals: Array (GoalState × Commands.Goal))
+  -- Fails with messages
+  | failure (messages: Array String)
+
+namespace TacticResult
+
+def is_success: TacticResult → Bool
+  | .success _ => true
+  | .failure _ => false
+
+end TacticResult
+
+/-- Execute tactic on given state -/
+def GoalState.execute (goal: GoalState) (tactic: String):
+    Commands.OptionsT M TacticResult := do
+  let options ← read
+  match (← execute_tactic (state := goal.savedState) (goal := goal.mvarId) (tactic := tactic)) with
+  | .error errors =>
+    return .failure errors
+  | .ok (nextState, nextGoals) =>
+    if nextGoals.isEmpty then
+      return .success #[]
+    else
+      let nextGoals: List GoalState := nextGoals.map fun mvarId => { mvarId, savedState := nextState }
+      let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal.mvarId
+      let goals ← nextGoals.mapM fun nextGoal => do
+        match (← MonadMCtx.getMCtx).findDecl? nextGoal.mvarId with
+        | .some mvarDecl =>
+          let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
+          return (nextGoal, serializedGoal)
+        | .none => throwError nextGoal.mvarId
+      return .success goals.toArray
+
+end Pantograph

Pantograph/Version.lean

@@ -1,6 +1,5 @@
 namespace Pantograph
 
-@[export pantograph_version]
+def version := "0.2.5"
-def version := "0.2.13"
 
 end Pantograph

README.md

@@ -18,7 +18,6 @@ export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATH
 
 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```
-The provided `flake.nix` has a develop environment with Lean already setup.
 
 ## Usage
 
@@ -33,7 +32,7 @@ result of a command execution.  The command can be passed in one of two formats
 command { ... }
 { "cmd": command, "payload": ... }
 ```
-The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
+The list of available commands can be found in `Pantograph/Commands.lean` and below. An
 empty command aborts the REPL.
 
 The `pantograph` executable must be run with a list of modules to import. It can
@@ -42,44 +41,42 @@ also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
 Example: (~5k symbols)
 ```
 $ pantograph Init
-env.catalog
+lib.catalog
-env.inspect {"name": "Nat.le_add_left"}
+lib.inspect {"name": "Nat.le_add_left"}
 ```
 Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
 ```
 $ pantograph Mathlib.Analysis.Seminorm
-env.catalog
+lib.catalog
 ```
 Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
 ```
 $ pantograph Init
 goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
-goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
+goal.tactic {"goalId": 0, "tactic": "intro n m"}
-goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
+goal.tactic {"goalId": 1, "tactic": "assumption"}
-goal.delete {"stateIds": [0]}
+goal.delete {"goalIds": [0]}
 stat {}
-goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
+goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
 stat
 ```
 where the application of `assumption` should lead to a failure.
 
 ## Commands
 
-See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
+See `Pantograph/Commands.lean` for a description of the parameters and return values in JSON.
 - `reset`: Delete all cached expressions and proof trees
 - `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
-- `env.catalog`: Display a list of all safe Lean symbols in the current environment
+- `lib.catalog`: Display a list of all safe Lean symbols in the current context
-- `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
+- `lib.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
   given symbol; If value flag is set, the value is printed or hidden. By default
   only the values of definitions are printed.
 - `options.set { key: value, ... }`: Set one or more options (not Lean options; those
-  have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
+  have to be set via command line arguments.), for options, see `Pantograph/Commands.lean`
 - `options.print`: Display the current set of options
 - `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
-- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
+- `goal.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given goal
-- `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state
+- `goal.remove {"goalIds": [<id>]}"`: Remove a bunch of stored goals.
-- `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
-- `goal.print {"stateId": <id>}"`: Print a goal state
 - `stat`: Display resource usage
 
 ## Errors

Test/Common.lean

@@ -1,57 +0,0 @@
-import Pantograph.Goal
-import Pantograph.Library
-import Pantograph.Protocol
-import LSpec
-
-namespace Pantograph
-
-namespace Protocol
-/-- Set internal names to "" -/
-def Goal.devolatilize (goal: Goal): Goal :=
-  {
-    goal with
-    name := "",
-    vars := goal.vars.map removeInternalAux,
-  }
-  where removeInternalAux (v: Variable): Variable :=
-    {
-      v with
-      name := ""
-    }
-deriving instance DecidableEq, Repr for Expression
-deriving instance DecidableEq, Repr for Variable
-deriving instance DecidableEq, Repr for Goal
-end Protocol
-
-def TacticResult.toString : TacticResult → String
-  | .success state => s!".success ({state.goals.length} goals)"
-  | .failure messages =>
-    let messages := "\n".intercalate messages.toList
-    s!".failure {messages}"
-  | .parseError error => s!".parseError {error}"
-  | .indexError index => s!".indexError {index}"
-
-def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
-
-open Lean
-
-def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do
-  let coreContext: Core.Context ← createCoreContext #[]
-  match ← (coreM.run' coreContext { env := env }).toBaseIO with
-  | .error exception =>
-    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
-  | .ok a            => return a
-def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
-  runCoreMSeq env metaM.run'
-def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := {
-    declName? := .none,
-    errToSorry := false,
-  })
-
-def defaultTermElabMContext: Lean.Elab.Term.Context := {
-    declName? := some "_pantograph".toName,
-    errToSorry := false
-  }
-
-end Pantograph

Test/Environment.lean

@@ -1,88 +0,0 @@
-import LSpec
-import Pantograph.Serial
-import Pantograph.Environment
-import Test.Common
-
-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
-  let entries: List (Name × Bool) := [
-    ("Nat.add_comm".toName, false),
-    ("Lean.Name".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)
-    LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  return suite
-
-inductive ConstantCat where
-  | induct (info: Protocol.InductInfo)
-  | ctor (info: Protocol.ConstructorInfo)
-  | recursor (info: Protocol.RecursorInfo)
-
-def test_inspect (env: Environment): IO LSpec.TestSeq := do
-  let testCases: List (String × ConstantCat) := [
-    ("Or", ConstantCat.induct {
-      numParams := 2,
-      numIndices := 0,
-      all := #["Or"],
-      ctors := #["Or.inl", "Or.inr"],
-    }),
-    ("Except.ok", ConstantCat.ctor {
-      induct := "Except",
-      cidx := 1,
-      numParams := 2,
-      numFields := 1,
-    }),
-    ("Eq.rec", ConstantCat.recursor {
-      all := #["Eq"],
-      numParams := 2,
-      numIndices := 1,
-      numMotives := 1,
-      numMinors := 1,
-      k := true,
-    }),
-    ("ForM.rec", ConstantCat.recursor {
-      all := #["ForM"],
-      numParams := 3,
-      numIndices := 0,
-      numMotives := 1,
-      numMinors := 1,
-      k := false,
-    })
-  ]
-  let inner: CoreM LSpec.TestSeq := do
-    testCases.foldlM (λ acc (name, cat) => do
-      let args: Protocol.EnvInspect := { name := name }
-      let result ← match ← Environment.inspect args (options := {}) with
-        | .ok result => pure $ result
-        | .error e => panic! s!"Error: {e.desc}"
-      let p := match cat with
-        | .induct info => LSpec.test name (result.inductInfo? == .some info)
-        | .ctor info => LSpec.test name (result.constructorInfo? == .some info)
-        | .recursor info => LSpec.test name (result.recursorInfo? == .some info)
-      return LSpec.TestSeq.append acc p
-    ) LSpec.TestSeq.done
-  runCoreMSeq env inner
-
-def suite: IO LSpec.TestSeq := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    --(imports := #["Prelude"].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))
-
-end Pantograph.Test.Environment

Test/Holes.lean

@@ -1,209 +0,0 @@
-import LSpec
-import Pantograph.Goal
-import Pantograph.Serial
-import Test.Common
-
-namespace Pantograph.Test.Holes
-open Pantograph
-open Lean
-
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
-
-def addTest (test: LSpec.TestSeq): TestM Unit := do
-  set $ (← get) ++ test
-
-def startProof (expr: String): TestM (Option GoalState) := do
-  let env ← Lean.MonadEnv.getEnv
-  let syn? := syntax_from_str env expr
-  addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
-  match syn? with
-  | .error error =>
-    IO.println error
-    return Option.none
-  | .ok syn =>
-    let expr? ← syntax_to_expr_type syn
-    addTest $ LSpec.check s!"Elaborating" expr?.isOk
-    match expr? with
-    | .error error =>
-      IO.println error
-      return Option.none
-    | .ok expr =>
-      let goal ← GoalState.create (expr := expr)
-      return Option.some goal
-
-def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
-  {
-    userName?,
-    target := { pp? := .some target},
-    vars := (nameType.map fun x => ({
-      userName := x.fst,
-      type? := .some { pp? := .some x.snd },
-      isInaccessible? := .some false
-    })).toArray
-  }
-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 metaM := termElabM.run' (ctx := defaultTermElabMContext)
-  let coreM := metaM.run'
-  match ← (coreM.run' coreContext { env := env }).toBaseIO with
-  | .error exception =>
-    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
-  | .ok (_, a) =>
-    return a
-
-/-- M-coupled goals -/
-def test_m_couple: 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"])
-  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-  -- Set m to 3
-  let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") 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 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ 3", .some "3 ≤ 5"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-  return ()
-
-def test_proposition_generation: TestM Unit := do
-  let state? ← startProof "Σ' p:Prop, p"
-  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 PSigma.mk") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      buildGoal [] "?fst" (userName? := .some "snd"),
-      buildGoal [] "Prop" (userName? := .some "fst")
-      ])
-  if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
-    addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
-  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-
-  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
-  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
-
-  let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[])
-
-  addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
-  return ()
-
-def test_partial_continuation: 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 := "apply Nat.succ") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "apply Nat.succ" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "Nat"])
-
-  -- Execute a partial continuation
-  let coupled_goals := state1.goals ++ state2.goals
-  let state1b ← match state2.resume (goals := coupled_goals) with
-    | .error msg => do
-      addTest $ assertUnreachable $ msg
-      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"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-
-  -- Roundtrip
-  --let coupled_goals := coupled_goals.map (λ g =>
-  --  { name := str_to_name $ name_to_ast g.name (sanitize := false)})
-  let coupled_goals := coupled_goals.map (λ g => name_to_ast g.name (sanitize := false))
-  let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
-  let state1b ← match state2.resume (goals := coupled_goals) with
-    | .error msg => do
-      addTest $ assertUnreachable $ msg
-      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"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-
-  -- Continuation should fail if the state does not exist:
-  match state0.resume coupled_goals with
-  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
-  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
-  -- Continuation should fail if some goals have not been solved
-  match state2.continue state1 with
-  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals")
-  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
-  return ()
-
-
-def suite: IO LSpec.TestSeq := do
-  let env: Lean.Environment ← Lean.importModules
-    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
-    (opts := {})
-    (trustLevel := 1)
-  let tests := [
-    ("2 < 5", test_m_couple),
-    ("Proposition Generation", test_proposition_generation),
-    ("Partial Continuation", test_partial_continuation)
-  ]
-  let tests ← tests.foldlM (fun acc tests => do
-    let (name, tests) := tests
-    let tests ← proofRunner env tests
-    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
-
-  return LSpec.group "Holes" tests
-
-end Pantograph.Test.Holes

Test/Integration.lean

@@ -2,7 +2,7 @@
  -/
 import LSpec
 import Pantograph
-namespace Pantograph.Test.Integration
+namespace Pantograph.Test
 open Pantograph
 
 def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
@@ -21,41 +21,52 @@ 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
       return suite ++ result) LSpec.TestSeq.done
   try
-    let coreM := commands.run context |>.run' {}
+    let termElabM := commands.run context |>.run' {}
+    let metaM := termElabM.run' (ctx := {
+      declName? := some "_pantograph",
+      errToSorry := false
+    })
+    let coreM := metaM.run'
     return Prod.fst $ (← coreM.toIO coreContext { env := env })
   catch ex =>
     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 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 := {}
+  let options: Commands.Options := {}
   subroutine_runner [
-    subroutine_step "env.inspect"
+    subroutine_step "lib.inspect"
       [("name", .str "Nat.add_one")]
      (Lean.toJson ({
        type := { pp? }, module? }:
-      Protocol.EnvInspectResult)),
+      Commands.LibInspectResult)),
     subroutine_step "options.set"
       [("printExprAST", .bool true)]
      (Lean.toJson ({ }:
-      Protocol.OptionsSetResult)),
+      Commands.OptionsSetResult)),
-    subroutine_step "env.inspect"
+    subroutine_step "lib.inspect"
       [("name", .str "Nat.add_one")]
      (Lean.toJson ({
        type := { pp?, sexp? }, module? }:
-      Protocol.EnvInspectResult)),
+      Commands.LibInspectResult)),
     subroutine_step "options.print"
       []
      (Lean.toJson ({ options with printExprAST := true }:
-      Protocol.OptionsPrintResult))
+      Commands.OptionsPrintResult))
   ]
 def test_malformed_command : IO LSpec.TestSeq :=
   let invalid := "invalid"
@@ -64,91 +75,19 @@ def test_malformed_command : IO LSpec.TestSeq :=
       [("name", .str "Nat.add_one")]
      (Lean.toJson ({
        error := "command", desc := s!"Unknown command {invalid}"}:
-      Protocol.InteractionError)),
+      Commands.InteractionError)),
     subroutine_named_step "JSON Deserialization" "expr.echo"
       [(invalid, .str "Random garbage data")]
      (Lean.toJson ({
-       error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
+       error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}:
-      Protocol.InteractionError))
+      Commands.InteractionError))
-  ]
-def test_tactic : IO LSpec.TestSeq :=
-  let goal1: Protocol.Goal := {
-    name := "_uniq.10",
-    target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
-  }
-  let goal2: Protocol.Goal := {
-    name := "_uniq.13",
-    target := { pp? := .some "x ∨ y → y ∨ x" },
-    vars := #[
-      { name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
-    ],
-  }
-  subroutine_runner [
-    subroutine_step "goal.start"
-      [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
-     (Lean.toJson ({stateId := 0, root := "_uniq.8"}:
-      Protocol.GoalStartResult)),
-    subroutine_step "goal.tactic"
-      [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
-     (Lean.toJson ({
-       nextStateId? := .some 1,
-       goals? := #[goal1],
-     }:
-      Protocol.GoalTacticResult)),
-    subroutine_step "goal.tactic"
-      [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
-     (Lean.toJson ({
-       nextStateId? := .some 2,
-       goals? := #[goal2],
-     }:
-      Protocol.GoalTacticResult))
   ]
 
-def test_env : IO LSpec.TestSeq :=
+def test_integration: IO LSpec.TestSeq := do
-  let name1 := "Pantograph.mystery"
-  let name2 := "Pantograph.mystery2"
-  subroutine_runner [
-    subroutine_step "env.add"
-      [
-        ("name", .str name1),
-        ("type", .str "Prop → Prop → Prop"),
-        ("value", .str "λ (a b: Prop) => Or a b"),
-        ("isTheorem", .bool false)
-      ]
-     (Lean.toJson ({}: Protocol.EnvAddResult)),
-    subroutine_step "env.inspect"
-      [("name", .str name1)]
-     (Lean.toJson ({
-       value? := .some { pp? := .some "fun a b => a ∨ b" },
-       type := { pp? := .some "Prop → Prop → Prop" },
-     }:
-      Protocol.EnvInspectResult)),
-    subroutine_step "env.add"
-      [
-        ("name", .str name2),
-        ("type", .str "Nat → Int"),
-        ("value", .str "λ (a: Nat) => a + 1"),
-        ("isTheorem", .bool false)
-      ]
-     (Lean.toJson ({}: Protocol.EnvAddResult)),
-    subroutine_step "env.inspect"
-      [("name", .str name2)]
-     (Lean.toJson ({
-       value? := .some { pp? := .some "fun a => ↑a + 1" },
-       type := { pp? := .some "Nat → Int" },
-     }:
-      Protocol.EnvInspectResult))
-  ]
-
-def suite: IO LSpec.TestSeq := do
 
   return LSpec.group "Integration" $
     (LSpec.group "Option modify" (← test_option_modify)) ++
-    (LSpec.group "Malformed command" (← test_malformed_command)) ++
+    (LSpec.group "Malformed command" (← test_malformed_command))
-    (LSpec.group "Tactic" (← test_tactic)) ++
-    (LSpec.group "Env" (← test_env))
 
 
-end Pantograph.Test.Integration
+end Pantograph.Test

Test/Main.lean

@@ -1,21 +1,18 @@
 import LSpec
-import Test.Environment
-import Test.Holes
 import Test.Integration
 import Test.Proofs
 import Test.Serial
 
 open Pantograph.Test
 
-def main := do
+unsafe def main := do
+  Lean.enableInitializersExecution
   Lean.initSearchPath (← Lean.findSysroot)
 
   let suites := [
-    Holes.suite,
+    test_integration,
-    Integration.suite,
+    test_proofs,
-    Proofs.suite,
+    test_serial
-    Serial.suite,
-    Environment.suite
   ]
   let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
   LSpec.lspecIO $ all

Test/Proofs.lean

@@ -1,12 +1,8 @@
-/-
-Tests pertaining to goals with no interdependencies
--/
 import LSpec
-import Pantograph.Goal
+import Pantograph.Tactic
 import Pantograph.Serial
-import Test.Common
 
-namespace Pantograph.Test.Proofs
+namespace Pantograph.Test
 open Pantograph
 open Lean
 
@@ -14,17 +10,21 @@ inductive Start where
   | copy (name: String) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M)
 
-def addTest (test: LSpec.TestSeq): TestM Unit := do
+deriving instance DecidableEq, Repr for Commands.Expression
+deriving instance DecidableEq, Repr for Commands.Variable
+deriving instance DecidableEq, Repr for Commands.Goal
+
+def add_test (test: LSpec.TestSeq): TestM Unit := do
   set $ (← get) ++ test
 
-def startProof (start: Start): TestM (Option GoalState) := do
+def start_proof (start: Start): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
   match start with
   | .copy name =>
-    let cInfo? := name.toName |> env.find?
+    let cInfo? := str_to_name name |> env.find?
-    addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
+    add_test $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
     match cInfo? with
     | .some cInfo =>
       let goal ← GoalState.create (expr := cInfo.type)
@@ -33,14 +33,14 @@ def startProof (start: Start): TestM (Option GoalState) := do
       return Option.none
   | .expr expr =>
     let syn? := syntax_from_str env expr
-    addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
+    add_test $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
     match syn? with
     | .error error =>
       IO.println error
       return Option.none
     | .ok syn =>
-      let expr? ← syntax_to_expr_type syn
+      let expr? ← syntax_to_expr syn
-      addTest $ LSpec.check s!"Elaborating" expr?.isOk
+      add_test $ LSpec.check s!"Elaborating" expr?.isOk
       match expr? with
       | .error error =>
         IO.println error
@@ -49,136 +49,72 @@ def startProof (start: Start): TestM (Option GoalState) := do
         let goal ← GoalState.create (expr := expr)
         return Option.some goal
 
-def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
+def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false
+
+def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
   {
-    userName?,
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
-      userName := x.fst,
+      name := x.fst,
       type? := .some { pp? := .some x.snd },
       isInaccessible? := .some false
     })).toArray
   }
-def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
+-- Like `build_goal` but allow certain variables to be elided.
-  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
+def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
+  {
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      name := x.fst,
+      type? := x.snd.map (λ type => { pp? := type }),
+      isInaccessible? := x.snd.map (λ _ => false)
+    })).toArray
+  }
 
-  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 =>
-    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
-  | .ok (_, a) =>
-    return a
 
 -- Individual test cases
 example: ∀ (a b: Nat), a + b = b + a := by
   intro n m
   rw [Nat.add_comm]
-def proof_nat_add_comm (manual: Bool): TestM Unit := do
+def proof_nat_add_comm: TestM Unit := do
-  let state? ← startProof <| match manual with
+  let goal? ← start_proof (.copy "Nat.add_comm")
-    | false => .copy "Nat.add_comm"
+  add_test $ LSpec.check "Start goal" goal?.isSome
-    | true => .expr "∀ (a b: Nat), a + b = b + a"
+  if let .some goal := goal? then
-  addTest $ LSpec.check "Start goal" state?.isSome
+    if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then
-  let state0 ← match state? with
+      let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
-    | .some state => pure state
+      add_test $ LSpec.check "intro n m" (sGoal = sGoal1e)
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with
+      if let .failure #[message] ← goal.execute "assumption" then
-    | .success state => pure state
+        add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
-    | other => do
+      else
-      addTest $ assertUnreachable $ other.toString
+        add_test $ assert_unreachable "assumption"
-      return ()
-  addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
 
-  match ← state1.execute (goalId := 0) (tactic := "assumption") with
+      if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
-  | .failure #[message] =>
+        return ()
-    addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
+      else
-  | other => do
+        add_test $ assert_unreachable "rw [Nat.add_comm]"
-    addTest $ assertUnreachable $ other.toString
+    else
+      add_test $ assert_unreachable "intro n m"
+def proof_nat_add_comm_manual: TestM Unit := do
+  let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a")
+  add_test $ LSpec.check "Start goal" goal?.isSome
+  if let .some goal := goal? then
+    if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then
+      let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
+      add_test $ LSpec.check "intro n m" (sGoal = sGoal1e)
 
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with
+      if let .failure #[message] ← goal.execute "assumption" then
-    | .success state => pure state
+        add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
-    | other => do
+      else
-      addTest $ assertUnreachable $ other.toString
+        add_test $ assert_unreachable "assumption"
-      return ()
-  addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
 
-  return ()
+      if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
-def proof_delta_variable: TestM Unit := do
+        return ()
-  let options: Protocol.Options := { noRepeat := true }
+      else
-  let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
+        add_test $ assert_unreachable "rw [Nat.add_comm]"
-  addTest $ LSpec.check "Start goal" state?.isSome
+    else
-  let state0 ← match state? with
+      add_test $ assert_unreachable "intro n m"
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
-    #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "intro m") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
-    #[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
-  return ()
-  where
--- Like `buildGoal` but allow certain variables to be elided.
-  buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
-    {
-      target := { pp? := .some target},
-      vars := (nameType.map fun x => ({
-        userName := x.fst,
-        type? := x.snd.map (λ type => { pp? := type }),
-        isInaccessible? := x.snd.map (λ _ => false)
-      })).toArray
-    }
-
-example (w x y z : Nat) (p : Nat → Prop)
-        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
-  simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
-  assumption
-def proof_arith: TestM Unit := do
-  let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
-  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 := "intros") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "intros" (state1.goals.length = 1)
-  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
-  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
-  let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.test "assumption" state3.goals.isEmpty
-  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
-  return ()
 
 -- Two ways to write the same theorem
 example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
@@ -196,121 +132,121 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
   . apply Or.inl
     assumption
 def proof_or_comm: TestM Unit := do
-  let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
+  let typeProp: Commands.Expression := { pp? := .some "Prop" }
-  let state0 ← match state? with
+  let branchGoal (caseName name: String): Commands.Goal := {
-    | .some state => pure state
+    caseName? := .some caseName,
-    | .none => do
+    target := { pp? := .some "q ∨ p" },
-      addTest $ assertUnreachable "Goal could not parse"
+    vars := #[
-      return ()
+      { name := "p", type? := .some typeProp, isInaccessible? := .some false },
-  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
+      { name := "q", type? := .some typeProp, isInaccessible? := .some false },
-  addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
+      { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
+    ]
+  }
+  let goal? ← start_proof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
+  add_test $ LSpec.check "Start goal" goal?.isSome
+  if let .some goal := goal? then
+    if let .success #[(goal, sGoal)] ← goal.execute "intro p q h" then
+      let sGoal1e := build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"
+      add_test $ LSpec.check "intro p q h" (sGoal = sGoal1e)
 
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
+      if let .success #[(goal1, sGoal1), (goal2, sGoal2)] ← goal.execute "cases h" then
-    | .success state => pure state
+        add_test $ LSpec.check "cases h/1" (sGoal1 = branchGoal "inl" "p")
-    | other => do
+        if let .success #[(goal, _)] ← goal1.execute "apply Or.inr" then
-      addTest $ assertUnreachable $ other.toString
+          if let .success #[] ← goal.execute "assumption" then
-      return ()
+            return ()
-  addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+          else
-    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
+            add_test $ assert_unreachable "assumption"
-  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
+        else
-  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
+          add_test $ assert_unreachable "apply Or.inr"
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      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
-    | other => 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
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
-  let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
-  addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
-  -- Ensure the proof can continue from `state4_2`.
-  let state2b ← match state4_2.continue state2 with
-    | .error msg => do
-      addTest $ assertUnreachable $ msg
-      return ()
-    | .ok state => pure state
-  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
-  let state3_1 ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  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
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
-
-  return ()
-  where
-    typeProp: Protocol.Expression := { pp? := .some "Prop" }
-    branchGoal (caseName varName: String): Protocol.Goal := {
-      userName? := .some caseName,
-      target := { pp? := .some "q ∨ p" },
-      vars := #[
-        { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
-        { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
-        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
-      ]
-    }
 
 
-def suite: IO LSpec.TestSeq := do
+        add_test $ LSpec.check "cases h/2" (sGoal2 = branchGoal "inr" "q")
+        if let .success #[(goal, _)] ← goal2.execute "apply Or.inl" then
+          if let .success #[] ← goal.execute "assumption" then
+            return ()
+          else
+            add_test $ assert_unreachable "assumption"
+        else
+          add_test $ assert_unreachable "apply Or.inl"
+
+      else
+        add_test $ assert_unreachable "cases h"
+    else
+      add_test $ assert_unreachable "intro p q h"
+
+example (w x y z : Nat) (p : Nat → Prop)
+        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
+  simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
+  assumption
+def proof_arith_1: TestM Unit := do
+  let goal? ← start_proof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
+  add_test $ LSpec.check "Start goal" goal?.isSome
+  if let .some goal := goal? then
+    if let .success #[(goal, _)] ← goal.execute "intros" then
+      if let .success #[(goal, _)] ← goal.execute "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *" then
+        if let .success #[] ← goal.execute "assumption" then
+          return ()
+        else
+          add_test $ assert_unreachable "assumption"
+      else
+        add_test $ assert_unreachable "simp ..."
+    else
+      add_test $ assert_unreachable "intros"
+
+def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do
+  let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a")
+  add_test $ LSpec.check "Start goal" goal?.isSome
+  if let .some goal := goal? then
+    if let .success #[(goal, sGoal)] ← goal.execute "intro n" then
+      let sGoal1e: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"
+      add_test $ LSpec.check "intro n" (sGoal = sGoal1e)
+
+      if let .success #[(_, sGoal)] ← goal.execute "intro m" then
+        let sGoal2e: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n"
+        add_test $ LSpec.check "intro m" (sGoal = sGoal2e)
+      else
+        add_test $ assert_unreachable "intro m"
+    else
+      add_test $ assert_unreachable "intro n"
+
+def proof_runner (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 := str_to_name "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 =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok (_, a) =>
+    return a
+
+def test_proofs : IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
-    (imports := #[{ module := "Init".toName, runtimeOnly := false}])
+    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
   let tests := [
-    ("Nat.add_comm", proof_nat_add_comm false),
+    ("Nat.add_comm", proof_nat_add_comm),
-    ("Nat.add_comm manual", proof_nat_add_comm true),
+    ("nat.add_comm manual", proof_nat_add_comm_manual),
-    ("Nat.add_comm delta", proof_delta_variable),
+    ("Or.comm", proof_or_comm),
-    ("arithmetic", proof_arith),
+    ("arithmetic 1", proof_arith_1),
-    ("Or.comm", proof_or_comm)
+    ("delta variable", proof_delta_variable)
   ]
   let tests ← tests.foldlM (fun acc tests => do
     let (name, tests) := tests
-    let tests ← proofRunner env tests
+    let tests ← proof_runner env tests
     return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
 
   return LSpec.group "Proofs" tests
 
-end Pantograph.Test.Proofs
+end Pantograph.Test
+

Test/Serial.lean

@@ -1,87 +1,76 @@
 import LSpec
 import Pantograph.Serial
-import Test.Common
+import Pantograph.Symbols
 
-namespace Pantograph.Test.Serial
+namespace Pantograph.Test
 
 open Pantograph
 open Lean
 
-deriving instance Repr, DecidableEq for Protocol.BoundExpression
+deriving instance Repr, DecidableEq for Commands.BoundExpression
 
-def test_name_to_ast: LSpec.TestSeq :=
+def test_str_to_name: LSpec.TestSeq :=
-  let quote := "\""
+    LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
-  let escape := "\\"
-  LSpec.test "a.b.1" (name_to_ast (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
-  LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
-  -- Pathological test case
-  LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
 
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
-  let entries: List (Name × Protocol.BoundExpression) := [
+  let entries: List (String × Commands.BoundExpression) := [
-    ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
+    ("Nat.add_comm", { 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", { 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 coreM := entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
-    let expr := env.find? symbol |>.get! |>.type
+    let expr := str_to_name symbol |> env.find? |>.get! |>.type
-    let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
+    let test := LSpec.check symbol ((← type_expr_to_bound expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
-  runCoreMSeq env coreM
+  let coreContext: Core.Context := {
+    currNamespace := Lean.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}" = "")
+  | .ok a            => return a
 
 def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
     -- This one contains unhygienic variable names which must be suppressed
-    ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
+    ("Nat.add", "(:forall :anon (:c Nat) (:forall :anon (:c Nat) (:c Nat)))"),
     -- These ones are normal and easy
-    ("Nat.add_one", "(: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)))"),
+    ("Nat.add_one", "(: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)))"),
-    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
+    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h (((((:c LE.le) (:c Nat)) (:c instLENat)) ((:c Nat.succ) 1)) 0) (((((:c LE.le) (:c Nat)) (:c instLENat)) 2) 1)) :implicit) :implicit)"),
     -- Handling of higher order types
     ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
     ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
   ]
   let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
-    let expr := env.find? symbol.toName |>.get! |>.type
+    let expr := str_to_name symbol |> env.find? |>.get! |>.type
     let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
-    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
-  runMetaMSeq env metaM
+  let coreM := metaM.run'
+  let coreContext: Core.Context := {
+    currNamespace := Lean.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}" = "")
+  | .ok a            => return a
 
-def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
-  let entries: List (String × String) := [
-    ("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
-    ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))")
-  ]
-  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
-    let env ← MonadEnv.getEnv
-    let s := syntax_from_str env source |>.toOption |>.get!
-    let expr := (← syntax_to_expr s) |>.toOption |>.get!
-    let test := LSpec.check source ((← serialize_expression_ast expr) = target)
-    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
-  runMetaMSeq env metaM
 
--- Instance parsing
+def test_serial: IO LSpec.TestSeq := do
-def test_instance (env: Environment): IO LSpec.TestSeq := do
-  let metaM: MetaM LSpec.TestSeq := do
-    let env ← MonadEnv.getEnv
-    let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
-    let s := syntax_from_str env source |>.toOption |>.get!
-    let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
-    return LSpec.TestSeq.done
-  runMetaMSeq env metaM
-
-def suite: IO LSpec.TestSeq := do
   let env: Environment ← importModules
-    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
+    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
 
-  return LSpec.group "Serialization" $
+  return LSpec.group "Serialisation" $
-    (LSpec.group "name_to_ast" test_name_to_ast) ++
+    (LSpec.group "str_to_name" test_str_to_name) ++
     (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
-    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) ++
+    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))
-    (LSpec.group "Sexp from expr" (← test_sexp_of_expr env)) ++
-    (LSpec.group "Instance" (← test_instance env))
 
-end Pantograph.Test.Serial
+end Pantograph.Test

flake.lock

@@ -1,220 +0,0 @@
-{
-  "nodes": {
-    "flake-parts": {
-      "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib"
-      },
-      "locked": {
-        "lastModified": 1696343447,
-        "narHash": "sha256-B2xAZKLkkeRFG5XcHHSXXcP7To9Xzr59KXeZiRf4vdQ=",
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "rev": "c9afaba3dfa4085dbd2ccb38dfade5141e33d9d4",
-        "type": "github"
-      },
-      "original": {
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "type": "github"
-      }
-    },
-    "flake-utils": {
-      "locked": {
-        "lastModified": 1656928814,
-        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
-        "type": "github"
-      },
-      "original": {
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "type": "github"
-      }
-    },
-    "lean": {
-      "inputs": {
-        "flake-utils": "flake-utils",
-        "lean4-mode": "lean4-mode",
-        "nix": "nix",
-        "nixpkgs": "nixpkgs_2",
-        "nixpkgs-old": "nixpkgs-old"
-      },
-      "locked": {
-        "lastModified": 1711508550,
-        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
-        "owner": "leanprover",
-        "repo": "lean4",
-        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
-        "type": "github"
-      },
-      "original": {
-        "owner": "leanprover",
-        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
-        "repo": "lean4",
-        "type": "github"
-      }
-    },
-    "lean4-mode": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1676498134,
-        "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
-        "type": "github"
-      },
-      "original": {
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "type": "github"
-      }
-    },
-    "lowdown-src": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1633514407,
-        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
-        "owner": "kristapsdz",
-        "repo": "lowdown",
-        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
-        "type": "github"
-      },
-      "original": {
-        "owner": "kristapsdz",
-        "repo": "lowdown",
-        "type": "github"
-      }
-    },
-    "nix": {
-      "inputs": {
-        "lowdown-src": "lowdown-src",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-regression": "nixpkgs-regression"
-      },
-      "locked": {
-        "lastModified": 1657097207,
-        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
-        "owner": "NixOS",
-        "repo": "nix",
-        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nix",
-        "type": "github"
-      }
-    },
-    "nixpkgs": {
-      "locked": {
-        "lastModified": 1653988320,
-        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-22.05-small",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs-lib": {
-      "locked": {
-        "dir": "lib",
-        "lastModified": 1696019113,
-        "narHash": "sha256-X3+DKYWJm93DRSdC5M6K5hLqzSya9BjibtBsuARoPco=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "f5892ddac112a1e9b3612c39af1b72987ee5783a",
-        "type": "github"
-      },
-      "original": {
-        "dir": "lib",
-        "owner": "NixOS",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "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,
-        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      }
-    },
-    "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=",
-        "owner": "nixos",
-        "repo": "nixpkgs",
-        "rev": "ca012a02bf8327be9e488546faecae5e05d7d749",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nixos",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "root": {
-      "inputs": {
-        "flake-parts": "flake-parts",
-        "lean": "lean",
-        "nixpkgs": "nixpkgs_3"
-      }
-    }
-  },
-  "root": "root",
-  "version": 7
-}

flake.nix

@@ -1,47 +0,0 @@
-{
-  description = "Pantograph";
-
-  inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
-    flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
-  };
-
-  outputs = inputs @ {
-    self,
-    nixpkgs,
-    flake-parts,
-    lean,
-    ...
-  } : flake-parts.lib.mkFlake { inherit inputs; } {
-    flake = {
-    };
-    systems = [
-      "x86_64-linux"
-      "x86_64-darwin"
-    ];
-    perSystem = { system, pkgs, ... }: let
-      leanPkgs = lean.packages.${system};
-      project = leanPkgs.buildLeanPackage {
-        name = "Pantograph";
-        roots = [ "Main" "Pantograph" ];
-        src = ./.;
-      };
-      test = leanPkgs.buildLeanPackage {
-        name = "Test";
-        roots = [ "Main" ];
-        src = ./Test;
-      };
-    in rec {
-      packages = {
-        inherit (leanPkgs) lean lean-all;
-        inherit (project) sharedLib executable;
-        default = project.executable;
-      };
-      checks = {
-        test = test.executable;
-      };
-      devShells.default = project.devShell;
-    };
-  };
-}

lake-manifest.json

@@ -1,14 +1,11 @@
-{"version": 7,
+{"version": 5,
- "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",
- "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