From 013e7b87ae05da82c62101544bacaecf1a1b3427 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sun, 19 May 2024 11:36:13 -0700
Subject: [PATCH] test failures on certain platforms, debugging

---
 tests/lean/run/KyleAlg.lean | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean
index 3d85ec40ea32..008c40ae6852 100644
--- a/tests/lean/run/KyleAlg.lean
+++ b/tests/lean/run/KyleAlg.lean
@@ -228,13 +228,15 @@ def test8 {G : Type _} [Group G]: Group (G × G × G × G × G × G × G × G) :
 
 namespace Lean
 
-unsafe def Expr.dagSizeUnsafe (e : Expr) : IO Nat := do
+unsafe def Expr.dagSizeUnsafe (e : Expr) (print : Bool := false) : IO Nat := do
   let (_, s) ← visit e |>.run ({}, 0)
   return s.2
 where
   visit (e : Expr) : StateRefT (HashSet USize × Nat) IO Unit := do
     let addr := ptrAddrUnsafe e
     unless (← get).1.contains addr do
+      if print then
+        println! "{addr}: {e}"
       modify fun (s, c) => (s.insert addr, c+1)
       match e with
       | Expr.proj _ _ s      => visit s
@@ -246,7 +248,7 @@ where
       | _ => return ()
 
 @[implemented_by Expr.dagSizeUnsafe]
-opaque Expr.dagSize (e : Expr) : IO Nat
+opaque Expr.dagSize (e : Expr) (print : Bool := false) : IO Nat
 
 def getDeclTypeValueDagSize (declName : Name) : CoreM Nat := do
   let info ← getConstInfo declName
@@ -283,11 +285,10 @@ def getDeclTypeValueDagSize (declName : Name) : CoreM Nat := do
 #guard_msgs in
 #eval getDeclTypeValueDagSize `test8
 
-def reduceAndGetDagSize (declName : Name) : MetaM Nat := do
+def reduceAndGetDagSize (declName : Name) (print : Bool := false) : MetaM Nat := do
   let c := mkConst declName [levelOne]
   let e ← Meta.reduce c
-  trace[Meta.debug] "{e}"
-  e.dagSize
+  e.dagSize print
 
 /-- info: 7 -/
 #guard_msgs in
@@ -305,10 +306,14 @@ def reduceAndGetDagSize (declName : Name) : MetaM Nat := do
 #guard_msgs in
 #eval reduceAndGetDagSize `test4
 
+#eval reduceAndGetDagSize `test4 (print := true)
+
 /-- info: 63 -/
 #guard_msgs in
 #eval reduceAndGetDagSize `test5
 
+#eval reduceAndGetDagSize `test5 (print := true)
+
 /-- info: 69 -/
 #guard_msgs in
 #eval reduceAndGetDagSize `test6