From 21f5263f2f28e5fd7b6a99c40f0c11351f04aedb Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 21 Aug 2025 14:12:21 +1000
Subject: [PATCH] feat: minor quality of life improvements in
 script/AnalyzeGrindAnnotations (#10021)

This PR make some minor changes to the grind annotation analysis script,
including sorting results and handling errors. Still need to add an
external UI.
---
 script/AnalyzeGrindAnnotations.lean | 26 ++++++++++++++++++++------
 1 file changed, 20 insertions(+), 6 deletions(-)

diff --git a/script/AnalyzeGrindAnnotations.lean b/script/AnalyzeGrindAnnotations.lean
index b1a92ad97e..4e38439450 100644
--- a/script/AnalyzeGrindAnnotations.lean
+++ b/script/AnalyzeGrindAnnotations.lean
@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 import Lean
 
 namespace Lean.Meta.Grind.Analyzer
+
+
 /-!
 A simple E-matching annotation analyzer.
 For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
@@ -72,16 +74,28 @@ def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
   if s > c.detailed then
     logInfo m!"{declName}\n{← thmsToMessageData thms}"
 
+-- Not sure why this is failing: `down_pure` perhaps has an unnecessary universe parameter?
+run_meta analyzeEMatchTheorem ``Std.Do.SPred.down_pure {}
+
 /-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
 def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
   let origins := (← getEMatchTheorems).getOrigins
-  for o in origins do
-    let .decl declName := o | pure ()
-    analyzeEMatchTheorem declName c
+  let decls := origins.filterMap fun | .decl declName => some declName | _ => none
+  for declName in decls.mergeSort Name.lt do
+    try
+      analyzeEMatchTheorem declName c
+    catch e =>
+      logError m!"{declName} failed with {e.toMessageData}"
+  logInfo m!"Finished analyzing {decls.length} theorems"
 
-set_option maxHeartbeats 5000000
-run_meta analyzeEMatchTheorems
+/-- Macro for analyzing E-match theorems with unlimited heartbeats -/
+macro "#analyzeEMatchTheorems" : command => `(
+  set_option maxHeartbeats 0 in
+  run_meta analyzeEMatchTheorems
+)
 
--- We can analyze specific theorems using commands such as
+#analyzeEMatchTheorems
+
+-- -- We can analyze specific theorems using commands such as
 set_option trace.grind.ematch.instance true in
 run_meta analyzeEMatchTheorem ``List.filterMap_some {}