fix: keep abstract nested proofs procedure from hiding sorry warning (#10388)

This PR fixes a bug where definitions with nested proofs that contain
`sorry` might not report "warning: declaration uses 'sorry'" if the
proof has the same type as another nested proof from a previous
declaration. The bug only affected log messages; `#print axioms` would
still correctly report uses of `sorryAx`.

The fix is that now the abstract nested proofs procedure does not
consult the aux lemma cache if the proof contains a `sorry`.

Closes #10196

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. -/

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