Zulip Chat Archive

Stream: general

Topic: Slow type-class search


Gabriel Ebner (Jun 15 2020 at 12:46):

This takes more than three seconds on my machine:

import all
set_option profiler true
example {α : Type*} {β : Type*} : has_add (α  β) :=
by apply_instance

Any idea what's going on here? (Also filed as issue #3080)

Sebastien Gouezel (Jun 15 2020 at 12:52):

Is this really surprising? When it succeeds because there is a ring or whatever around, it can be pretty quick, but when it fails it has to try every possible instance, even those that have low priority. And there are many many many ways in mathlib to have a has_add instance.

Gabriel Ebner (Jun 15 2020 at 14:52):

Good point. Then we'll have to fix this in core. lean#332 reduces the example to 83ms.

Sebastien Gouezel (Jun 15 2020 at 14:57):

Gabriel, you're still going to shave off 30 minutes on compilation time :)

Johan Commelin (Jun 15 2020 at 15:00):

This is really crazy... I'm amazed by all these fixes that keep improving the system.


Last updated: Dec 20 2023 at 11:08 UTC