New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - fix(AlgebraicGeometry/GammaSpecAdjunction): speedup by adding universes #12469
Conversation
!bench |
Here are the benchmark results for commit 037b868. Benchmark Metric Change
======================================================================
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction instructions -54.2% |
@@ -460,7 +454,7 @@ theorem SpecΓIdentity_naturality {R S : CommRingCat} (f : R ⟶ S) : | |||
(Scheme.Spec.map f.op).1.c.app (op ⊤) ≫ SpecΓIdentity.hom.app _ = | |||
SpecΓIdentity.hom.app _ ≫ f := SpecΓIdentity.hom.naturality f | |||
|
|||
theorem SpecΓIdentity_hom_app_presheaf_obj {X : Scheme} (U : Opens X) : | |||
theorem SpecΓIdentity_hom_app_presheaf_obj {X : Scheme.{u}} (U : Opens X) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Probably this one is worth stressing. I don't change the proof at all; I just make the universe explicit, and according to the profiler the total time taken on my machine goes from 0.7 secs to 0.23.
bors p=5 |
bors merge |
…es (#12469) Add some explicit universe annotations because they cause a speedup (currently an unexplained phenomenon, unfortunately). Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Removes a porting note resolved by #12469; clarifies a porting note touched by it.
…es (#12469) Add some explicit universe annotations because they cause a speedup (currently an unexplained phenomenon, unfortunately). Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Removes a porting note resolved by #12469; clarifies a porting note touched by it.
…es (#12469) Add some explicit universe annotations because they cause a speedup (currently an unexplained phenomenon, unfortunately). Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Removes a porting note resolved by #12469; clarifies a porting note touched by it.
Add some explicit universe annotations because they cause a speedup (currently an unexplained phenomenon, unfortunately).
Ok so I don't really know what's going on here. The Zulip thread is here, with Ruben reporting that on recent nightlies the compilation time for this file had got worse, and it was already bad. When doing some experiments I added some explicit universe annotations (not because I thought they would help -- it was literally just to make a diff smaller) and one declaration just magically got much much faster. So I put
set_option maxHeartbeats 20000
(note: not 200000) at the top of the file, a couple more declarations broke, and I added explicit universe annotations in all of them and they all got fixed. It would be good to get some kind of explanation of what's going on here because the universe unification problem looks to me like it should be trivial: there is only one universe at play in this file and the answer to all the universe unifications questions I saw was "set?u.12345 = ?u.54321
".In
comp_ring_hom_ext
I guess there was a possibility that Lean was ultimately deciding that both universes should be equal but taking some time over it, and now we just tell it to assume this (note that the change doesn't change the type of the declaration).