Makefile

@@ -6,7 +6,7 @@ TEST_EXE := build/bin/test
 TEST_SOURCE := $(wildcard Test/*.lean)
 
 $(LIB) $(EXE): $(SOURCE)
-	lake build
+	lake build pantograph
 
 $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 	lake build test
@@ -14,4 +14,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 test: $(TEST_EXE)
 	lake env $(TEST_EXE)
 
-.PHONY: test
+clean:
+	lake clean
+
+.PHONY: test clean

Pantograph.lean

@@ -1,7 +1,7 @@
 import Pantograph.Commands
 import Pantograph.Serial
 import Pantograph.Symbols
-import Pantograph.Tactic
+import Pantograph.Goal
 import Pantograph.SemihashMap
 
 namespace Pantograph

Pantograph/Goal.lean

@@ -31,12 +31,15 @@ structure GoalState where
 abbrev M := Elab.TermElabM
 
 def GoalState.create (expr: Expr): M GoalState := do
+  -- 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))
+  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
   let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
   let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
   return {
-    savedState := savedState,
+    savedState,
     mvarId := goal.mvarId!
   }
 
@@ -52,7 +55,9 @@ def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Strin
         let errors ← (messages.map Message.data).mapM fun md => md.toString
         return .error errors
       else
-        return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals)
+        let unsolved ← Elab.Tactic.getUnsolvedGoals
+        -- The order of evaluation is important here
+        return .ok (← MonadBacktrack.saveState, unsolved)
     catch exception =>
       return .error #[← exception.toMessageData.toString]
   match Parser.runParserCategory

Pantograph/Serial.lean

@@ -28,19 +28,11 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
 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)
 
@@ -249,7 +241,7 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe
       caseName? := match mvarDecl.userName with
         | Name.anonymous => .none
         | name => .some <| toString name,
-      isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
+      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
       target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
     }

Test/Holes.lean

@@ -1,5 +1,5 @@
 import LSpec
-import Pantograph.Tactic
+import Pantograph.Goal
 import Pantograph.Serial
 
 namespace Pantograph.Test.Holes

Test/Proofs.lean

@@ -1,5 +1,5 @@
 import LSpec
-import Pantograph.Tactic
+import Pantograph.Goal
 import Pantograph.Serial
 
 namespace Pantograph.Test.Proofs
@@ -39,7 +39,7 @@ def start_proof (start: Start): TestM (Option GoalState) := do
       IO.println error
       return Option.none
     | .ok syn =>
-      let expr? ← syntax_to_expr syn
+      let expr? ← syntax_to_expr_type syn
       add_test $ LSpec.check s!"Elaborating" expr?.isOk
       match expr? with
       | .error error =>
@@ -213,7 +213,7 @@ def proof_runner (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 := {
-    currNamespace := str_to_name "Aniva",
+    currNamespace := Name.append .anonymous "Aniva",
     openDecls := [],     -- No 'open' directives needed
     fileName := "<Pantograph>",
     fileMap := { source := "", positions := #[0], lines := #[1] }
@@ -232,7 +232,7 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :
 /-- Tests the most basic form of proofs whose goals do not relate to each other -/
 def suite: IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
-    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
     (opts := {})
     (trustLevel := 1)
   let tests := [