From 3b83c81540e2aa2571b8b3c793e29f56db8cc022 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 15 Dec 2023 13:07:59 -0500
Subject: [PATCH] fix: Force instantiate all mvars in env.add

---
 Pantograph.lean       |  1 +
 Test/Integration.lean | 22 +++++++++++++++++++---
 2 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index aeb920e..2bd066e 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -114,6 +114,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           | .ok syn => do
             try
               let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
+              Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
               let expr ← Lean.instantiateMVars expr
               pure $ expr
             catch ex => return .error (← ex.toMessageData.toString)
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 351efa3..0a6c210 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -113,21 +113,37 @@ def test_tactic : IO LSpec.TestSeq :=
   ]
 
 def test_env : IO LSpec.TestSeq :=
-  let name := "Pantograph.Mystery"
+  let name1 := "Pantograph.mystery"
+  let name2 := "Pantograph.mystery2"
   subroutine_runner [
     subroutine_step "env.add"
       [
-        ("name", .str name),
+        ("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 name)]
+      [("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 => Int.ofNat a + 1" },
+       type := { pp? := .some "Nat → Int" },
      }:
       Protocol.EnvInspectResult))
   ]