From cb6c11686ef62c6badd4deeb5ffc33b68fdeba84 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 4 May 2026 23:01:55 +1000 Subject: [PATCH] fix: `withoutExporting` around diagnostic reporting 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 #13581. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Lean/Meta/Diagnostics.lean | 3 +++ src/Lean/Meta/Tactic/Simp/Diagnostics.lean | 3 +++ tests/elab/13581.lean | 15 +++++++++++++++ 3 files changed, 21 insertions(+) create mode 100644 tests/elab/13581.lean diff --git a/src/Lean/Meta/Diagnostics.lean b/src/Lean/Meta/Diagnostics.lean index 2cce90c99327..d1b9c832edb7 100644 --- a/src/Lean/Meta/Diagnostics.lean +++ b/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) diff --git a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean index ed0746a2811d..cfd3477548dd 100644 --- a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean +++ b/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 diff --git a/tests/elab/13581.lean b/tests/elab/13581.lean new file mode 100644 index 000000000000..5bfbcbd784cb --- /dev/null +++ b/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