From 71b5bf3ef62c6414d4eab046a6e8d1f669e221f0 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sat, 12 Jul 2025 19:24:00 -0700 Subject: [PATCH] fix: include `._closed` decls in trace.Compiler.result output (#9336) This PR changes the implementation of `trace.Compiler.result` to use the decls as they are provided rather than looking them up in the LCNF mono environment extension, which was seemingly done to save the trouble of re-normalizing fvar IDs before printing the decl. This means that the `._closed` decls created by the `extractClosed` pass will now be included in the output, which was definitely confusing before if you didn't know what was happening. --- src/Lean/Compiler/LCNF/Main.lean | 5 ++--- tests/lean/reduceArity.lean.expected.out | 2 +- tests/lean/run/emptyLcnf.lean | 8 +++---- tests/lean/run/erased.lean | 10 ++++----- tests/lean/unhygienicCode.lean.expected.out | 24 ++++++++++----------- 5 files changed, 24 insertions(+), 25 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 75680b6cd2..650d41a4b0 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -105,9 +105,8 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck) if (← Lean.isTracingEnabledFor `Compiler.result) then for decl in decls do - -- We display the declaration saved in the environment because the names have been normalized - let some decl' ← getDeclAt? decl.name .mono | unreachable! - Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl'}" + let decl ← normalizeFVarIds decl + Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}" let irDecls ← IR.toIR decls IR.compile irDecls diff --git a/tests/lean/reduceArity.lean.expected.out b/tests/lean/reduceArity.lean.expected.out index 9320b2fd49..e158d9598b 100644 --- a/tests/lean/reduceArity.lean.expected.out +++ b/tests/lean/reduceArity.lean.expected.out @@ -21,7 +21,7 @@ return _x.1 [Compiler.result] size: 4 def h (n : Nat) (a : Nat) : Nat := - let _x.1 := double; + let _x.1 := h._closed_0; let _x.2 := g._redArg n a _x.1; let _x.3 := g._redArg a n _x.1; let _x.4 := Nat.add _x.2 _x.3; diff --git a/tests/lean/run/emptyLcnf.lean b/tests/lean/run/emptyLcnf.lean index 5c024247ee..ee3adf70af 100644 --- a/tests/lean/run/emptyLcnf.lean +++ b/tests/lean/run/emptyLcnf.lean @@ -42,11 +42,11 @@ trace: [Compiler.result] size: 5 return _x.3 [Compiler.result] size: 8 def _eval a.1 a.2 a.3 : EStateM.Result Lean.Exception PUnit PUnit := - let _x.4 := "f"; - let _x.5 := Lean.Name.mkStr1 _x.4; + let _x.4 := _eval._closed_0; + let _x.5 := _eval._closed_1; let _x.6 := 1; - let _x.7 := Array.mkEmpty ◾ _x.6; - let _x.8 := Array.push ◾ _x.7 _x.5; + let _x.7 := _eval._closed_2; + let _x.8 := _eval._closed_3; let _x.9 := PUnit.unit; let _f.10 := _eval._lam_0 _x.8 _x.9; let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3; diff --git a/tests/lean/run/erased.lean b/tests/lean/run/erased.lean index 4debf52771..165643d7cc 100644 --- a/tests/lean/run/erased.lean +++ b/tests/lean/run/erased.lean @@ -64,12 +64,12 @@ trace: [Compiler.result] size: 5 [Compiler.result] size: 9 def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : PUnit) : EStateM.Result Lean.Exception PUnit PUnit := - let _x.4 : String := "Erased"; - let _x.5 : String := "mk"; - let _x.6 : Lean.Name := Lean.Name.mkStr2 _x.4 _x.5; + let _x.4 : String := _eval._closed_0; + let _x.5 : String := _eval._closed_1; + let _x.6 : Lean.Name := _eval._closed_2; let _x.7 : Nat := 1; - let _x.8 : Array Lean.Name := Array.mkEmpty ◾ _x.7; - let _x.9 : Array Lean.Name := Array.push ◾ _x.8 _x.6; + let _x.8 : Array Lean.Name := _eval._closed_3; + let _x.9 : Array Lean.Name := _eval._closed_4; let _x.10 : PUnit := PUnit.unit; let _f.11 : Lean.Elab.Term.Context → lcAny → diff --git a/tests/lean/unhygienicCode.lean.expected.out b/tests/lean/unhygienicCode.lean.expected.out index ebaeed5c89..8304bcd105 100644 --- a/tests/lean/unhygienicCode.lean.expected.out +++ b/tests/lean/unhygienicCode.lean.expected.out @@ -66,19 +66,19 @@ let _x.1 := Syntax.missing; let _x.2 := 1; let _x.3 := false; - let _x.4 := @SourceInfo.fromRef _x.1 _x.3; - let _x.5 := "UnhygienicMain"; - let _x.6 := Name.mkStr1 _x.5; - let _x.7 := "term_+_"; - let _x.8 := Name.mkStr1 _x.7; - let _x.9 := "a"; - let _x.10 := String.toSubstring' _x.9; - let _x.11 := Name.mkStr1 _x.9; - let _x.12 := addMacroScope _x.6 _x.11 _x.2; + let _x.4 := foo._closed_0; + let _x.5 := foo._closed_1; + let _x.6 := foo._closed_2; + let _x.7 := foo._closed_3; + let _x.8 := foo._closed_4; + let _x.9 := foo._closed_5; + let _x.10 := foo._closed_6; + let _x.11 := foo._closed_7; + let _x.12 := foo._closed_8; let _x.13 := [] _; - let _x.14 := Syntax.ident _x.4 _x.10 _x.12 _x.13; - let _x.15 := "+"; - let _x.16 := Syntax.atom _x.4 _x.15; + let _x.14 := foo._closed_9; + let _x.15 := foo._closed_10; + let _x.16 := foo._closed_11; let _x.17 := Nat.reprFast n; let _x.18 := SourceInfo.none; let _x.19 := @Syntax.mkNumLit _x.17 _x.18;