Debugging timeout in doc-gen

Stream: lean4

[Anne Baanen]

I am working on rendering a tactic index in doc-gen, but I get a timeout in whnf when I try it on my test repository:

[...]

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Server.moduleFromDocumentUri: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.CodeAction.holeCodeActionProvider: failed to generate equality theorems for `match` expression `_private.Lean.Server.CodeActions.Provider.0.Lean.CodeAction.holeCodeActionProvider.match_5`
case isTrue
motive✝ : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo) → Sort u_1
x✝¹ : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo)
h_1✝ : (ctx : Lean.Elab.ContextInfo) → (info : Lean.Elab.TermInfo) → motive✝ #[(ctx, info)]
h_2✝ : (x : Array (Lean.Elab.ContextInfo × Lean.Elab.TermInfo)) → motive✝ x
x✝ : ∀ (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.TermInfo), x✝¹ = #[(ctx, info)] → False
h✝ : x✝¹.size = 1
⊢ (⋯ ▸ fun h => ⋯ ▸ Prod.casesOn (x✝¹.getLit 0 ⋯ ⋯) fun fst snd => h_1✝ fst snd) ⋯ = h_2✝ x✝¹
WARNING: Failed to calculate equational lemmata for Lean.Elab.Tactic.evalGrindCore: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Meta.Tactic.TryThis.addRewriteSuggestion: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
WARNING: Failed to calculate equational lemmata for Lean.Expr.name?: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
info: stderr:
uncaught exception: (deterministic) timeout at `whnf`, maximum number of heartbeats (100000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
error: external command '/home/runner/work/docgen-tester/docgen-tester/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4' exited with code 1
Some required targets logged failures:
- «doc-gen4»/coreDocs

(At least I think that is the source of the error, I didn't see any other error while scrolling through the full logs.)

How should I start debugging this? I tried dbg_trace around the code I added, but that seems to exit without issues. So the error seems to be in something I did not write?

[Henrik Böving]

Many of these whnf timeouts are expected because it is just generally impossible to compute and render all of the equations within a reasonable time (hence why they are also just warnings)). I would not be terribly surprised if core has just grown to a point where it can't be rendered on a machine as weak as a github runner anymore because it doesn't have enough RAM? It's quite hard to tell what's going wrong, given that it just manages to do this every 8 hours on mathlib4_docs.

[Anne Baanen]

The same error seems to happen on my machine, though. Thing is, the last one is not a warning but an uncaught exception, which tears down the whole build proces...

[Henrik Böving]

In that case I'd say the first step to figuring out what is wrong is to figure out what it is that you do differently from the mathlib4_docs CI then :sweat_smile:

[Anne Baanen]

Mhm. I put a dbg_trace s!"Wrote the tactic docs." after my new code gets called, and this shows up before all the whnf warnings (as expected, since the module doc rendering happens after the tactics).

[Henrik Böving]

So does it work on your machine without the diff

[Anne Baanen]

Yes!

[Anne Baanen]

(And also in CI.)

[Anne Baanen]

Although there was a lean version bump in between. Sorry, one moment please.

[Anne Baanen]

Yep, on the doc-gen commit tagged v4.24.0, the build succeeds as expected: without a timeout error (and lots of warnings).

[Henrik Böving]

It's not quite clear to me what is happening then either, the only thing I could imagine from the top of my head is that maybe Lean.Elab.Tactic.Doc.allTacticDocs does something to the environment which then causes a subsequent whnf call to fail for some reaosn? But I'm really not quite sure.