Zulip Chat Archive
Stream: general
Topic: Timeout
Yaël Dillies (Aug 14 2021 at 06:17):
#8644 just got a random timeout in category_theory.grothendieck. Don't know what you can do with that, but I thought I should tell you.
Yaël Dillies (Oct 06 2021 at 06:32):
Random timeout in linear_algebra.quadratic_form if people want to speed it up.
Johan Commelin (Oct 06 2021 at 06:33):
Is this not fixed by yesterdays
rss-bot said:
chore(linear_algebra/quadratic_form): speed up quadratic_form.lin_mul…
chore(linear_algebra/quadratic_form): speed up quadratic_form.lin_mul_lin (#9567)In my single profiler run, this reduced elaboration time from 20s to 1.5s.
https://github.com/leanprover-community/mathlib/commit/7455f47c7037681073655ff0716f7ce09b766c2a
Scott Morrison (Oct 06 2021 at 06:35):
I think we just need a bunch of people to merge master.
Yaël Dillies (Oct 06 2021 at 06:47):
Oh! Thank you for the pointer, will merge.
Yaël Dillies (Feb 22 2022 at 09:26):
@Oliver Nash I just hit a timeout in algebra.lie.engel.
Oliver Nash (Feb 22 2022 at 09:26):
I'll take a look now.
Yaël Dillies (Feb 22 2022 at 09:27):
Thanks!
Oliver Nash (Feb 22 2022 at 09:30):
It's branch#sup_bot_hom, right?
Oliver Nash (Feb 22 2022 at 09:33):
I cannot reproduce this locally with my timeout set to 100000.
Oliver Nash (Feb 22 2022 at 09:34):
I've literally just checked out branch#sup_bot_hom, grabbed a cache, and tried in VS Code and also lean --make src/algebra/lie/engel.lean at the command line and they both work fine.
Oliver Nash (Feb 22 2022 at 09:35):
I'll look for a way to speed up that proof anyway but I'd like to understand why I cannot reproduce this.
Anne Baanen (Feb 22 2022 at 09:42):
#12193 is also hitting a timeout that seems unrelated in geometry/euclidean/oriented_angle.lean:638
Anne Baanen (Feb 22 2022 at 09:43):
The code suggests at a first glance it is related to Yaël's timeout:
@[simp] lemma oangle_conj_lie (x y : V) :
hb.oangle (hb.conj_lie x) (hb.conj_lie y) = -hb.oangle x y :=
by simp [conj_lie, oangle, ←(star_ring_end ℂ).map_div]
Oliver Nash (Feb 22 2022 at 09:44):
Ha, I think the lie there is short for "Linear Isometric Equivalence" and nothing to do with the famous Norwegian!
Oliver Nash (Feb 22 2022 at 09:59):
This makes some improvement anyway: #12205
Yaël Dillies (Feb 22 2022 at 10:16):
I couldn't reproduce it locally either :sad:
Yaël Dillies (Feb 22 2022 at 10:16):
The timeout in oriented_angle has been fixed yesterday by Rob.
Yaël Dillies (Apr 09 2022 at 21:33):
#13242 is hitting a (definitely unrelated) timeout in category_theory.fin_category. Anyone to issue a speedup?
Yaël Dillies (Apr 09 2022 at 21:46):
Update: #13194 and #13197 too :scream:
Yaël Dillies (Apr 09 2022 at 22:11):
@Andrew Yang, you're the one to gitblame.
Moritz Doll (Apr 09 2022 at 22:12):
Bors seems to have to different issues: the category_theory.fin_category and name collisions in topology/algebra/group for filter.inv_mem_inv and set.inv_mem_inv.
Yaël Dillies (Apr 09 2022 at 22:13):
Argh, those latter ones are mine. I did fix everything as it came but it's an uphill battle.
Yaël Dillies (Apr 09 2022 at 22:14):
Can a @maintainers pull #13170 off the queue then?
Yaël Dillies (Apr 09 2022 at 22:14):
I will merge master tomorrow when #bors is less busy
Arthur Paulino (Apr 09 2022 at 22:27):
Does bors cancel work? Or is it reserved for maintainers?
Yaël Dillies (Apr 10 2022 at 09:49):
docs#category_theory.fin_category.obj_as_type_equiv_as_type takes 41s to compile locally. I'm taking a stab at making it faster.
Yaël Dillies (Apr 10 2022 at 10:30):
Moritz Doll (Apr 10 2022 at 15:49):
Bors still has some timeout issues and again category theory is to blame, but this time it is docs#category_theory.groupoid_of_elements and it seems that #13125 is failing repeatedly
Bryan Gin-ge Chen (Apr 10 2022 at 19:08):
Looks like batches are now also timing out on docs#measure_theory.measure.finite_spanning_sets_in.prod : https://github.com/leanprover-community/mathlib/runs/5962695533?check_suite_focus=true https://github.com/leanprover-community/mathlib/runs/5963011819?check_suite_focus=true
Yaël Dillies (Apr 10 2022 at 19:09):
Is my speedup timing out on those? :confused:
Bryan Gin-ge Chen (Apr 10 2022 at 19:10):
It seems so, unfortunately.
Yaël Dillies (Apr 10 2022 at 19:11):
Do you want me to fix them in #13298 then?
Bryan Gin-ge Chen (Apr 10 2022 at 19:16):
Having separate PRs for each fix would be cleaner, but I won't insist. (I have to go AFK for a bit, so if fix(es) appear, hopefully another maintainer can put them on the top of the queue with bors r+ p=1000 .)
Yaël Dillies (Apr 10 2022 at 19:17):
Yes, but doesn't that risk bors not batching them together?
Yaël Dillies (Apr 10 2022 at 22:59):
This is really puzzling. finite_spanning_sets_in (μ.prod ν) alone takes 10-20s to compile. No matter how many type coercions or explicit instances I put in, it still takes as long.
Alex J. Best (Apr 10 2022 at 23:04):
What about adding explicit universes?
Yaël Dillies (Apr 10 2022 at 23:05):
Oh I didn't try! I'm onto fixing docs#category_theory.groupoid_of_elements now
Yaël Dillies (Apr 10 2022 at 23:08):
Oh miracle! #13298 did go through in the end
Kyle Miller (Apr 10 2022 at 23:11):
Yaël Dillies said:
This is really puzzling.
finite_spanning_sets_in (μ.prod ν)alone takes 10-20s to compile. No matter how many type coercions or explicit instances I put in, it still takes as long.
Is this the definition of finite_spanning_sets_in.prod that you're looking at? I'm curious: what does putting noncomputable! out front do to compilation time? (It seems to be significantly faster on my computer, but I'm not completely sure...)
Yaël Dillies (Apr 10 2022 at 23:16):
Oh wow you are right on spot, Kyle. Went down from 20s to milliseconds using noncomputable!.
Yaël Dillies (Apr 10 2022 at 23:17):
Does noncomputable! apply hereditarily or do we need to mark noncomputable stuff that uses noncomputable! stuff?
Kyle Miller (Apr 10 2022 at 23:18):
Over those 20s, the compiler's spending a whole lot of time calculating that it basically doesn't need to calculate anything. (The structure it constructs has no computationally relevant fields.)
Kyle Miller (Apr 10 2022 at 23:19):
Since this module is using noncomputable theory, what will happen is that every definition in this file that uses this one will be noncomputable automatically (as necessary).
Yaël Dillies (Apr 10 2022 at 23:22):
Kyle Miller (Apr 10 2022 at 23:23):
By the way, this is what the compiler compiles it down to:
[compiler.optimize_bytecode] measure_theory.measure.finite_spanning_sets_in.prod 10
0: scnstr #0
1: ret
That means "create a value using constructor number 0 (with no arguments) and return it."
Yaël Dillies (Apr 10 2022 at 23:24):
Heading off for today. I will leave docs#category_theory.groupoid_of_elements now for someone else to fix.
Kevin Buzzard (Apr 10 2022 at 23:24):
Thanks so much Yael!
Yaël Dillies (Apr 10 2022 at 23:25):
Seeing bors failing hurts!
Kevin Buzzard (Apr 10 2022 at 23:26):
I need to add noncomputable! to my list of things to try when something takes an absurdly long amount of time
Yaël Dillies (Apr 11 2022 at 22:35):
@maintainers (sorry, I have been pinging you a lot this week end :grinning:), could #13372 be merged quickly?
Yaël Dillies (Apr 12 2022 at 08:40):
Could someone put #13170 back on the queue now that it's quieter?
Johan Commelin (Apr 12 2022 at 08:53):
done
Yaël Dillies (Apr 12 2022 at 10:42):
Yet another timeout in category_theory.preadditive.biproducts :rolling_eyes:
Yaël Dillies (Apr 12 2022 at 10:42):
Is this how mathlib is gonna die? crippled by category theory timeouts?
Johan Commelin (Apr 12 2022 at 10:47):
Ouch...
Mauricio Collares (Apr 12 2022 at 10:48):
Assuming timeouts are deterministic, it would be great to have a table of how many heartbeats each def/lemma takes at the moment so people can work on optimizing them before disaster strikes.
Yaël Dillies (Apr 12 2022 at 10:49):
"Deterministic" timeouts are unfortunately rarely deterministic...
Yaël Dillies (Apr 12 2022 at 10:51):
docs#category_theory.biprod.column_nonzero_of_iso indeed takes a whopping 76s to elaborate.
Yaël Dillies (Apr 12 2022 at 10:56):
#13383. Once again it's a decidability issue.
Yaël Dillies (Apr 12 2022 at 10:58):
We're also exceeding the API rate :sad:
Kevin Buzzard (Apr 12 2022 at 11:04):
by_contradiction is a huge gotcha. I often just stick classical in front of it before using it.
Yaël Dillies (Apr 12 2022 at 11:05):
by_contra' avoids the decidability check entirely, right?
Kevin Buzzard (Apr 12 2022 at 11:08):
If the proof now takes 2 seconds instead of 76 then it must be doing _something_ differently but I don't know what.
Yaël Dillies (May 01 2022 at 22:16):
I'm hitting a timeout with docs#AffineScheme.Spec (38.5s of decl post-processing) and I don't know how to fix it. Could anyone take a look? Is decl post-processing the attribute applications? Spec is tagged with @[derive [full, faithful, ess_surj], simps].
Yaël Dillies (May 01 2022 at 22:16):
cc @Andrew Yang
Yaël Dillies (May 01 2022 at 22:18):
Okay it's clearly simps going mad.
Yaël Dillies (May 01 2022 at 22:27):
Floris van Doorn (May 02 2022 at 11:42):
Note that @[simps] calls simp on the right-hand side in the case that the right-hand side is not a construction application (to figure out what the definition should reduce to). In cases where simp is slow, this means that adding the @[simps] attribute is also slow.
Yaël Dillies (May 02 2022 at 11:51):
I'm wondering how much compile time goes into those slow declarations. If each of them takes 30s, it would add up quick...
Floris van Doorn (May 02 2022 at 12:01):
Yeah, that might be worth investigating. @[simps] should not be automatically added to all declarations that are not constructor applications, since I think that in many cases you won't use those simp lemmas much.
Last updated: Dec 20 2023 at 11:08 UTC