`#time` and `trace.profiler` miss nearly all of the time spent in some files

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Consider these three files: test_30.tar.gz

One of them is test_30_time.lean:

import Std.Tactic
section Test

variable {α : Type}

variable (f : α → α) (g : α → α) (h : α → α → α)
variable (a b c : α)
#time
variable (eq_haa_a : ∀ x y : α, (h x y) = c)

set_option maxRecDepth 150000 in
#time
example : (((h (((h (((h (((h (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))) (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))))) (((h (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))) (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))))))) (((h (((h (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))) (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))))) (((h (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))) (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))))))))) (((h (((h (((h (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))) (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))))) (((h (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))) (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))))))) (((h (((h (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))) (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))))) (((h (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))))) (((h (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))))) (((h (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))))) (((h (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))))) (((h (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))))) (((h (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a)))))) (((h (((h ((h a) a)) ((h a) a)))) (((h ((h a) a)) ((h a) a))))))))))))))))))))))) = (c) := by
  sorry
#time
end Test

The others are similar but using headers like
test_30_profile.lean:

import Std.Tactic
set_option maxRecDepth 150000
set_option trace.profiler true
set_option trace.profiler.threshold 0
set_option trace.Elab.command true

And
test_30_noprofile.lean:

import Std.Tactic
set_option maxRecDepth 150000

Using Lean (version 4.18.0, arm64-apple-darwin23.6.0, commit 11ccbced7964, Release) (though Lean nightly seems to show roughly similar behavior), running

for i in test_30_time test_30_profile test_30_noprofile; do echo $i; time lean $i.lean > $i.log; done

gives

test_30_time
lean $i.lean > $i.log  32.43s user 2.34s system 95% cpu 36.581 total
test_30_profile
lean $i.lean > $i.log  32.61s user 2.27s system 94% cpu 36.727 total
test_30_noprofile
lean $i.lean > $i.log  32.63s user 2.29s system 94% cpu 36.809 total

and the logs show:
for time:

time: 2ms
test_30_time.lean:13:0: warning: declaration uses 'sorry'
time: 293ms
time: 0ms

for profile:

cat test_30_profile.log |  grep '^\[' | grep -o '\[[0-9][^]]*\]' | grep -o '[0-9\.]*' | awk '{s+=$1} END {print s}'

gives 0.354223 (test_30_profile.log)
(this was from a slightly earlier run, so the numbers are a bit off from those in the .tar.gz, but not by much)

Where is all the missing time being spent?

Context

#lean4 > trace profiler is missing more than 99% of the time

Steps to Reproduce

See above

Expected behavior: #time and profiler output should add up to overall running time of the file minus any overhead from profiling

Actual behavior: only about 200ms of about 30s--60s is accounted for.

Versions

Lean 4.18.0
Target: arm64-apple-darwin23.6.0 macOS

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Unpack test_30.tar.gz and begin with test_30_time.lean, reproducing the discrepancy with #time and trace.profiler. Trace where those entry points collect timing data; done means the reported timings include the time spent in the affected files.