chore: reenable Lake

.

disable printing expressions

src/Lean/Meta/Basic.lean

@@ -1894,7 +1894,14 @@ def isExprDefEq (t s : Expr) : MetaM Bool :=
     Remark: the kernel does *not* update the type of variables in the local context.
     -/
     resetDefEqPermCaches
-    checkpointDefEq (mayPostpone := true) <| Meta.isExprDefEqAux t s
+    let start ← IO.getNumHeartbeats
+    let r ← checkpointDefEq (mayPostpone := true) <| Meta.isExprDefEqAux t s
+    if profiler.isDefEq.get (← getOptions) then
+      let finish ← IO.getNumHeartbeats
+      let elapsed := (finish - start) / 1000
+      if elapsed ≥ profiler.isDefEq.threshold.get (← getOptions) then
+        logInfo s!"isDefEq took {elapsed} heartbeats"
+    return r
 
 /--
   Determines whether two expressions are definitionally equal to each other.

src/Lean/Util/Profile.lean

@@ -13,7 +13,7 @@ register_builtin_option profiler : Bool := {
   defValue := false
   group    := "profiler"
   descr    := "show exclusive execution times of various Lean components
-  
+
 See also `trace.profiler` for an alternative profiling system with structured output."
 }
 
@@ -23,6 +23,16 @@ register_builtin_option profiler.threshold : Nat := {
   descr    := "threshold in milliseconds, profiling times under threshold will not be reported individually"
 }
 
+register_builtin_option profiler.isDefEq : Bool := {
+  defValue := false
+  descr    := "Report slow isDefEq problems"
+}
+
+register_builtin_option profiler.isDefEq.threshold : Nat := {
+  defValue := 200000
+  descr    := "Threshold for reporting isDefEq heartbeats"
+}
+
 @[export lean_get_profiler]
 private def get_profiler (o : Options) : Bool :=
   profiler.get o