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