diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index 7d1cde8ba0..cafe2e07f2 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -21,6 +21,10 @@ def abstractProof [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadOptions m] [ let type ← (Core.betaReduce type : MetaM _) let type ← zetaReduce type let type ← postprocessType type + /- https://github.com/leanprover/lean4/issues/10196 + If we use the cache when the proof contains `sorry`, + then we may fail to get a "declaration contains 'sorry'" warning for the current declaration. -/ + let cache := cache && !proof.hasSorry /- We turn on zetaDelta-expansion to make sure we don't need to perform an expensive `check` step to identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zetaDelta expansion step. In a benchmark created by @selsam, The extra `check` step was a bottleneck. -/ diff --git a/tests/lean/run/10196.lean b/tests/lean/run/10196.lean new file mode 100644 index 0000000000..e848aef4bd --- /dev/null +++ b/tests/lean/run/10196.lean @@ -0,0 +1,53 @@ +/-! +# Abstracting nested proofs hid 'sorry' warnings +https://github.com/leanprover/lean4/issues/10196 +-/ + +/-! +Simplified version. The second `g'` did not use to have a warning. +It re-used the `g._proof_1` proof. +-/ + +def f (n : Nat) (_ : n ≠ 0) : Nat := n +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def g (m : Nat) := f m sorry +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def g' (m : Nat) := f m sorry + +/-! +Examples from the issue. The `ByteString.Pos.next` definition did not use to have a warning. +-/ +structure ByteString where +structure ByteString.Pos (s : ByteString) where +structure ByteString.Slice where +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def ByteString.toSlice (s : ByteString) : ByteString.Slice := + sorry +structure ByteString.Slice.Pos (s : ByteString.Slice) where +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def ByteString.Slice.endPos (s : ByteString.Slice) : s.Pos := + sorry +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def ByteString.Slice.Pos.get {s : ByteString.Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : Char := + sorry +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def ByteString.Pos.toSlice {s : ByteString} (pos : s.Pos) : s.toSlice.Pos := + sorry +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def ByteString.Slice.Pos.next {s : ByteString.Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : s.Pos := + sorry +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def ByteString.Pos.get {s : ByteString} (pos : s.Pos) : Char := + pos.toSlice.get sorry +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def ByteString.Pos.next {s : ByteString} (pos : s.Pos) (h : True) : s.toSlice.Pos := + pos.toSlice.next sorry