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