maxRecDepth in getEqnsFor?

Stream: lean4

[Henrik Böving]

A recent Lean update seems to have broken Lean.Meta.getEqnsFor? in a way. More concretely doc-gen4 was generating documentation using this function for Lean.Level.substParams.go just fine until I bumped it from v4.2.0-rc4 to v4.3.0-rc2 just now. Now it fails to generate the equations with a max recursion depth error, #mwe:

import Lean
#eval Lean.Meta.getEqnsFor? `Lean.Level.substParams.go

This can be worked around with set_option maxRecDepth 4096 though, at which point it times out on heartbeats. Note that this was previously possible as https://leanprover-community.github.io/mathlib4_docs/Lean/Level.html#Lean.Level.substParams.go used to contain rendered equation output (right until I deployed the first doc-gen output with the updated version).

Should I report this regression on the issue tracker as well?

[Henrik Böving]

(deleted)

[Henrik Böving]

(deleted)

[Mario Carneiro]

The cause of the failure is this:

example (s : Lean.Name → Option Lean.Level)
  (u_1 v : Lean.Level) :
  Lean.Level.substParams.go s (Lean.Level.succ v) =
    if Lean.Level.hasParam (Lean.Level.succ v) = true then
      Lean.Level.updateSucc! (Lean.Level.succ v) (Lean.Level.substParams.go s v)
    else Lean.Level.succ v := rfl
-- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

[Mario Carneiro]

I just got a regression in mathport of a similar nature: https://github.com/leanprover-community/mathport/actions/runs/6918636188/job/18821091067 (things time out with maxHeartbeats), so this lends credence to there being a performance regression somewhere