Alphabetical listing of imports

Stream: mathlib4

[Damiano Testa]

Is it something desired/expected that imports be in alphabetical order? I think that this is required for Mathlib.lean and Tactic.lean.

[Anne Baanen]

I certainly check for this in my reviews, mostly because I find it neater. More importantly, it makes merge conflicts easier to spot / resolve: if two PRs change the imports then they will agree on the order, so the only different lines are actual changes in the imports, and not reorderings.

[Eric Wieser]

Note that changing import order can change behavior

[Damiano Testa]

I was giving this a try on branch#adomani/alpha. There is an error in Tactic.Positivity.Core and I wonder if this is what Eric points out or just my script having messed up somewhere.

I'll look into it tomorrow, but the dependence on the order maybe is a signal that alphabetising imports should not be a requirement.

[Damiano Testa]

Also, has someone consciously ordered their imports, so as to simplify a proof?

[Damiano Testa]

This could be next level golfing: find the global permutation of imports that allows you to shorten the most proofs...

[Damiano Testa]

Here is what happens in #6763 for building master (now linting):

• in Mathlib.Tactic.Positivity.Core I left Mathlib.Tactic.NormNum.Core first, to avoid a timeout;
• in Mathlib.LinearAlgebra.Charpoly.ToMatrix I bumped a little the heartbeats (the file has 2 direct imports and swapping them did not fix the timeout);
• in Mathlib.NumberTheory.NumberField.Norm declaration isUnit_norm now builds with

set_option maxHeartbeats 6400000 in  -- via count_heartbeat in
set_option synthInstance.maxHeartbeats 10000000 in -- by hand: timeout with one fewer 0

The sorting of the imports was very crude, so I may have missed sorting "disconnected" imports, but the bulk of the sorting should be done.

As I mentioned, maybe this is not wanted, but, if it is, then the next step would probably be enforcing that new PRs sort their imports and check that the current ones are really all sorted.

[Mario Carneiro]

Damiano Testa said:

Also, has someone consciously ordered their imports, so as to simplify a proof?

To simplify a proof? I doubt it, but to avoid something failing I can definitely imagine

[Matthew Ballard]

That crazy bump is almost completely due to Subalgebra.toX’s

[Damiano Testa]

A different perspective is that it is entirely due to import orders... :upside_down:

[Matthew Ballard]

:) but it can’t just be a problem here

[Damiano Testa]

Agreed! Anyway, I saw that Alex just ibenched the branch, so we'll get some data!

[Matthew Ballard]

I can imagine a fuzzing import order tool ;)

[Matthew Ballard]

At quick glance it wants to pull apart the algebra instance on the algebraic closure

[Damiano Testa]

The results are in. They look... random to me. If anyone who understands what they really say wants to comment, I'd be happy to learn!

[Damiano Testa]

The results are in. They look... random to me. If anyone who understands what they really say wants to comment, I'd be happy to learn!

[Alex J. Best]

I think we should expect them to look random. But it would be good to understand

- ~Mathlib.NumberTheory.NumberField.Norm instructions 1423.4%

at least!

[Matthew Ballard]

Do we have a linter or anything that reports all uses of a particular instance in a build?

[Damiano Testa]

I just re-updated #6763, but maybe there is no interest in doing this.

I personally think that it might be informative to understand

• how to avoid the huge timeouts in docs#RingOfIntegers.isUnit_norm
• why docs#Mathlib.Meta.Positivity.normNumPositivity seem to not build at all, if import Mathlib.Tactic.NormNum.Core does not appear fairly early.

I will stop maintining up to date the PR, but I have a script that alphabetizes the imports, so can recreate it whenever there is interest!