From 075bec6da23ee2b4545e0b2865b7a134d64940d0 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 6 Mar 2024 15:26:35 -0800
Subject: [PATCH 01/16] feat: Output shared library in flake

---
 flake.nix | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/flake.nix b/flake.nix
index 7610209..9f586f6 100644
--- a/flake.nix
+++ b/flake.nix
@@ -28,9 +28,10 @@
         src = ./.;
       };
     in rec {
-      packages = project // {
-        inherit leanPkgs;
-        default = packages.executable;
+      packages = {
+        inherit (leanPkgs) lean lean-all;
+        inherit (project) sharedLib executable;
+        default = project.executable;
       };
       devShells.default = project.devShell;
     };
-- 
2.44.1


From ecacf2107c5c56f94810c4f1eeedf6ac8bb153ec Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 6 Mar 2024 15:27:22 -0800
Subject: [PATCH 02/16] feat(build): Add shared facet for lean_lib

---
 lakefile.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lakefile.lean b/lakefile.lean
index f0832e2..89ad70f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,6 +4,7 @@ open Lake DSL
 package pantograph
 
 lean_lib Pantograph {
+  defaultFacets := #[LeanLib.sharedFacet]
 }
 
 @[default_target]
-- 
2.44.1


From 021d0b5b7d10b821abb0e07f1341caa9bca8b405 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 8 Mar 2024 23:50:44 -0800
Subject: [PATCH 03/16] feat: Add exported version function

---
 Pantograph.lean         | 1 +
 Pantograph/Library.lean | 8 ++++++++
 2 files changed, 9 insertions(+)
 create mode 100644 Pantograph/Library.lean

diff --git a/Pantograph.lean b/Pantograph.lean
index 46729fc..90ce2d2 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -2,6 +2,7 @@ import Pantograph.Goal
 import Pantograph.Protocol
 import Pantograph.Serial
 import Pantograph.Environment
+import Pantograph.Library
 import Lean.Data.HashMap
 
 namespace Pantograph
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
new file mode 100644
index 0000000..330d84d
--- /dev/null
+++ b/Pantograph/Library.lean
@@ -0,0 +1,8 @@
+import Pantograph.Version
+
+namespace Pantograph
+
+@[export pantograph_version]
+def pantograph_version: String := version
+
+end Pantograph
-- 
2.44.1


From 863c6d9e7d8342f833a05091758ffb30c2f7bc8f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 9 Mar 2024 16:50:36 -0800
Subject: [PATCH 04/16] feat(lib): Catalog command FFI

---
 Main.lean                   | 53 +++---------------------------
 Pantograph.lean             |  3 +-
 Pantograph/Environment.lean |  4 +--
 Pantograph/Library.lean     | 64 ++++++++++++++++++++++++++++++++++++-
 4 files changed, 72 insertions(+), 52 deletions(-)

diff --git a/Main.lean b/Main.lean
index 68d1a3e..7c36db2 100644
--- a/Main.lean
+++ b/Main.lean
@@ -2,6 +2,7 @@ import Lean.Data.Json
 import Lean.Environment
 
 import Pantograph.Version
+import Pantograph.Library
 import Pantograph
 
 -- Main IO functions
@@ -39,35 +40,6 @@ partial def loop : MainM Unit := do
     IO.println str
   loop
 
-namespace Lean
-
-/-- This is better than the default version since it handles `.` and doesn't
- crash the program when it fails. -/
-def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
-  let ps := (entry.splitOn "=").map String.trim
-  let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
-  let key := key.toName
-  let defValue ← getOptionDefaultValue key
-  match defValue with
-  | DataValue.ofString _ => pure $ opts.setString key val
-  | DataValue.ofBool _   =>
-    match val with
-    | "true" => pure $ opts.setBool key true
-    | "false" => pure $ opts.setBool key false
-    | _ => throw  s!"invalid Bool option value '{val}'"
-  | DataValue.ofName _   => pure $ opts.setName key val.toName
-  | DataValue.ofNat _    =>
-    match val.toNat? with
-    | none   => throw s!"invalid Nat option value '{val}'"
-    | some v => pure $ opts.setNat key v
-  | DataValue.ofInt _    =>
-    match val.toInt? with
-    | none   => throw s!"invalid Int option value '{val}'"
-    | some v => pure $ opts.setInt key v
-  | DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
-
-end Lean
-
 
 unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
@@ -79,32 +51,17 @@ unsafe def main (args: List String): IO Unit := do
   Lean.enableInitializersExecution
   Lean.initSearchPath (← Lean.findSysroot)
 
-  let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
-    |>.foldlM Lean.setOptionFromString' Lean.Options.empty
-    |>.run
-  let options ← match options? with
-    | .ok options => pure options
-    | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
+  let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+    |>.toArray |> createCoreContext
   let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
-
-  let env ← Lean.importModules
-    (imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false }))
-    (opts := {})
-    (trustLevel := 1)
+  let coreState ← createCoreState imports.toArray
   let context: Context := {
     imports
   }
-  let coreContext: Lean.Core.Context := {
-    currNamespace := Lean.Name.str .anonymous "Aniva"
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph>",
-    fileMap := { source := "", positions := #[0], lines := #[1] },
-    options := options
-  }
   try
     let coreM := loop.run context |>.run' {}
     IO.println "ready."
-    discard <| coreM.toIO coreContext { env := env }
+    discard <| coreM.toIO coreContext coreState
   catch ex =>
     IO.println "Uncaught IO exception"
     IO.println ex.toString
diff --git a/Pantograph.lean b/Pantograph.lean
index 90ce2d2..f1f194c 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -71,7 +71,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let nGoals := state.goalStates.size
     return .ok { nGoals }
   env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
-    Environment.catalog args
+    let result ← Environment.catalog args
+    return .ok result
   env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
     let state ← get
     Environment.inspect args state.options
diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index b823e8f..df0bc7f 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -30,13 +30,13 @@ 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.CR Protocol.EnvCatalogResult) := do
+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 .ok { symbols := names }
+  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
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 330d84d..5b5e954 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -1,8 +1,70 @@
 import Pantograph.Version
+import Pantograph.Environment
+import Pantograph.Protocol
+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
 
 @[export pantograph_version]
-def pantograph_version: String := version
+def pantographVersion: String := version
+
+/-- 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], lines := #[1] },
+    options := options
+  }
+
+@[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_catalog]
+def catalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do
+  let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog)
+  let (result, _) ← coreM.toIO cc cs
+  return result
 
 end Pantograph
-- 
2.44.1


From 4706df22179a73c25af3ba9cb65ec4e3ee96b177 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 9 Mar 2024 19:36:25 -0800
Subject: [PATCH 05/16] feat(lib): Search path function

---
 Main.lean               | 3 +--
 Pantograph/Library.lean | 6 ++++++
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/Main.lean b/Main.lean
index 7c36db2..de73033 100644
--- a/Main.lean
+++ b/Main.lean
@@ -48,8 +48,7 @@ unsafe def main (args: List String): IO Unit := do
     println! s!"{version}"
     return
 
-  Lean.enableInitializersExecution
-  Lean.initSearchPath (← Lean.findSysroot)
+  initSearch ""
 
   let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
     |>.toArray |> createCoreContext
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 5b5e954..07e4656 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -38,6 +38,12 @@ namespace Pantograph
 @[export pantograph_version]
 def pantographVersion: String := version
 
+/-- 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
-- 
2.44.1


From ca89d671cc1b83acff63247b688eb92acb7c7398 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 9 Mar 2024 20:33:36 -0800
Subject: [PATCH 06/16] refactor: Move some functions to `Library.lean`

---
 Pantograph.lean          | 28 +-------------------
 Pantograph/Library.lean  | 57 +++++++++++++++++++++++++++++++++++++---
 Pantograph/Protocol.lean |  2 +-
 Pantograph/Serial.lean   |  2 +-
 4 files changed, 57 insertions(+), 32 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index f1f194c..f9b5dc5 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -22,14 +22,6 @@ abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
 -- certain monadic features in `MainM`
 abbrev CR α := Except Protocol.InteractionError α
 
-def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
-  metaM.run'
-def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
-  termElabM.run' (ctx := {
-    declName? := .none,
-    errToSorry := false,
-  }) |>.run'
-
 def execute (command: Protocol.Command): MainM Lean.Json := do
   let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
     match Lean.fromJson? command.payload with
@@ -57,9 +49,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       errorCommand s!"Unknown command {cmd}"
     return Lean.toJson error
   where
-  errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
-  errorCommand := errorI "command"
-  errorIndex := errorI "index"
   -- Command Functions
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -80,22 +69,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
-    let env ← Lean.MonadEnv.getEnv
-    let syn ← match syntax_from_str env args.expr with
-      | .error str => return .error $ errorI "parsing" str
-      | .ok syn => pure syn
-    runTermElabM (do
-      match ← syntax_to_expr syn with
-      | .error str => return .error $ errorI "elab" str
-      | .ok expr => do
-        try
-          let type ← Lean.Meta.inferType expr
-          return .ok {
-              type := (← serialize_expression (options := state.options) type),
-              expr := (← serialize_expression (options := state.options) expr)
-          }
-        catch exception =>
-          return .error $ errorI "typing" (← exception.toMessageData.toString))
+    exprEcho args state.options
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 07e4656..cdc112f 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -3,7 +3,6 @@ import Pantograph.Environment
 import Pantograph.Protocol
 import Lean
 
-
 namespace Lean
 
 /-- This is better than the default version since it handles `.` and doesn't
@@ -35,6 +34,18 @@ 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 }
+def errorCommand := errorI "command"
+def errorIndex := errorI "index"
+
 @[export pantograph_version]
 def pantographVersion: String := version
 
@@ -67,10 +78,50 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
     (trustLevel := 1)
   return { env := env }
 
-@[export pantograph_catalog]
-def catalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do
+@[export pantograph_env_catalog]
+def envCatalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do
   let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog)
   let (result, _) ← coreM.toIO cc cs
   return result
 
+@[export pantograph_env_inspect]
+def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State)
+    (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): IO (Protocol.CR Protocol.EnvInspectResult) := do
+  let coreM: Lean.CoreM _ := Environment.inspect ({
+    name, value? := .some value, dependency?:= .some dependency
+  }: Protocol.EnvInspect) options
+  let (result, _) ← coreM.toIO cc cs
+  return result
+
+@[export pantograph_env_add]
+def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State)
+  (name: String) (type: String) (value: String) (isTheorem: Bool): IO (Protocol.CR Protocol.EnvAddResult) := do
+  let coreM: Lean.CoreM _ := Environment.addDecl { name, type, value, isTheorem }
+  let (result, _) ← coreM.toIO cc cs
+  return result
+
+def exprEcho (args: Protocol.ExprEcho) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
+    let env ← Lean.MonadEnv.getEnv
+    let syn ← match syntax_from_str env args.expr with
+      | .error str => return .error $ errorI "parsing" str
+      | .ok syn => pure syn
+    runTermElabM (do
+      match ← syntax_to_expr syn with
+      | .error str => return .error $ errorI "elab" str
+      | .ok expr => do
+        try
+          let type ← Lean.Meta.inferType expr
+          return .ok {
+              type := (← serialize_expression options type),
+              expr := (← serialize_expression options expr)
+          }
+        catch exception =>
+          return .error $ errorI "typing" (← exception.toMessageData.toString))
+
+@[export pantograph_expr_echo]
+def exprEchoExport (cc: Lean.Core.Context) (cs: Lean.Core.State) (expr: String) (options: @&Protocol.Options): IO (Protocol.CR Protocol.ExprEchoResult) := do
+  let coreM: Lean.CoreM _ := exprEcho { expr } options
+  let (result, _) ← coreM.toIO cc cs
+  return result
+
 end Pantograph
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 84e0cc2..5015ad1 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -163,7 +163,7 @@ structure EnvAdd where
   name: String
   type: String
   value: String
-  isTheorem?: Bool
+  isTheorem: Bool
   deriving Lean.FromJson
 structure EnvAddResult where
   deriving Lean.ToJson
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 38d1f14..547b3dc 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -157,7 +157,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
     | .instImplicit => " :instImplicit"
   of_name (name: Name) := name_to_ast name sanitize
 
-def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
+def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
   let pp := toString (← Meta.ppExpr e)
   let pp?: Option String := match options.printExprPretty with
     | true => .some pp
-- 
2.44.1


From d958dbed9dd6bc3210b34170b87eec4969059bfa Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 10 Mar 2024 06:41:35 -0700
Subject: [PATCH 07/16] feat(lib): CoreM execution function

---
 Pantograph.lean         |  5 +++-
 Pantograph/Library.lean | 63 +++++++++++++++++++++++------------------
 2 files changed, 40 insertions(+), 28 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index f9b5dc5..ad563f0 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -69,7 +69,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
-    exprEcho args state.options
+    let expr ← match ← exprParse args.expr with
+      | .ok expr => pure $ expr
+      | .error e => return .error e
+    exprPrint expr state.options
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index cdc112f..a8c0ce7 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -1,6 +1,7 @@
-import Pantograph.Version
 import Pantograph.Environment
+import Pantograph.Goal
 import Pantograph.Protocol
+import Pantograph.Version
 import Lean
 
 namespace Lean
@@ -70,6 +71,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do
     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
@@ -78,11 +80,14 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
     (trustLevel := 1)
   return { env := env }
 
+/-- Execute a `CoreM` monad -/
+@[export pantograph_exec_core]
+def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α): IO (α × Lean.Core.State) :=
+  coreM.toIO context state
+
 @[export pantograph_env_catalog]
-def envCatalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do
-  let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog)
-  let (result, _) ← coreM.toIO cc cs
-  return result
+def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
+  Environment.catalog ({}: Protocol.EnvCatalog)
 
 @[export pantograph_env_inspect]
 def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State)
@@ -100,28 +105,32 @@ def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State)
   let (result, _) ← coreM.toIO cc cs
   return result
 
-def exprEcho (args: Protocol.ExprEcho) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
-    let env ← Lean.MonadEnv.getEnv
-    let syn ← match syntax_from_str env args.expr with
-      | .error str => return .error $ errorI "parsing" str
-      | .ok syn => pure syn
-    runTermElabM (do
-      match ← syntax_to_expr syn with
-      | .error str => return .error $ errorI "elab" str
-      | .ok expr => do
-        try
-          let type ← Lean.Meta.inferType expr
-          return .ok {
-              type := (← serialize_expression options type),
-              expr := (← serialize_expression options expr)
-          }
-        catch exception =>
-          return .error $ errorI "typing" (← exception.toMessageData.toString))
+@[export pantograph_expr_parse]
+def exprParse (s: String): Lean.CoreM (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
+  runTermElabM (do
+    match ← syntax_to_expr syn with
+    | .error str => return .error $ errorI "elab" str
+    | .ok expr => return .ok expr)
 
-@[export pantograph_expr_echo]
-def exprEchoExport (cc: Lean.Core.Context) (cs: Lean.Core.State) (expr: String) (options: @&Protocol.Options): IO (Protocol.CR Protocol.ExprEchoResult) := do
-  let coreM: Lean.CoreM _ := exprEcho { expr } options
-  let (result, _) ← coreM.toIO cc cs
-  return result
+@[export pantograph_expr_print]
+def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
+  let termElabM: Lean.Elab.TermElabM _ :=
+      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]
+def goalStart (expr: Lean.Expr): Lean.CoreM GoalState :=
+  runTermElabM (GoalState.create expr)
 
 end Pantograph
-- 
2.44.1


From f42a27e0366a6f5fa858ffea1379675236494377 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 10 Mar 2024 08:13:10 -0700
Subject: [PATCH 08/16] feat(lib): Expose goal state interface

---
 Pantograph.lean          | 24 +++++++---------
 Pantograph/Library.lean  | 62 +++++++++++++++++++++++++---------------
 Pantograph/Protocol.lean |  2 +-
 Pantograph/Version.lean  |  1 +
 4 files changed, 52 insertions(+), 37 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index ad563f0..cc2471f 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -49,6 +49,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       errorCommand s!"Unknown command {cmd}"
     return Lean.toJson error
   where
+  errorCommand := errorI "command"
+  errorIndex := errorI "index"
   -- Command Functions
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -93,14 +95,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
-    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none =>
-        (match syntax_from_str env expr with
-        | .error str => return .error <| errorI "parsing" str
-        | .ok syn => do
-          (match ← syntax_to_expr syn with
-          | .error str => return .error <| errorI "elab" str
-          | .ok expr => return .ok (← GoalState.create expr)))
+    let expr?: Except Protocol.InteractionError GoalState ← runTermElabM (match args.expr, args.copyFrom with
+      | .some expr, .none => do
+          match ← exprParse expr with
+          | .ok expr => return .ok (← GoalState.create expr)
+          | .error e => return .error e
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
@@ -123,9 +122,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | .some goalState => do
       let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
         | .some tactic, .none => do
-          pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic))
+          pure ( Except.ok (← goalTactic goalState args.goalId tactic))
         | .none, .some expr => do
-          pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr))
+          pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
         | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
       match nextGoalState? with
       | .error error => return .error error
@@ -157,8 +156,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
           | .some branch => pure $ target.continue branch
         | .none, .some goals =>
-          let goals := goals.map (λ name => { name := name.toName })
-          pure $ target.resume goals
+          pure $ goalResume target goals
         | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
       match nextState? with
       | .error error => return .error <| errorI "structure" error
@@ -168,7 +166,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           goalStates := state.goalStates.insert nextStateId nextGoalState,
           nextId := state.nextId + 1
         }
-        let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run'
+        let goals ← goalSerialize nextGoalState (options := state.options)
         return .ok {
           nextStateId,
           goals,
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index a8c0ce7..b1a6864 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -1,6 +1,7 @@
 import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Protocol
+import Pantograph.Serial
 import Pantograph.Version
 import Lean
 
@@ -44,11 +45,6 @@ def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
   }) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
-def errorCommand := errorI "command"
-def errorIndex := errorI "index"
-
-@[export pantograph_version]
-def pantographVersion: String := version
 
 /-- Adds the given paths to Lean package search path -/
 @[export pantograph_init_search]
@@ -82,30 +78,27 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
 
 /-- Execute a `CoreM` monad -/
 @[export pantograph_exec_core]
-def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α): IO (α × Lean.Core.State) :=
+def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α):
+    IO (α × Lean.Core.State) :=
   coreM.toIO context state
 
-@[export pantograph_env_catalog]
+@[export pantograph_env_catalog_m]
 def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
   Environment.catalog ({}: Protocol.EnvCatalog)
 
-@[export pantograph_env_inspect]
-def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State)
-    (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): IO (Protocol.CR Protocol.EnvInspectResult) := do
-  let coreM: Lean.CoreM _ := Environment.inspect ({
+@[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
-  let (result, _) ← coreM.toIO cc cs
-  return result
 
-@[export pantograph_env_add]
-def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State)
-  (name: String) (type: String) (value: String) (isTheorem: Bool): IO (Protocol.CR Protocol.EnvAddResult) := do
-  let coreM: Lean.CoreM _ := Environment.addDecl { name, type, value, isTheorem }
-  let (result, _) ← coreM.toIO cc cs
-  return result
+@[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 }
 
-@[export pantograph_expr_parse]
+@[export pantograph_expr_parse_m]
 def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do
   let env ← Lean.MonadEnv.getEnv
   let syn ← match syntax_from_str env s with
@@ -116,8 +109,9 @@ def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do
     | .error str => return .error $ errorI "elab" str
     | .ok expr => return .ok expr)
 
-@[export pantograph_expr_print]
-def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
+@[export pantograph_expr_print_m]
+def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options):
+    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
   let termElabM: Lean.Elab.TermElabM _ :=
       try
         let type ← Lean.Meta.inferType expr
@@ -129,8 +123,30 @@ def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Proto
         return .error $ errorI "typing" (← exception.toMessageData.toString)
   runTermElabM termElabM
 
-@[export pantograph_goal_start]
+@[export pantograph_goal_start_m]
 def goalStart (expr: Lean.Expr): Lean.CoreM GoalState :=
   runTermElabM (GoalState.create expr)
 
+@[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
+
+
+
 end Pantograph
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 5015ad1..91c44a8 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -221,7 +221,7 @@ structure GoalContinue where
   -- The state which is an ancestor of `target` where goals will be extracted from
   branch?: Option Nat := .none
   -- Or, the particular goals that should be brought back into scope
-  goals?: Option (List String) := .none
+  goals?: Option (Array String) := .none
   deriving Lean.FromJson
 structure GoalContinueResult where
   nextStateId: Nat
diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean
index 7bf12f9..e412ced 100644
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@@ -1,5 +1,6 @@
 namespace Pantograph
 
+@[export pantograph_version]
 def version := "0.2.12-alpha"
 
 end Pantograph
-- 
2.44.1


From 5db727e30bc9d515ccfbb867c126c4c828bcbaea Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 10 Mar 2024 15:09:38 -0700
Subject: [PATCH 09/16] fix: Execute expr parsing within goal.start

---
 Pantograph.lean         | 13 ++++++++-----
 Pantograph/Library.lean |  6 ------
 2 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index cc2471f..0168894 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -95,11 +95,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
-    let expr?: Except Protocol.InteractionError GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none => do
-          match ← exprParse expr with
-          | .ok expr => return .ok (← GoalState.create expr)
-          | .error e => return .error e
+    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
+      | .some expr, .none =>
+        (match syntax_from_str env expr with
+        | .error str => return .error <| errorI "parsing" str
+        | .ok syn => do
+          (match ← syntax_to_expr syn with
+          | .error str => return .error <| errorI "elab" str
+          | .ok expr => return .ok (← GoalState.create expr)))
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index b1a6864..f1115e1 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -76,12 +76,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
     (trustLevel := 1)
   return { env := env }
 
-/-- Execute a `CoreM` monad -/
-@[export pantograph_exec_core]
-def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α):
-    IO (α × Lean.Core.State) :=
-  coreM.toIO context state
-
 @[export pantograph_env_catalog_m]
 def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
   Environment.catalog ({}: Protocol.EnvCatalog)
-- 
2.44.1


From 285cf0416aa687cfd9d9b7cb1a2224f6eeef395d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 10 Mar 2024 15:33:32 -0700
Subject: [PATCH 10/16] feat(lib): Option creation function

---
 Pantograph.lean         | 17 ++++-------
 Pantograph/Library.lean | 64 ++++++++++++++++++++++++++++-------------
 2 files changed, 50 insertions(+), 31 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index 0168894..fceac00 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -71,10 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
-    let expr ← match ← exprParse args.expr with
-      | .ok expr => pure $ expr
-      | .error e => return .error e
-    exprPrint expr state.options
+    exprEcho args.expr state.options
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options
@@ -96,13 +93,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none =>
-        (match syntax_from_str env expr with
-        | .error str => return .error <| errorI "parsing" str
-        | .ok syn => do
-          (match ← syntax_to_expr syn with
-          | .error str => return .error <| errorI "elab" str
-          | .ok expr => return .ok (← GoalState.create expr)))
+      | .some expr, .none => do
+        let expr ← match ← exprParse expr with
+          | .error e => return .error e
+          | .ok expr => pure $ expr
+        return .ok $ ← GoalState.create expr
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index f1115e1..b731fb3 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -80,6 +80,23 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
 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) :=
@@ -92,34 +109,41 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
     Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
   Environment.addDecl { name, type, value, isTheorem }
 
-@[export pantograph_expr_parse_m]
-def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do
+/-- 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
-  runTermElabM (do
-    match ← syntax_to_expr syn with
-    | .error str => return .error $ errorI "elab" str
-    | .ok expr => return .ok expr)
+  match ← syntax_to_expr syn with
+  | .error str => return .error $ errorI "elab" str
+  | .ok expr => return .ok expr
 
-@[export pantograph_expr_print_m]
-def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options):
+@[export pantograph_expr_echo_m]
+def exprEcho (expr: String) (options: @&Protocol.Options):
     Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
-  let termElabM: Lean.Elab.TermElabM _ :=
-      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)
+  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_m]
-def goalStart (expr: Lean.Expr): Lean.CoreM GoalState :=
-  runTermElabM (GoalState.create expr)
+@[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 :=
-- 
2.44.1


From c83af044b4627eda5a12135b1ba197bea5ff3da2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 11 Mar 2024 21:31:59 -0700
Subject: [PATCH 11/16] fix: Pass options by reference

---
 Pantograph/Environment.lean | 2 +-
 Pantograph/Library.lean     | 4 ++--
 Pantograph/Serial.lean      | 8 ++++++--
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index df0bc7f..f37225f 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -37,7 +37,7 @@ def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
     | .some x => acc.push x
     | .none => acc)
   return { symbols := names }
-def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
+def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
   let env ← Lean.MonadEnv.getEnv
   let name :=  args.name.toName
   let info? := env.find? name
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index b731fb3..d72fd3a 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -98,7 +98,7 @@ def mkOptions
   }
 
 @[export pantograph_env_inspect_m]
-def envInspect (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options):
+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
@@ -162,7 +162,7 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat
   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) :=
+def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
   runMetaM <| state.serializeGoals (parent := .none) options
 
 
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 547b3dc..213ae6d 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -172,7 +172,7 @@ def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol
   }
 
 /-- Adapted from ppGoal -/
-def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
       : MetaM Protocol.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
@@ -242,7 +242,11 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar
   where
   of_name (n: Name) := name_to_ast n (sanitize := false)
 
-protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
+protected def GoalState.serializeGoals
+      (state: GoalState)
+      (parent: Option GoalState := .none)
+      (options: @&Protocol.Options := {}):
+    MetaM (Array Protocol.Goal):= do
   state.restoreMetaM
   let goals := state.goals.toArray
   let parentDecl? := parent.bind (λ parentState =>
-- 
2.44.1


From b64adf31cfa319bd220fb821ee6521c56d00b171 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 14 Mar 2024 16:34:01 -0700
Subject: [PATCH 12/16] feat(lib): Export goal.print function

---
 Pantograph.lean         | 8 +-------
 Pantograph/Library.lean | 9 +++++++++
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index fceac00..bcf8395 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -179,12 +179,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     match state.goalStates.find? args.stateId with
     | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
     | .some goalState => runMetaM <| do
-      goalState.restoreMetaM
-      let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
-      let parent? ← goalState.parentExpr?.mapM (λ expr => serialize_expression state.options expr)
-      return .ok {
-        root?,
-        parent?,
-      }
+      return .ok (← goalPrint goalState state.options)
 
 end Pantograph
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index d72fd3a..52a88b6 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -165,6 +165,15 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat
 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
-- 
2.44.1


From 689112d973404ce6da01aae6bd476e0fb7892343 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 14 Mar 2024 22:40:14 -0700
Subject: [PATCH 13/16] fix: Use Arrays only in the ABI

---
 Pantograph/Environment.lean | 6 +++---
 Pantograph/Protocol.lean    | 7 ++++---
 Test/Environment.lean       | 8 ++++----
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index f37225f..ecae517 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -66,8 +66,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     | .inductInfo induct => { core with inductInfo? := .some {
           numParams := induct.numParams,
           numIndices := induct.numIndices,
-          all := induct.all.map (·.toString),
-          ctors := induct.ctors.map (·.toString),
+          all := induct.all.toArray.map (·.toString),
+          ctors := induct.ctors.toArray.map (·.toString),
           isRec := induct.isRec,
           isReflexive := induct.isReflexive,
           isNested := induct.isNested,
@@ -79,7 +79,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           numFields := ctor.numFields,
       } }
     | .recInfo r => { core with recursorInfo? := .some {
-          all := r.all.map (·.toString),
+          all := r.all.toArray.map (·.toString),
           numParams := r.numParams,
           numIndices := r.numIndices,
           numMotives := r.numMotives,
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 91c44a8..e9a5f87 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -124,8 +124,8 @@ structure EnvInspect where
 structure InductInfo where
   numParams: Nat
   numIndices: Nat
-  all: List String
-  ctors: List String
+  all: Array String
+  ctors: Array String
   isRec:       Bool := false
   isReflexive: Bool := false
   isNested:    Bool := false
@@ -138,7 +138,7 @@ structure ConstructorInfo where
   numFields: Nat
   deriving Lean.ToJson
 structure RecursorInfo where
-  all: List String
+  all: Array String
   numParams: Nat
   numIndices: Nat
   numMotives: Nat
@@ -230,6 +230,7 @@ structure GoalContinueResult where
 
 -- Remove goal states
 structure GoalDelete where
+  -- This is ok being a List because it doesn't show up in the ABI
   stateIds: List Nat
   deriving Lean.FromJson
 structure GoalDeleteResult where
diff --git a/Test/Environment.lean b/Test/Environment.lean
index df3f3ae..977ed7d 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -34,8 +34,8 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
     ("Or", ConstantCat.induct {
       numParams := 2,
       numIndices := 0,
-      all := ["Or"],
-      ctors := ["Or.inl", "Or.inr"],
+      all := #["Or"],
+      ctors := #["Or.inl", "Or.inr"],
     }),
     ("Except.ok", ConstantCat.ctor {
       induct := "Except",
@@ -44,7 +44,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
       numFields := 1,
     }),
     ("Eq.rec", ConstantCat.recursor {
-      all := ["Eq"],
+      all := #["Eq"],
       numParams := 2,
       numIndices := 1,
       numMotives := 1,
@@ -52,7 +52,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
       k := true,
     }),
     ("ForM.rec", ConstantCat.recursor {
-      all := ["ForM"],
+      all := #["ForM"],
       numParams := 3,
       numIndices := 0,
       numMotives := 1,
-- 
2.44.1


From b7542b4749015d8ee6f43f656256d955e00bf94b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 15 Mar 2024 06:01:25 -0700
Subject: [PATCH 14/16] chore: Lean version bump to 4.7.0-rc2

Multithreading in ABI was not stabilized in 4.1.0
---
 Makefile           |  8 ++++----
 flake.lock         |  8 ++++----
 flake.nix          |  2 +-
 lake-manifest.json | 24 +++++++++++++-----------
 lakefile.lean      |  2 +-
 lean-toolchain     |  2 +-
 6 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/Makefile b/Makefile
index 39350b6..5d4ad6b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,8 @@
-LIB := build/lib/Pantograph.olean
-EXE := build/bin/pantograph
+LIB := ./.lake/build/lib/Pantograph.olean
+EXE := ./.lake/build/bin/pantograph
 SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
 
-TEST_EXE := build/bin/test
+TEST_EXE := ./.lake/build/bin/test
 TEST_SOURCE := $(wildcard Test/*.lean)
 
 $(LIB) $(EXE): $(SOURCE)
@@ -12,7 +12,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 	lake build test
 
 test: $(TEST_EXE)
-	lake env $(TEST_EXE)
+	$(TEST_EXE)
 
 clean:
 	lake clean
diff --git a/flake.lock b/flake.lock
index 67246b6..89f0e9d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -41,16 +41,16 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1695693562,
-        "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
+        "lastModified": 1709691092,
+        "narHash": "sha256-jHY8BhDotfGcMS0Xzl5iawqCaug3dDEKuD5Y1WcM06I=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
+        "rev": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "v4.1.0",
+        "ref": "v4.7.0-rc2",
         "repo": "lean4",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 9f586f6..54640d3 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=v4.1.0";
+    lean.url = "github:leanprover/lean4?ref=v4.7.0-rc2";
   };
 
   outputs = inputs @ {
diff --git a/lake-manifest.json b/lake-manifest.json
index 6c2efa0..6ebbbe5 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,12 +1,14 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/lurk-lab/LSpec.git",
-    "subDir?": null,
-    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-    "opts": {},
-    "name": "LSpec",
-    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-    "inherited": false}}],
- "name": "pantograph"}
+ [{"url": "https://github.com/lurk-lab/LSpec.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "pantograph",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 89ad70f..d7bc630 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -15,7 +15,7 @@ lean_exe pantograph {
 }
 
 require LSpec from git
-  "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
+  "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
 lean_lib Test {
 }
 lean_exe test {
diff --git a/lean-toolchain b/lean-toolchain
index a9bddf0..faa2254 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.1.0
+leanprover/lean4:4.7.0-rc2
-- 
2.44.1


From bb09d1e96457ae9f2ba3bfed5aaee6fb23661d41 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 15 Mar 2024 18:44:28 -0700
Subject: [PATCH 15/16] chore: Version bump to 4.8.0 prerelease

---
 flake.lock | 8 ++++----
 flake.nix  | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/flake.lock b/flake.lock
index 89f0e9d..6278d68 100644
--- a/flake.lock
+++ b/flake.lock
@@ -41,16 +41,16 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1709691092,
-        "narHash": "sha256-jHY8BhDotfGcMS0Xzl5iawqCaug3dDEKuD5Y1WcM06I=",
+        "lastModified": 1710520221,
+        "narHash": "sha256-8Fm4bj9sqqsUHFZweSdGMM5GdUX3jkGK/ggGq27CeQc=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a",
+        "rev": "f70895ede54501adf0db77474f452a7fef40d0b3",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "v4.7.0-rc2",
+        "ref": "f70895ede54501adf0db77474f452a7fef40d0b3",
         "repo": "lean4",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 54640d3..dd98225 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=v4.7.0-rc2";
+    lean.url = "github:leanprover/lean4?ref=f70895ede54501adf0db77474f452a7fef40d0b3";
   };
 
   outputs = inputs @ {
-- 
2.44.1


From a3a244159bebd19677a18e0d6704a5ae18d631d6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 16 Mar 2024 19:00:28 -0700
Subject: [PATCH 16/16] chore: Version bump to 0.2.13

---
 Pantograph/Version.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean
index e412ced..e23d886 100644
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.12-alpha"
+def version := "0.2.13"
 
 end Pantograph
-- 
2.44.1