PR summary 4466755c92

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

./scripts/technical-debt-metrics.sh pr_summary

!bench

Here are the benchmark results for commit dbb8c6d.
There were significant changes against commit efeadfb:

  Benchmark                                   Metric         Change
  =================================================================
+ ~Mathlib.RingTheory.Kaehler.JacobiZariski   instructions   -29.0%

🚀 Pull request has been placed on the maintainer queue by grunweg.

Wow, these are great speed-ups! These should definitely land soon.

Do you understand why this changes performance? If so, it would be good to document (and look for other instances in mathlib/perhaps even write a linter). If not, can you start a discussion on zulip?

I'll be bold nominate for a quick merge, mostly to get the ball rolling. maintainer delegate?

You probably missed the discussion at https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321099.20use.20unification.20hints.20for.20generators.

So @mattrobball and @erdOne should have a look first.

I think changing the convention for naming universes in this file is not a good idea. I am pretty sure that the kernel is able to check equality of levels from the names directly and that is what allows it avoid many unfolding steps. I am less sure about the importance of the ordering.

I think changing the convention for naming universes in this file is not a good idea. I am pretty sure that the kernel is able to check equality of levels from the names directly and that is what allows it avoid many unfolding steps. I am less sure about the importance of the ordering.

It definitely matters that the universes of R, S and T appear before the universes of P, Q, etc. alphabetically, just replace a, b and c by x, y and z respectively and many declarations even start to timeout with maxHeartbeats reached.

I should be clear since there are two possible orderings: 1. declaration ordering (ie what line number/column does a level appear) and 2. orderings on the names via the usual lexicographical ordering on strings.

The former doesn't seem to matter. The latter seems to matter both for the elaborator and the kernel. Lexical ordering gives equality in the kernel.

I should be clear since there are two possible orderings: 1. declaration ordering (ie what line number/column does a level appear) and 2. orderings on the names via the usual lexicographical ordering on strings.

The former doesn't seem to matter. The latter seems to matter both for the elaborator and the kernel. Lexical ordering gives equality in the kernel.

So what exactly do you suggest to change in this PR?

I think it is possible to preserve the alphabetical order while having universe names adhering to the naming convention.
And I'm guessing that is what Matthew is also suggesting?

Aha, thanks for the clarification, changed it accordingly.

!bench

Is there an open issue on anything like this with core?

Here are the benchmark results for commit 8700e71.
There were significant changes against commit efeadfb:

  Benchmark                                   Metric         Change
  =================================================================
+ ~Mathlib.RingTheory.Kaehler.JacobiZariski   instructions   -29.1%

I think I need to take a little time to evaluate this holistically. I am concerned we are papering over problems which will only become worse with time.

I raise your 29% to 60% ;-)

#21165 (comment)

I raise your 29% to 60% ;-)

You did not follow the unwritten rules of this competition which clearly state without changing the results of this file. :)

But I saved half a trillion instructions! That is a huge number!

I've closed the PR in case anyone thought it was serious.

How do we move forwards on this? Presumably someone needs to find some kind of example, ideally mathlib-free, showing where the problem is? This might be really hard.

I am not sure that this PR is more serious than #21165. The latter does follow existing patterns in Mathlib.

Given @kbuzzard 's comment I am becoming more skeptical that the current design is aligned with how Lean works, currently.

1. We should raise the issue with core to get their opinion on design. Note that δAux_toAlgHom seems a prime example for this comment
2. We can attempt a fix to the elaborator and/or kernel to see if indeed inconsistent universe normalization of nested max's is a/the culprit here.
3. We can, and probably should, attempt to unbundle the type fields from the offending structures.

This has now come up in the triage meeting because it's one of the longest open PRs on the queue. One way of proceeding is that we document that this is a hack and merge it because at the end of the day it's making mathlib compile more quickly for everyone. What do people think about this?

PS there doesn't seem to be a link to the relevant Zulip thread, which is here.

I still worry we are just digging ourselves deeper into a hole with the current designs.

This pull request has conflicts, please merge master and resolve them.

This PR has been migrated to a fork-based workflow: #26008