Significance of ordering of imports?

Stream: lean4

[Isak Colboubrani]

Does the order of imports affect the correctness or behavior of a Lean program?

More specifically: Are there any scenarios where reordering the import statements in a Lean file could result in changes to the program's correctness, introduce errors, or alter its runtime behavior?

[Damiano Testa]

Actually, several things can go wrong, the simplest one of which is that a timeout may occur since lean may end up going via a "longer" path than previously.

[Damiano Testa]

There was at some point a proposal or reordering alphabetically all import statements, almost all worked as intended with the alphabetical replacement, some timed out, but would still work increasing the time limit, but one of them I was not able to fix.

[Jon Eugster]

Was that purely a problem with the instance inference not finding the right instances in time or using wrong ones first?

[Jon Eugster]

At least, it's not possible in Lean to import a certain declaration twice, so reordeing imports would not change terms etc. which are actually written out explicitly, right?

[Damiano Testa]

I could not debug the one that kept failing no matter the time limit (it was in... norm_num, maybe?). The others I think that it was instance inference: sometimes, it just had to wade through useless stuff, other times, it may have found a "wrong" one. Let me see if I can find the PR.

[Damiano Testa]

#6763

[Damiano Testa]

In the PR, you can also find a link to a Zulip discussion about it.

[Isak Colboubrani]

Thank you @Damiano Testa—this was a very interesting read! It's quite surprising (at least to me) that the order of imports can have such a significant impact in certain pathological cases. I'm trying to determine whether any of these cases indicate bugs in Lean, or if everything is functioning as intended.

Are there two distinct issues here: one leading to a compilation error and another causing a compilation timeout? Can we construct a minimal working example (#mwe) for each scenario?

Assuming the compilation is successful, would it be theoretically possible for a change in import order to alter runtime behavior? Can we come up with an example of such a scenario?

[Jon Eugster]

So just to elaborate on the instance order, here's a small mock example where a "change of imports" does alter your program output:

import Init.Data.ToString.Basic -- contains `instToStringNat`

open Lean IO

def test [ToString Nat] (n : Nat) : IO Unit := do
  println s!"you entered {n}"

#eval test 1        -- you entered 1
#synth ToString Nat -- instToStringNat

-- assume: due to changed import order, this now has higher priority.
instance badInstance : ToString Nat where
  toString _ := "42"

#eval test 1        -- you entered 42
#synth ToString Nat -- badInstance

This is equivalent to having the badInstance in a second file that's either imported before or after the existing import.

This isn't a bug in Lean, but rather a bad setup by the person adding badInstance. Now, in mathlib it's much more complicated because there is a huge hierarchy of structures, you do want to have multiple paths how to synthesise certain instances, and you have to set your instances up correctly. (In the linked discussion they mention the Subalgebra.toX instances which took higher priority than they should)

Same should apply for implicit arguments {_ : _}, but I'd think that's less commonly a problem because of how they are resolved.

It's also thinkable that a tactic is dependent on the order things are in the environment. For example (not exactly the same as import order, but maybe it's still close enough)

import Lean

def n : Nat := by
  have m := 2
  have l := 3
  assumption

def n' : Nat := by
  have l := 3
  have m := 2
  assumption


#eval n   -- 3
#eval n' -- 2

here I would say isn't a bug in assumption but rather a mistake by the person using assumption in a definition.

I guess my main point is that I believe while it's certainly a bug if the order of imports changes the behaviour of your code, it's most likely not a bug in Lean itself but rather bugs in tactic code or library setups.

[Damiano Testa]

I agree with Jon's point of view: "good" code should probably be independent of import order, but whether it is or not, I do not consider the possibility of writing import-order-depending code as a bug in Lean necessarily.

[Damiano Testa]

As for code behaviour, you could write a linter that checks whether the imports are sorted alphabetically and logs a warning otherwise: this is certainly import-order-dependent code!