Tracking: explicit universes can improve performance substantially #12737
Labels
performance-hack
Something that improves performance but is poorly understood.
Comments
mattrobball
added
the
performance-hack
mathlib-bors bot
pushed a commit
that referenced
this issue
May 7, 2024
Testing for leanprover/lean4#4085 exposed possible regressions typeclass synthesis which can be ameliorated using explicit universes. We do this and we add references to the issue #12737 tracking these changes.
apnelson1
pushed a commit
that referenced
this issue
May 12, 2024
Testing for leanprover/lean4#4085 exposed possible regressions typeclass synthesis which can be ameliorated using explicit universes. We do this and we add references to the issue #12737 tracking these changes.
callesonne
pushed a commit
that referenced
this issue
May 16, 2024
Testing for leanprover/lean4#4085 exposed possible regressions typeclass synthesis which can be ameliorated using explicit universes. We do this and we add references to the issue #12737 tracking these changes.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
For
AlgebraicGeometry.Schemeand similar bundled categories, elaboration seems to inject level metavariables resulting more steps in unification. Providing explicit universe annotations,Scheme.{u}, prevents this.It would nice to understand what is happening.
The text was updated successfully, but these errors were encountered: