Triaging Lean compiler bug

Stream: lean4

[Leni Aniva]

I have a file in a project that when compiled, never finishes compiling and Lean keeps using more and more memory. Is there a canonical way to triage this problem?

[Leni Aniva]

These tracing options don't do anything:

set_option trace.Compiler true
set_option trace.Compiler.result true

I'm using lake lean Test/FileInQuestion.lean to compile the file.

[Aaron Liu]

Try using the trace.compiler.* options, the trace.Compiler.* ones don't seem to do anything yet.

[Leni Aniva]

Lean got stuck after printing this:

[compiler] compiling old: [Catenary.Test.Mystery._example]

where the example is

example (n m k : Nat) (ih : n + m = n + k → m = k) : (n + 1) + m = (n + 1) + k → m = k :=
  let h1 := Nat.succ.injEq (n + m) (n + k)
  let h2 := Eq.trans (congr (congrArg Eq (Nat.succ_add n m)) (Nat.succ_add n k)) h1
  let h3 := implies_congr h2 (Eq.refl (m = k))
  Eq.mpr h3 ih

Correction: It seems like the infinite loop originated in def code and not this example.

[Leni Aniva]

After running for a while:

Test/Mystery.lean:174:4: error: (deterministic) timeout at `delab`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)

[Leni Aniva]

Could it be because there are too few type annotations in the file so isDefEq ate all the heartbeat?

[Patrick Massot]

If this is about the old compiler then the answer is very easy: it will never be fixed. The new compiler is around the corner.

[Leni Aniva]

Patrick Massot said:

If this is about the old compiler then the answer is very easy: it will never be fixed. The new compiler is around the corner.

Will it be in Lean v4.20?

[Patrick Massot]

No, it’s not that close. But it’s close enough to make sure the old compiler won’t get any fix (unless there is something really massively urgent).

[Henrik Böving]

Leni Aniva said:

After running for a while:

Test/Mystery.lean:174:4: error: (deterministic) timeout at `delab`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)

This error message just doesn't look like a compiler error at all to me? It's timing out in delaboration

[Leni Aniva]

Henrik Böving said:

Leni Aniva said:

After running for a while:

Test/Mystery.lean:174:4: error: (deterministic) timeout at `delab`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)

This error message just doesn't look like a compiler error at all to me? It's timing out in delaboration

Yes, it was because I set set_option trace.compiler true. I couldn't figure out what was timing out the compiler.

[Henrik Böving]

And have you actually confirmed that it is a compiler error/timeout by other means?

[Leni Aniva]

Henrik Böving said:

And have you actually confirmed that it is a compiler error by other means?

If I comment out a section of the code (which is a standard test harness) I have, the compiler doesnt time out anymore. That is all the evidence I have. lake test gets stuck at [90/96] Test.Mystery... so the infinite loop probably happens at compile time.