test failures on certain platforms, debugging

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