Zulip Chat Archive

Stream: mathlib4

Topic: Slow SecondCountableEither


Patrick Massot (Aug 31 2023 at 18:42):

Some performance issue both people who like to debug those:

import Mathlib.MeasureTheory.Measure.Haar.OfBasis

variable
  {E : Type*} [NormedAddCommGroup E] [NormedSpace  E]
  {H : Type*} [NormedAddCommGroup H] [NormedSpace  H] [FiniteDimensional  H]


--set_option synthInstance.maxHeartbeats 100000
set_option trace.Meta.synthInstance.instances true in
example : SecondCountableTopologyEither  (H L[] E) := by
  infer_instance

Patrick Massot (Aug 31 2023 at 18:42):

(from the sphere eversion ongoing port)

Matthew Ballard (Aug 31 2023 at 18:47):

22000 suffices on the toolchain from lean4#2478 but infer_instance is doing tons of work there

Matthew Ballard (Aug 31 2023 at 19:09):

Does

attribute [-instance] FiniteDimensional.complexToReal

suffice on your toolchain?

Patrick Massot (Aug 31 2023 at 19:17):

Yes

Yury G. Kudryashov (Aug 31 2023 at 20:21):

Why do you need FiniteDimensional at all?

Yury G. Kudryashov (Aug 31 2023 at 20:21):

Does it try the second space first?


Last updated: Dec 20 2023 at 11:08 UTC