From de99c8015a547bcd8baa91852970a2e15cda2abf Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Thu, 6 Feb 2025 14:11:53 +1100
Subject: [PATCH] feat: `#info_trees in` command (#6964)

This PR adds a convenience command `#info_trees in`, which prints the
info trees generated by the following command. It is useful for
debugging or learning about `InfoTree`.
---
 src/Init/Notation.lean         |  8 ++++
 src/Lean/Elab.lean             |  1 +
 src/Lean/Elab/InfoTrees.lean   | 25 ++++++++++++
 tests/lean/run/info_trees.lean | 69 ++++++++++++++++++++++++++++++++++
 4 files changed, 103 insertions(+)
 create mode 100644 src/Lean/Elab/InfoTrees.lean
 create mode 100644 tests/lean/run/info_trees.lean

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index debb6d14a3..e4fd0a02a3 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -749,6 +749,14 @@ The top-level command elaborator only runs the linters if `#guard_msgs` is not p
 syntax (name := guardMsgsCmd)
   (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
 
+/--
+Format and print the info trees for a given command.
+This is mostly useful for debugging info trees.
+-/
+syntax (name := infoTreesCmd)
+  "#info_trees" " in" ppLine command : command
+
+
 namespace Parser
 
 /--
diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 8f72567832..cd51cf18c6 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -55,3 +55,4 @@ import Lean.Elab.MatchExpr
 import Lean.Elab.Tactic.Doc
 import Lean.Elab.Time
 import Lean.Elab.RecommendedSpelling
+import Lean.Elab.InfoTrees
diff --git a/src/Lean/Elab/InfoTrees.lean b/src/Lean/Elab/InfoTrees.lean
new file mode 100644
index 0000000000..82c5128581
--- /dev/null
+++ b/src/Lean/Elab/InfoTrees.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.Elab.Command
+
+open Lean Elab Command
+
+namespace Lean.Elab.Tactic.InfoTrees
+
+@[builtin_command_elab infoTreesCmd, inherit_doc guardMsgsCmd]
+def elabInfoTrees : CommandElab
+  | `(command| #info_trees%$tk in $cmd) => do
+    if ! (← getInfoState).enabled then
+      logError "Info trees are disabled, can not use `#info_trees`."
+    else
+      elabCommand cmd
+      let infoTrees ← getInfoTrees
+      for t in infoTrees do
+        logInfoAt tk (← t.format)
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.InfoTrees
diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean
new file mode 100644
index 0000000000..b1b70ee236
--- /dev/null
+++ b/tests/lean/run/info_trees.lean
@@ -0,0 +1,69 @@
+-- This tests the `#info_trees in` command.
+-- If it proves too fragile to test the result using `#guard_msgs`,
+-- it is fine to simply remove the `#guard_msgs` and expected output.
+
+/--
+info: Try this: exact Nat.zero_le n
+---
+info: • command @ ⟨69, 0⟩-⟨69, 40⟩ @ Lean.Elab.Command.elabDeclaration
+  • Nat : Type @ ⟨69, 15⟩-⟨69, 18⟩ @ Lean.Elab.Term.elabIdent
+    • [.] Nat : some Sort.{?_uniq.1} @ ⟨69, 15⟩-⟨69, 18⟩
+    • Nat : Type @ ⟨69, 15⟩-⟨69, 18⟩
+  • n (isBinder := true) : Nat @ ⟨69, 11⟩-⟨69, 12⟩
+  • 0 ≤ n : Prop @ ⟨69, 22⟩-⟨69, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
+    • Macro expansion
+      0 ≤ n
+      ===>
+      binrel% LE.le✝ 0 n
+      • 0 ≤ n : Prop @ ⟨69, 22⟩†-⟨69, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
+        • 0 ≤ n : Prop @ ⟨69, 22⟩†-⟨69, 27⟩†
+          • [.] LE.le✝ : none @ ⟨69, 22⟩†-⟨69, 27⟩†
+          • 0 : Nat @ ⟨69, 22⟩-⟨69, 23⟩ @ Lean.Elab.Term.elabNumLit
+          • n : Nat @ ⟨69, 26⟩-⟨69, 27⟩ @ Lean.Elab.Term.elabIdent
+            • [.] n : none @ ⟨69, 26⟩-⟨69, 27⟩
+            • n : Nat @ ⟨69, 26⟩-⟨69, 27⟩
+  • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨69, 8⟩-⟨69, 9⟩
+  • n (isBinder := true) : Nat @ ⟨69, 11⟩-⟨69, 12⟩
+  • CustomInfo(Lean.Elab.Term.BodyInfo)
+    • Tactic @ ⟨69, 31⟩-⟨69, 40⟩
+      (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])))
+      before ⏎
+      n : Nat
+      ⊢ 0 ≤ n
+      after no goals
+      • Tactic @ ⟨69, 31⟩-⟨69, 33⟩
+        "by"
+        before ⏎
+        n : Nat
+        ⊢ 0 ≤ n
+        after no goals
+        • Tactic @ ⟨69, 34⟩-⟨69, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
+          (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))
+          before ⏎
+          n : Nat
+          ⊢ 0 ≤ n
+          after no goals
+          • Tactic @ ⟨69, 34⟩-⟨69, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
+            (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])
+            before ⏎
+            n : Nat
+            ⊢ 0 ≤ n
+            after no goals
+            • Tactic @ ⟨69, 34⟩-⟨69, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
+              (Tactic.exact? "exact?" [])
+              before ⏎
+              n : Nat
+              ⊢ 0 ≤ n
+              after no goals
+              • CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo)
+              • UserWidget Lean.Meta.Tactic.TryThis.tryThisWidget
+                {"suggestions": [{"suggestion": "exact Nat.zero_le n"}],
+                 "style": null,
+                 "range":
+                 {"start": {"line": 68, "character": 34}, "end": {"line": 68, "character": 40}},
+                 "isInline": true,
+                 "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨69, 8⟩-⟨69, 9⟩
+-/
+#guard_msgs in
+#info_trees in
+theorem t (n : Nat) : 0 ≤ n := by exact?