RFC: maxHeartbeats option is not respected during equation theorem generation

[NicolasRouquette]

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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[nomeata]

Im actually planning to remove the whole eqnAffectingOptions machinery, given that it was put in place for backward.* options which I hope we can remove.

That said, currently it should use the heartbeats set on the command line. This is generally true for realizable constants that relate to imported files (and so the eqnAffectingOptions is a bit of a red herring here I think).

[NicolasRouquette]

Thanks @nomeata; this will help tools like doc-gen4 and in particularly this PR: https://github.com/leanprover/doc-gen4/pull/336

Presumably, getEqnsFor? will look like this:

def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
  getEqnsFor?Core declName

Presumably, the above should use the value of maxHeartbeats in the current MetaM context.

In the case of doc-gen4, this will be helpful since it constructs a Core.Context that flows through MetaM like this in DocGen4/Load

let config := {
  maxHeartbeats := maxHeartbeats,
  options := ⟨[...]⟩,
  ...
}
Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}

[nomeata]

Presumably, the above should use the value of maxHeartbeats in the current MetaM context.

That's unfortunately not how realizeConst works, the current context is ignored and it's using the context at the beginning of elaboration. Maybe there is a way to affect that, though.