fix: withoutExporting around diagnostic reporting (#13630)

This PR fixes an "Unknown constant" error when `set_option diagnostics
true` is enabled in module mode under a `public section`. Diagnostic
output may reference private declarations such as `_match_*` and
`_sparseCasesOn_*` that are recorded in unfold counters; constructing
the message previously failed because the environment was in exporting
mode and could not resolve those names. The diagnostic-printing paths in
`Lean.Meta.Diagnostics.reportDiag` and
`Lean.Meta.Tactic.Simp.Diagnostics.reportDiag` now run under
`withoutExporting`.

Closes https://github.com/leanprover/lean4/issues/13581.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/Lean/Meta/Diagnostics.lean

@@ -85,6 +85,9 @@ def appendSection (m : Array MessageData) (cls : Name) (header : String) (s : Di
 /-- Logs diagnostics and resets the counters -/
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
+    -- Diagnostic output may reference private declarations (e.g. `_match_*`,
+    -- `_sparseCasesOn_*`) that are not visible in exporting mode (issue #13581).
+    withoutExporting do
     let unfoldCounter := (← get).diag.unfoldCounter
     let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
     let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)

src/Lean/Meta/Tactic/Simp/Diagnostics.lean

@@ -67,6 +67,9 @@ def mkDiagMessages (diag : Simp.Diagnostics) : MetaM (Array MessageData) := do
 
 def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
+    -- Diagnostic output may reference private declarations that are not visible
+    -- in exporting mode (issue #13581).
+    withoutExporting do
     let m ← mkDiagMessages diag
     unless m.isEmpty do
       logInfo <| .trace { cls := `simp, collapsed := false } "Diagnostics" m

tests/elab/13581.lean

@@ -0,0 +1,15 @@
+-- https://github.com/leanprover/lean4/issues/13581
+-- Reporting `diagnostics` must not crash on private match/sparseCasesOn helpers
+-- in module mode under a `public section`.
+module
+
+public section
+
+def onlyTrue : Bool → Bool
+  | true => true
+  | x    => x
+
+#guard_msgs (drop trace) in
+set_option diagnostics true in
+set_option diagnostics.threshold 0 in
+example : onlyTrue true = true := rfl