timing information in instance synthesis

Stream: mathlib4

[Sébastien Gouëzel]

Can anyone remind me of the incantation to get timings for instance synthesis?

import Mathlib

set_option trace.Meta.synthInstance true in
--set_option trace.profiler true in
theorem ContinuousLinearMap.norm_smulRightL'
    {𝕜 E Fₗ : Type*} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜]
    [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) [Nontrivial Fₗ] :
    ‖(smulRightL 𝕜 E Fₗ) c‖ = ‖c‖ := by simp

shows the instance synthesis steps, but no timings. And If I uncomment the line set_option trace.profiler true I get timings, but I lose the instance synthesis steps.

[Kevin Buzzard]

Probably they're still there but just buried in a sea of other information and you have to start unfolding to find them.

buzzard@IC-HWDXTW69VR ~ % cd Lean/Projects/Mathlib
buzzard@IC-HWDXTW69VR Mathlib % cat > Mathlib/test2.lean
import Mathlib

set_option trace.Meta.synthInstance true in
set_option trace.profiler true in
theorem ContinuousLinearMap.norm_smulRightL'
    {𝕜 E Fₗ : Type*} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜]
    [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) [Nontrivial Fₗ] :
    ‖(smulRightL 𝕜 E Fₗ) c‖ = ‖c‖ := by simp
buzzard@IC-HWDXTW69VR Mathlib % lake build Mathlib/test2.lean > test2.out
buzzard@IC-HWDXTW69VR Mathlib % grep "\[Meta.synthInstance\]" test2.out
[very large amount of output suppressed]

Is this at all helpful?

[Sébastien Gouëzel]

Yes, definitely helpful! Grepping through a file like that which will be much more efficient than clicking on arrows in VSCode :-)

[Sébastien Gouëzel]

Thanks!

[Sébastien Gouëzel]

The trace is 1736 kB before my PR on Riemannian manifolds, and 1739 kB afterwards. And the timings are very much comparable. It doesn't look like a crazy exponential blow up (but still enough to make the simpNF linter reach a deterministic timeout)!