feat: hide elaboration errors from partial syntax trees by default

src/Lean/Elab/Frontend.lean

@@ -49,6 +49,11 @@ def setParserState (ps : Parser.ModuleParserState) : FrontendM Unit := modify fu
 def setMessages (msgs : MessageLog) : FrontendM Unit := modify fun s => { s with commandState := { s.commandState with messages := msgs } }
 def getInputContext : FrontendM Parser.InputContext := do pure (← read).inputCtx
 
+register_builtin_option showPartialSyntaxErrors : Bool := {
+  defValue := false
+  descr    := "show elaboration errors from partial syntax tree (i.e. after parser recovery)"
+}
+
 def processCommand : FrontendM Bool := do
   updateCmdPos
   let cmdState ← getCommandState
@@ -57,15 +62,18 @@ def processCommand : FrontendM Bool := do
   let scope := cmdState.scopes.head!
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let pos := ictx.fileMap.toPosition pstate.pos
-  match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with
-  | (cmd, ps, messages) =>
+  match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate {} with
+  | (cmd, ps, parseMessages) =>
     modify fun s => { s with commands := s.commands.push cmd }
     setParserState ps
-    setMessages messages
+    setMessages (cmdState.messages ++ parseMessages)
     if Parser.isEOI cmd || Parser.isExitCommand cmd then
       pure true -- Done
     else
       profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd
+      if parseMessages.hasErrors && !showPartialSyntaxErrors.get scope.opts then
+        -- discard elaboration errors
+        setMessages (cmdState.messages ++ parseMessages)
       pure false
 
 partial def processCommands : FrontendM Unit := do

src/Lean/Server/Snapshots.lean

@@ -6,8 +6,7 @@ Authors: Wojciech Nawrocki
 -/
 import Init.System.IO
 
-import Lean.Elab.Import
-import Lean.Elab.Command
+import Lean.Elab.Frontend
 
 /-! One can think of this module as being a partial reimplementation
 of Lean.Elab.Frontend which also stores a snapshot of the world after
@@ -91,13 +90,13 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
   let cmdState := snap.cmdState
   let scope := cmdState.scopes.head!
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
-  let (cmdStx, cmdParserState, msgLog) :=
-    Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog
+  let (cmdStx, cmdParserState, parserMessages) :=
+    Parser.parseCommand inputCtx pmctx snap.mpState {}
   let cmdPos := cmdStx.getPos?.get!
   if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
-    Sum.inr msgLog
+    Sum.inr (snap.msgLog ++ parserMessages)
   else
-    let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog }
+    let cmdStateRef ← IO.mkRef { snap.cmdState with messages := snap.msgLog ++ parserMessages }
     let cmdCtx : Elab.Command.Context := {
         cmdPos   := snap.endPos
         fileName := inputCtx.fileName
@@ -107,7 +106,10 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
       Elab.Command.catchExceptions
         (Elab.Command.elabCommand cmdStx)
         cmdCtx cmdStateRef
-    let postCmdState ← cmdStateRef.get
+    let mut postCmdState ← cmdStateRef.get
+    if parserMessages.hasErrors && !Frontend.showPartialSyntaxErrors.get scope.opts then
+      -- discard elaboration errors
+      postCmdState := { postCmdState with messages := snap.msgLog ++ parserMessages }
     let postCmdSnap : Snapshot := {
         beginPos := cmdPos
         stx := cmdStx

tests/lean/348.lean.expected.out

@@ -1,10 +1 @@
 348.lean:3:24: error: expected ')'
-348.lean:3:8-3:24: error: unexpected parentheses notation
-348.lean:3:2-3:24: error: application type mismatch
-  pure PUnit.unit
-argument
-  PUnit.unit
-has type
-  PUnit : Sort ?u
-but is expected to have type
-  String : Type

tests/lean/StxQuot.lean.expected.out

@@ -1,8 +1,4 @@
 StxQuot.lean:8:12: error: expected command, identifier or term
-StxQuot.lean:8:10-8:12: error: unexpected syntax
-  failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
-StxQuot.lean:8:0-8:12: error: failed to synthesize
-  MetaEval ?m
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "<missing>"
 "<missing>"
@@ -11,10 +7,6 @@ StxQuot.lean:8:0-8:12: error: failed to synthesize
 "(term_+_ <missing> \"+\" (numLit \"1\"))"
 "(term_+_ (numLit \"1\") \"+\" (numLit \"1\"))"
 StxQuot.lean:18:15: error: expected term
-StxQuot.lean:18:10-18:15: error: unexpected syntax
-  failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
-StxQuot.lean:18:0-18:15: error: failed to synthesize
-  MetaEval ?m
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] \"=>\" `a._@.UnhygienicMain._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\") [])))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\") [])))]"

tests/lean/eoi.lean.expected.out

@@ -1,2 +1 @@
 eoi.lean:2:0: error: unexpected end of input; expected ':=', 'where' or '|'
-eoi.lean:1:0-1:13: error: declaration body is missing

tests/lean/exitAfterParseError.lean.expected.out

@@ -1,2 +1 @@
 exitAfterParseError.lean:5:0: error: expected ':=', 'where' or '|'
-exitAfterParseError.lean:3:0-3:7: error: declaration body is missing

tests/lean/precissues.lean.expected.out

@@ -5,9 +5,7 @@ f 1 fun (x : Nat) => x : Nat
 f 1 fun (x : Nat) => x : Nat
 id : ?m → ?m
 precissues.lean:15:10: error: expected command
-id : ?m → ?m
 precissues.lean:17:10: error: expected command
-1 : Nat
 id ((fun (this : True) => this) True.intro) : True
 0 = (fun (this : Nat) => this) 1 : Prop
 0 =

tests/lean/tokenErrors.lean.expected.out

@@ -3,13 +3,5 @@ tokenErrors.lean:2:9: error: invalid escape sequence
 tokenErrors.lean:3:7: error: unterminated string literal
 tokenErrors.lean:4:11: error: unterminated identifier escape
 tokenErrors.lean:6:0: error: unterminated comment
-tokenErrors.lean:5:0-5:3: error: unexpected doc string
-  failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
 tokenErrors.lean:7:0: error: unterminated comment
-tokenErrors.lean:6:0-6:6: error: unknown constant '[anonymous]'
-inductive Nat : Type
-constructors:
-Nat.zero : Nat
-Nat.succ : Nat → Nat
 tokenErrors.lean:7:1: error: unterminated comment
-tokenErrors.lean:7:0-7:1: error: unexpected command

tests/lean/unknownTactic.lean.expected.out

@@ -1,15 +1,5 @@
 unknownTactic.lean:3:3: error: unknown tactic
-unknownTactic.lean:1:41-3:8: error: unsolved goals
-x : Nat
-a✝ : x = x
-⊢ x = x
 ---
 unknownTactic.lean:8:17: error: unknown tactic
-unknownTactic.lean:8:2-8:19: error: unsolved goals
-x : Nat
-⊢ x = x
 ---
 unknownTactic.lean:14:17: error: unknown tactic
-unknownTactic.lean:14:2-14:19: error: unsolved goals
-x : Nat
-⊢ x = x

tests/lean/weirdmacro.lean.expected.out

@@ -1,6 +1,3 @@
 weirdmacro.lean:1:6: error: expected no space before ':' or string literal
-weirdmacro.lean:1:0-1:5: error: unexpected syntax
-  failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
 weirdmacro.lean:1:30-1:32: error: elaboration function for 'antiquot' has not been implemented
 weirdmacro.lean:1:32: error: expected command
-weirdmacro.lean:3:7-3:11: error: unknown identifier 'term'