From ed1eee201ab906946244517f0ab070c2dcc9a63a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 May 2021 20:53:43 -0700 Subject: [PATCH] fix: avoid "failed to evaluate" error when extension has `sorry` See updated test output. --- src/Lean/KeyedDeclsAttribute.lean | 10 ++++++++-- tests/lean/435.lean.expected.out | 1 - tests/lean/notationPrecheck.lean.expected.out | 2 -- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 6b8921d025..fa22052dc8 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -7,6 +7,7 @@ import Lean.Attributes import Lean.Compiler.InitAttr import Lean.ToExpr import Lean.ScopedEnvExtension +import Lean.Compiler.IR.CompilerM /-! A builder for attributes that are applied to declarations of a common type and @@ -129,8 +130,13 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe descr := df.descr add := fun constName stx attrKind => do let key ← df.evalKey false stx - let val ← evalConstCheck γ df.valueTypeName constName - ext.add { key := key, decl := constName, value := val } attrKind + match IR.getSorryDep (← getEnv) constName with + | none => + let val ← evalConstCheck γ df.valueTypeName constName + ext.add { key := key, decl := constName, value := val } attrKind + | _ => + -- If the declaration contains `sorry`, we skip `evalConstCheck` to avoid unnecessary bizarre error message + pure () applicationTime := AttributeApplicationTime.afterCompilation } pure { defn := df, tableRef := tableRef, ext := ext } diff --git a/tests/lean/435.lean.expected.out b/tests/lean/435.lean.expected.out index a0d0be8961..c2279730f3 100644 --- a/tests/lean/435.lean.expected.out +++ b/tests/lean/435.lean.expected.out @@ -1,3 +1,2 @@ 435.lean:3:37-3:42: warning: declaration uses 'sorry' 435.lean:5:21-5:23: error: unknown identifier 'op' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. -435.lean:5:0-5:23: error: cannot evaluate code because it uses 'sorry' and/or contains errors diff --git a/tests/lean/notationPrecheck.lean.expected.out b/tests/lean/notationPrecheck.lean.expected.out index def14deaa9..a1f123efaa 100644 --- a/tests/lean/notationPrecheck.lean.expected.out +++ b/tests/lean/notationPrecheck.lean.expected.out @@ -1,8 +1,6 @@ notationPrecheck.lean:1:25-1:26: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. -notationPrecheck.lean:1:0-1:26: error: cannot evaluate code because it uses 'sorry' and/or contains errors notationPrecheck.lean:4:16-4:19: error: no macro or `[quotPrecheck]` instance for syntax kind 'termB_' found b x This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check. -notationPrecheck.lean:4:0-4:19: error: cannot evaluate code because it uses 'sorry' and/or contains errors notationPrecheck.lean:8:7-8:8: error: elaboration function for 'termB_' has not been implemented b x✝