All the equational lemma generation bugs in doc-gen4

[hargoniX]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

For doc-gen4 I'm generating all the equational lemmata there are (with the exception of those that time out due to heartbeats)
and the following of them are failing with actual errors during generation instead of just a timeout:

• BinaryHeap.heapifyDown
• Array.findIdx?.loop
• ByteSlice.forIn.loop
• Lean.expandExplicitBindersAux.loop
• Lean.Export.exportName
• Array.heapSort.loop
• Lean.Elab.Term.resolveLocalName.loop
• Lean.Export.exportLevel

they are most likely not all related to the same issue since there are different error messages but I figured posting them in one issue might be for the best.

Steps to Reproduce

Note that some of these functions are coming from Mathlib4, I reproduce it like this by cloning Mathlib4, setting the lean-toolchain to the (current) latest nightly and writing the following at the bottom of Mathlib.lean:

-- Only required for heapifyDown to fail
set_option maxHeartbeats 100000
attribute [simp] BinaryHeap.heapifyDown
attribute [simp] Array.findIdx?.loop
attribute [simp] ByteSlice.forIn.loop
attribute [simp] Lean.expandExplicitBindersAux.loop
attribute [simp] Lean.Export.exportName
attribute [simp] Array.heapSort.loop
attribute [simp] Lean.Elab.Term.resolveLocalName.loop
attribute [simp] Lean.Export.exportLevel

All of these end up failing with quite large error messages I don't really know what to make of

Versions

Lean: Lean (version 4.0.0-nightly-2022-02-04, commit 6d07092, Release)
OS: Linux

[leodemoura]

@hargoniX Thanks for creating the issue. I will investigate and try to improve the tactic used to automatically prove the equational theorems.

All of these end up failing with quite large error messages I don't really know what to make of

The error message includes the proof state where the tactic got stuck, and its complexity is proportional to the size of the definition.

[leodemoura]

The previous commit also fixes

attribute [simp] ByteSlice.forIn.loop