From 3a3c816a27c0bd454711e2f9e4e20cbbde47ba85 Mon Sep 17 00:00:00 2001 From: jrr6 <7482866+jrr6@users.noreply.github.com> Date: Wed, 30 Jul 2025 19:52:53 -0400 Subject: [PATCH] chore: break up universe level error message (#9637) This PR improves the readability of the "maximum universe level offset exceeded" error message. --- src/Lean/Elab/Level.lean | 4 +++- tests/lean/bigUnivOffsets.lean.expected.out | 8 ++++++-- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 5acc198755..8eb5b1fa72 100644 --- a/src/Lean/Elab/Level.lean +++ b/src/Lean/Elab/Level.lean @@ -56,7 +56,9 @@ register_builtin_option maxUniverseOffset : Nat := { private def checkUniverseOffset [Monad m] [MonadError m] [MonadOptions m] (n : Nat) : m Unit := do let max := maxUniverseOffset.get (← getOptions) unless n <= max do - throwError "maximum universe level offset threshold ({max}) has been reached, you can increase the limit using option `set_option maxUniverseOffset `, but you are probably misusing universe levels since offsets are usually small natural numbers" + throwError m!"Universe level offset `{n}` exceeds maximum offset `{max}`" + ++ .note m!"This code is probably misusing universe levels, since they are usually small natural numbers. \ + If you are confident this is not the case, you can increase the limit using `set_option maxUniverseOffset `" partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do let kind := stx.getKind diff --git a/tests/lean/bigUnivOffsets.lean.expected.out b/tests/lean/bigUnivOffsets.lean.expected.out index 1b0e2dd5e9..9bd74a9126 100644 --- a/tests/lean/bigUnivOffsets.lean.expected.out +++ b/tests/lean/bigUnivOffsets.lean.expected.out @@ -1,2 +1,6 @@ -bigUnivOffsets.lean:1:12-1:21: error: maximum universe level offset threshold (32) has been reached, you can increase the limit using option `set_option maxUniverseOffset `, but you are probably misusing universe levels since offsets are usually small natural numbers -bigUnivOffsets.lean:5:13-5:25: error: maximum universe level offset threshold (32) has been reached, you can increase the limit using option `set_option maxUniverseOffset `, but you are probably misusing universe levels since offsets are usually small natural numbers +bigUnivOffsets.lean:1:12-1:21: error: Universe level offset `100000000` exceeds maximum offset `32` + +Note: This code is probably misusing universe levels, since they are usually small natural numbers. If you are confident this is not the case, you can increase the limit using `set_option maxUniverseOffset ` +bigUnivOffsets.lean:5:13-5:25: error: Universe level offset `10000000` exceeds maximum offset `32` + +Note: This code is probably misusing universe levels, since they are usually small natural numbers. If you are confident this is not the case, you can increase the limit using `set_option maxUniverseOffset `