Zulip Chat Archive

Stream: lean4

Topic: RFC: `maxHeartbeats` option


Nicolas Rouquette (Dec 08 2025 at 05:19):

I tried adding support for specifying maxHeartbeats in doc-gen4 to address this seemingly simple issue: Add support for specifying maxHeartbeats doc-gen4#335

The PR I developed turned out to be anything but simple: Added support for specifying max heartbeats via an env. variable or a CLI argument doc-gen4#336

In chasing down where maxHeartbeats comes from, I realized that this option should perhaps be included in eqnAffectingOptions as explained here: https://github.com/leanprover/lean4/issues/11546

This addition should be a minimal change, but I'd like to get the experts to weigh in on this.
Without this addition, the current behavior prevents easily overriding maxHeartbeats in doc-gen4 as I've experienced in my PR: https://github.com/leanprover/doc-gen4/pull/336


Last updated: Dec 20 2025 at 21:32 UTC