Fix elab async issue in tactic mode + add 2 new tests

Author: augustepoiroux

REPL/Snapshots.lean

@@ -211,9 +211,12 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option
       let s := match prevEnv? with
       | none => s
       | some env => { s with env }
+      let coreCtx ← readThe Core.Context
+      -- Ensure tactic snapshots run synchronously.
+      let coreCtx := { coreCtx with options := coreCtx.options.insert `Elab.async false }
       pure <|
       { coreState := s
-        coreContext := ← readThe Core.Context
+        coreContext := coreCtx
         metaState := ← getThe Meta.State
         metaContext := ← readThe Meta.Context
         termState := {}

test/app_type_mismatch2_parallel.expected.out

@@ -0,0 +1,41 @@
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data":
+   "(kernel) application type mismatch\n  @Eq.ndrec Nat (n✝ + 1) (fun x => x = 0)\n    (have this := of_decide_eq_true (id (Eq.refl true));\n    of_decide_eq_true (id (Eq.refl true)))\nargument has type\n  true = true\nbut function has type\n  (fun x => x = 0) (n✝ + 1) → ∀ {b : Nat}, n✝ + 1 = b → (fun x => x = 0) b"}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 19},
+   "goal": "⊢ 1 = 0",
+   "endPos": {"line": 1, "column": 24}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["case zero\n⊢ 0 = 0", "case succ\nn✝ : Nat\n⊢ n✝ + 1 = 0"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["case succ\nn✝ : Nat\n⊢ n✝ + 1 = 0"]}
+
+{"proofStatus":
+ "Error: kernel type check failed: (kernel) application type mismatch\n  @Eq.ndrec Nat (n✝ + 1) (fun x => x = 0)\n    (have this := of_decide_eq_true (id (Eq.refl true));\n    of_decide_eq_true (id (Eq.refl true)))\nargument has type\n  true = true\nbut function has type\n  (fun x => x = 0) (n✝ + 1) → ∀ {b : Nat}, n✝ + 1 = b → (fun x => x = 0) b",
+ "proofState": 3,
+ "goals": []}
+
+{"sorries": [{"proofState": 4, "goal": "n✝ : Nat\n⊢ true = true"}],
+ "proofStatus": "Incomplete: open goals remain",
+ "proofState": 5,
+ "goals": ["case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0"]}
+
+{"message":
+ "Lean error:\nTactic `apply` failed: could not unify the type of `?succ`\n  n✝ + 1 = 0\nwith the goal\n  true = true\n\nn✝ : Nat\n⊢ true = true"}
+

test/app_type_mismatch2_parallel.in

@@ -0,0 +1,14 @@
+{"cmd": "example : 1 = 0 := by\n  cases 1\n  rfl\n  have: true := by\n    apply ?succ\n    trivial", "setOptions":[[["Elab","async"],true]]}
+
+{"cmd": "example : 1 = 0 := sorry", "setOptions":[[["Elab","async"],true]]}
+
+{"tactic": "cases 1", "proofState": 0}
+
+{"tactic": "rfl", "proofState": 1}
+
+{"tactic": "have: true := by\n    apply ?succ\n    trivial", "proofState": 2}
+
+{"tactic": "have: true := sorry", "proofState": 2}
+
+{"tactic": "apply ?succ", "proofState": 4}
+

test/set_option.expected.out

@@ -0,0 +1,21 @@
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 8, "column": 0},
+   "endPos": {"line": 8, "column": 8},
+   "data": "Elab.async = false"}],
+ "env": 0}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 10, "column": 0},
+   "endPos": {"line": 10, "column": 8},
+   "data": "Elab.async = true"}],
+ "env": 1}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 8, "column": 0},
+   "endPos": {"line": 8, "column": 8},
+   "data": "Elab.async = true"}],
+ "env": 2}
+

test/set_option.in

@@ -0,0 +1,6 @@
+{"cmd": "import Lean\nopen Lean Elab Command\n\nelab \"#show_pp\" : command => do\n  let o ← getOptions\n  logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp"}
+
+{"cmd": "import Lean\nopen Lean Elab Command\n\nset_option Elab.async true\n\nelab \"#show_pp\" : command => do\n  let o ← getOptions\n  logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp"}
+
+{"cmd": "import Lean\nopen Lean Elab Command\n\nelab \"#show_pp\" : command => do\n  let o ← getOptions\n  logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp", "setOptions":[[["Elab","async"],true]]}
+