From ed0c59bdb5b01d76fc2012ee85c19ea308f66e3d Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 22 Nov 2024 16:11:38 -0800 Subject: [PATCH] fix: make sure `#check id` heeds `pp.raw` This PR fixes a bug where the signature pretty printer would ignore the current setting of `pp.raw`. This fixes an issue where `#check ident` would not heed `pp.raw`. Closes #6090. --- src/Lean/PrettyPrinter.lean | 12 ++++++++---- tests/lean/root.lean.expected.out | 2 +- tests/lean/run/6090.lean | 30 ++++++++++++++++++++++++++++++ 3 files changed, 39 insertions(+), 5 deletions(-) create mode 100644 tests/lean/run/6090.lean diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 4d0500c854e1..33631da5e4d9 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/src/Lean/PrettyPrinter.lean @@ -90,10 +90,14 @@ def ppModule (stx : TSyntax ``Parser.Module.module) : CoreM Format := do open Delaborator in /-- Pretty-prints a declaration `c` as `c.{} : `. -/ def ppSignature (c : Name) : MetaM FormatWithInfos := do - let decl ← getConstInfo c - let e := .const c (decl.levelParams.map mkLevelParam) - let (stx, infos) ← delabCore e (delab := delabConstWithSignature) - return ⟨← ppTerm ⟨stx⟩, infos⟩ -- HACK: not a term + if pp.raw.get (← getOptions) then + let info ← getConstInfo c + return s!"{mkConst c (info.levelParams.map mkLevelParam)} : {info.type}" + else + let decl ← getConstInfo c + let e := .const c (decl.levelParams.map mkLevelParam) + let (stx, infos) ← delabCore e (delab := delabConstWithSignature) + return ⟨← ppTerm ⟨stx⟩, infos⟩ -- HACK: not a term private partial def noContext : MessageData → MessageData | MessageData.withContext _ msg => noContext msg diff --git a/tests/lean/root.lean.expected.out b/tests/lean/root.lean.expected.out index 4f298108b409..7eac01396cdb 100644 --- a/tests/lean/root.lean.expected.out +++ b/tests/lean/root.lean.expected.out @@ -7,7 +7,7 @@ root.lean:35:14-35:22: error: protected declarations must be in a namespace root.lean:41:7-41:8: error: unknown identifier 'h' root.lean:43:7-43:8: error: unknown identifier 'f' Bla.f (x : Nat) : Nat -prv (x : Nat) : Nat +_private.root.0.prv : Nat -> Nat root.lean:90:89-90:93: error: unsolved goals x : Nat ⊢ isEven (x + 1 + 1) = isEven x diff --git a/tests/lean/run/6090.lean b/tests/lean/run/6090.lean new file mode 100644 index 000000000000..f4312077572e --- /dev/null +++ b/tests/lean/run/6090.lean @@ -0,0 +1,30 @@ +/-! +# Make sure `#check` heeds `pp.raw` +https://github.com/leanprover/lean4/issues/6090 +-/ + +section +/-- info: id.{u} {α : Sort u} (a : α) : α -/ +#guard_msgs in #check id +/-- info: @id : {α : Sort u_1} → α → α -/ +#guard_msgs in #check @id +-- '#print' was unaffected, but throw in a test anyway. +/-- +info: def id.{u} : {α : Sort u} → α → α := +fun {α} a => a +-/ +#guard_msgs in #print id + +set_option pp.raw true + +/-- info: id.{u} : forall {α : Sort.{u}}, α -> α -/ +#guard_msgs in #check id +/-- info: id.{u_1} : forall {α : Sort.{u_1}}, α -> α -/ +#guard_msgs in #check @id +-- '#print' was unaffected, but throw in a test anyway. +/-- +info: def id.{u} : forall {α : Sort.{u}}, α -> α := +fun {α : Sort.{u}} (a : α) => a +-/ +#guard_msgs in #print id +end