From 431ca4e481fb1856d36ed17f322419ab59ed8e25 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 Jul 2024 17:57:01 -0700
Subject: [PATCH] fix: Move elab context to condensed

---
 Pantograph/Condensed.lean | 5 +++--
 Pantograph/Library.lean   | 6 ++----
 Test/Common.lean          | 2 +-
 Test/Metavar.lean         | 2 +-
 Test/Proofs.lean          | 2 +-
 Test/Serial.lean          | 4 ++--
 6 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index a1688f1..ac41133 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -50,12 +50,13 @@ def metaContext: Meta.Context := {}
 @[export pantograph_meta_state]
 def metaState: Meta.State := {}
 @[export pantograph_elab_context]
-def elabContext: Meta.Context := {}
+def elabContext: Elab.Term.Context := {
+    errToSorry := false
+  }
 @[export pantograph_elab_state]
 def elabState (levelNames: Array Name): Elab.Term.State := {
     levelNames := levelNames.toList,
   }
 
 
-
 end Pantograph.Condensed
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 3bc3cc1..2f37cfa 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -1,3 +1,4 @@
+import Pantograph.Condensed
 import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Protocol
@@ -38,13 +39,10 @@ open Lean
 
 namespace Pantograph
 
-def defaultTermElabMContext: Elab.Term.Context := {
-    errToSorry := false
-  }
 def runMetaM { α } (metaM: MetaM α): CoreM α :=
   metaM.run'
 def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
-  termElabM.run' (ctx := defaultTermElabMContext) |>.run'
+  termElabM.run' (ctx := Condensed.elabContext) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 
diff --git a/Test/Common.lean b/Test/Common.lean
index e4e1d4c..4b17736 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -73,7 +73,7 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
 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 := Pantograph.defaultTermElabMContext)
+  termElabM.run' (ctx := Pantograph.Condensed.elabContext)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 0818881..4ac8454 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -67,7 +67,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
   let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+  let metaM := termElabM.run' (ctx := Condensed.elabContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 9c45138..51e869d 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -76,7 +76,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
   let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+  let metaM := termElabM.run' (ctx := Condensed.elabContext)
   let coreM := metaM.run'
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
diff --git a/Test/Serial.lean b/Test/Serial.lean
index 2d2b9d1..1c00501 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
         | .ok expr => pure expr
         | .error e => return elabFailure e
       return LSpec.check source ((← serializeExpressionSexp expr) = target)
-    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultTermElabMContext)
+    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
     return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
     LSpec.TestSeq.done
 
@@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
     let testCaseName := target.take 10
     let test := LSpec.check   testCaseName ((← serializeExpressionSexp expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
+  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
 
 -- Instance parsing
 def test_instance (env: Environment): IO LSpec.TestSeq :=