RFC: maxHeartbeats option is not respected during equation theorem generation

Proposal

Clear and detailed description of the proposal. Consider the following questions:

• User Experience: How does this feature improve the user experience?

  I tried adding support for specifying maxHeartbeats in doc-gen4 to address this seemingly simple issue: https://github.com/leanprover/doc-gen4/issues/335

  The PR I developed turned out to be anything but simple: https://github.com/leanprover/doc-gen4/pull/336

  doc-gen4 calculates equations here using Lean.Meta.getEqnsFor?:

  def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
    -- This is the entry point for lazy equation generation. Ignore the current value
    -- of the options, and revert to the default.
    withOptions (eqnAffectingOptions.foldl fun os o => o.set os o.defValue) do
      getEqnsFor?Core declName
  

  • getEqnsFor? resets certain options to defaults via eqnAffectingOptions
  • maxHeartbeats is not in that list, so it gets whatever default is in the fresh context (200000)
  • Therefore, tools like cannot override maxHeartbeats.

• Suggestion:

  Add maxHeartbeats to eqnAffectingOptions

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?

  This should help solving this issue [doc-gen4#335] and simplify the WIP PR doc-gen#336

• Maintainability: Will this change streamline code maintenance or simplify its structure?

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start in Lean/Meta/Eqns.lean at eqnAffectingOptions and getEqnsFor?, then read DocGen4/Process/DefinitionInfo.lean to understand the equation-generation call site. Review doc-gen4 issue #335 and pull request #336 for context; done means maxHeartbeats is honored during equation theorem generation.