import Mathlib leads to Lean not terminating

Stream: new members

[Sven Manthe]

I used a Lean file with "import Mathlib", and repeatedly different non-well-typed statements led to Lean using 100% CPU and seemingly not terminating (for at least some minutes). Moreover, removing the relevant line did not stop this Lean process, and adding it back in increased the CPU usage by another 100%. The only way to stop it seemed to be to kill the Lean process externally.
Replacing the import Mathlib by importing only the parts I needed resolved the issue. I could reproduce this behavior both on Manjaro and Linux Mint. @Floris van Doorn suggested I report it here. Here is a minimal working example (the last line causing the problems), but I also have different examples:

import Mathlib

@[ext]
structure ATree (A: Type) where
  carrier: Set (List A)
  isTree: ∀(x: List A)(a: A), x ++ [a] ∈ carrier → x ∈ carrier

instance : CoeFun (ATree A) (Set (List A)) where coe T := T.carrier

[Adomas Baliuka]

In my very brief experience of using import Mathlib, very long compilation times were normal but settled down eventually (as long as I didn't modify anything within Mathlib itself and only used it in my own code)

[Kevin Buzzard]

import Mathlib is not the problem, that compiles super-quickly in Lean 4 (assuming you've got your project set up correctly with a fully-compiled mathlib). I need to add variable (A : Type) to make this a full MWE but Lean hangs on the instance for me.

[Kevin Buzzard]

With just import Mathlib.Data.Set.Basic I get the expected error

application type mismatch
  CoeFun (ATree A) (Set (List A))
argument
  Set (List A)
has type
  Type : Type 1
but is expected to have type
  outParam (ATree A → Sort ?u.427) : Type ?u.427

[Eric Wieser]

docs#CoeFun doesn't make any sense here

[Eric Wieser]

I think there must be a bad coercion instance somewhere

[Kevin Buzzard]

import Mathlib.Order.Heyting.Regular

is the bad import.

[Eric Wieser]

How did you find that so quickly?

[Kevin Buzzard]

blind luck

[Kevin Buzzard]

I copied the entire Mathlib.lean as imports to the file and then bisected. The big problem with this approach is that when you finally get it down to one import, that import file is not the problem because it imports 5 other files which import 25 other files etc etc, so the search has only just begun. So I bisected down to that import, and then replaced it with its only import and the problem went away and I was like "wooah, it must be my birthday or something"

[Eric Wieser]

docs#Heyting.Regular.instCoeRegular is the bad instance

[Eric Wieser]

In that attribute [-instance] Heyting.Regular.instCoeRegular makes the problem go away

[Eric Wieser]

The instance looks harmless though

[Kevin Buzzard]

Kevin Buzzard said:

blind luck

Oh, the correct answer is actually "problem happens to be in a leaf file" (which might also explain why it wasn't spotted before)

[Floris van Doorn]

Eric Wieser said:

The instance looks harmless though

Shouldn't it be marked as CoeHead or CoeTail or something? It clearly is not harmless...

[Mario Carneiro]

yes, it should be a CoeOut

[Floris van Doorn]

Even without that instance, it takes 3+ seconds to fail, which is kinda unfortunate. It's quite sad that all coercions take 1-2 seconds to fail, even if they are clearly nonsense, like between Set (List A) =?= sorryAx (ATree A → Sort ?u.535) true T

[Floris van Doorn]

The failure takes almost a thousand steps, each costing 0-30ms.

[Kevin Buzzard]

Floris you're old enough to remember when attempting to coerce from Int to Nat in Lean 3 would time out; hopefully now, like then, we'll be able to solve these problems.

[Floris van Doorn]

#7293

[Floris van Doorn]

Kevin Buzzard said:

Floris you're old enough to remember when attempting to coerce from Int to Nat in Lean 3 would time out; hopefully now, like then, we'll be able to solve these problems.

I hope so. This is causing quite a lot of issues.

[Floris van Doorn]

And of course we should write Lean 4 linters guarding against bad coercions like the one above.

[Eric Wieser]

Is the problem that Lean is trying to coerce to Set (List A), so it tries to find Regular (Set (List A)), which it thinks it can get from Regular (Regular (Set (List A)))...?

[Floris van Doorn]

I am quite sure that was exactly what was happening.

[Floris van Doorn]

We had linters in Lean 3 against such coercions (although I forgot which of Foo A -> A or A -> Bar A was problematic).

[Anne Baanen]

Kevin Buzzard said:

I copied the entire Mathlib.lean as imports to the file and then bisected. The big problem with this approach is that when you finally get it down to one import, that import file is not the problem because it imports 5 other files which import 25 other files etc etc, so the search has only just begun.

Perhaps we should have (a script that generates) a version of Mathlib.lean with the imports topologically sorted. So that A.lean comes after B.lean if A imports B. Might be a useful first step towards a #mwe-ifier.