From 2b71203c1e800dcd5085bf3b5ec58b5136186dc1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 30 Mar 2024 00:17:16 -0700
Subject: [PATCH 1/2] fix: Instantiation causes infinite loop

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

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index f44fcad..15bde0e 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -127,7 +127,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
       | .error e => return .error e
       | .ok expr => pure expr
     try
-      let type ← instantiateAll (← Lean.Meta.inferType expr)
+      let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr)
       return .ok {
           type := (← serialize_expression options type),
           expr := (← serialize_expression options expr)
@@ -171,9 +171,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
     state.restoreMetaM
     return {
       root? := ← state.rootExpr?.mapM (λ expr => do
-        serialize_expression options (← instantiateAll expr)),
+        serialize_expression options (← unfoldAuxLemmas expr)),
       parent? := ← state.parentExpr?.mapM (λ expr => do
-        serialize_expression options (← instantiateAll expr)),
+        serialize_expression options (← unfoldAuxLemmas expr)),
     }
   runMetaM metaM
 
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index f829611..bf79314 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -18,10 +18,6 @@ namespace Pantograph
 def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
-def instantiateAll (e: Lean.Expr) : Lean.MetaM Lean.Expr := do
-  let e ← unfoldAuxLemmas e
-  instantiateMVars (← Lean.Meta.whnf e)
-
 --- Input Functions ---
 
 /-- Read syntax object from string -/

From e9c9548f174d0aeb80589ea8415978538407b925 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 31 Mar 2024 15:40:14 -0700
Subject: [PATCH 2/2] fix: unfoldAuxLemma should be coreM

---
 Pantograph/Environment.lean | 2 +-
 Pantograph/Serial.lean      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index 19c3249..303c2b5 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -64,7 +64,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       else .none,
     valueDependency? := ← if args.dependency?.getD false
       then info.value?.mapM (λ e => do
-        let e ← (unfoldAuxLemmas e).run'
+        let e ← unfoldAuxLemmas e
         pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
       else pure (.none),
     module? := module?
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index bf79314..7377c68 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -15,7 +15,7 @@ def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxL
 namespace Pantograph
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
+def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
 --- Input Functions ---