From 435431ca7e08b66abca030611820abdd483715db Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 13 Apr 2021 19:10:39 +0200 Subject: [PATCH] feat: hide elaboration errors from partial syntax trees by default --- src/Lean/Elab/Frontend.lean | 14 +++++++++++--- src/Lean/Server/Snapshots.lean | 16 +++++++++------- tests/lean/348.lean.expected.out | 9 --------- tests/lean/StxQuot.lean.expected.out | 8 -------- tests/lean/eoi.lean.expected.out | 1 - tests/lean/exitAfterParseError.lean.expected.out | 1 - tests/lean/precissues.lean.expected.out | 2 -- tests/lean/tokenErrors.lean.expected.out | 8 -------- tests/lean/unknownTactic.lean.expected.out | 10 ---------- tests/lean/weirdmacro.lean.expected.out | 3 --- 10 files changed, 20 insertions(+), 52 deletions(-) diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index cebd5772c6..d648d89f0e 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/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 diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index 103c4f81aa..cea14928a4 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/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 diff --git a/tests/lean/348.lean.expected.out b/tests/lean/348.lean.expected.out index 2a46438639..4abed64a94 100644 --- a/tests/lean/348.lean.expected.out +++ b/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 diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 6d9542021f..498fa36a71 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/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" "" "" @@ -11,10 +7,6 @@ StxQuot.lean:8:0-8:12: error: failed to synthesize "(term_+_ \"+\" (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\") [])))]" diff --git a/tests/lean/eoi.lean.expected.out b/tests/lean/eoi.lean.expected.out index e3ece41a45..89a2853718 100644 --- a/tests/lean/eoi.lean.expected.out +++ b/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 diff --git a/tests/lean/exitAfterParseError.lean.expected.out b/tests/lean/exitAfterParseError.lean.expected.out index ced20411fb..87d0dd244a 100644 --- a/tests/lean/exitAfterParseError.lean.expected.out +++ b/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 diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out index 56b7e6d7ff..6ad63029a9 100644 --- a/tests/lean/precissues.lean.expected.out +++ b/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 = diff --git a/tests/lean/tokenErrors.lean.expected.out b/tests/lean/tokenErrors.lean.expected.out index 362fbce916..567df327cc 100644 --- a/tests/lean/tokenErrors.lean.expected.out +++ b/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 diff --git a/tests/lean/unknownTactic.lean.expected.out b/tests/lean/unknownTactic.lean.expected.out index e9e743df06..da22471d63 100644 --- a/tests/lean/unknownTactic.lean.expected.out +++ b/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 diff --git a/tests/lean/weirdmacro.lean.expected.out b/tests/lean/weirdmacro.lean.expected.out index e3dc899952..d9a1728085 100644 --- a/tests/lean/weirdmacro.lean.expected.out +++ b/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'