From 64971a1e3cbf00e89e394beb24c6ce9331d85a19 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 4 Jan 2022 11:14:57 +0100 Subject: [PATCH] fix: term macro errors should be fatal --- src/Lean/Elab/Term.lean | 3 ++- tests/lean/macroError.lean | 3 +++ tests/lean/macroError.lean.expected.out | 1 + 3 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 tests/lean/macroError.lean create mode 100644 tests/lean/macroError.lean.expected.out diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 2bf15f5001..1c8e813172 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1216,7 +1216,8 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : withNestedTraces do let env ← getEnv match (← liftMacroM (expandMacroImpl? env stx)) with - | some (decl, Except.ok stxNew) => + | some (decl, stxNew?) => + let stxNew ← liftMacroM <| liftExcept stxNew? withInfoContext' (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <| withMacroExpansion stx stxNew <| withRef stxNew <| diff --git a/tests/lean/macroError.lean b/tests/lean/macroError.lean new file mode 100644 index 0000000000..d81ed4b1bc --- /dev/null +++ b/tests/lean/macroError.lean @@ -0,0 +1,3 @@ +macro "foo" : term => Lean.Macro.throwError "Test Error" + +#check foo diff --git a/tests/lean/macroError.lean.expected.out b/tests/lean/macroError.lean.expected.out new file mode 100644 index 0000000000..c6ebf13697 --- /dev/null +++ b/tests/lean/macroError.lean.expected.out @@ -0,0 +1 @@ +macroError.lean:3:7-3:10: error: Test Error