Added support for specifying max heartbeats via an env. variable or a CLI argument #336
Conversation
Lake's getAugmentedEnv creates a new environment with only specific variables (LEAN_PATH, LEAN_SRC_PATH, etc.) rather than inheriting the shell environment. This means DOCGEN_MAX_HEARTBEATS was not being passed through to the doc-gen4 subprocess. This fix reads DOCGEN_MAX_HEARTBEATS from the environment in the lakefile and explicitly passes it as --max-heartbeats CLI argument to the 'single' and 'genCore' commands.
The maxHeartbeats parameter was being passed to Load.load but the Process.process function had a hardcoded value of 5000000 that was overriding it. This fix: 1. Adds maxHeartbeats parameter to Process.process (with same default) 2. Uses the parameter instead of hardcoded value 3. Passes maxHeartbeats from Load.load to Process.process This allows DOCGEN_MAX_HEARTBEATS env var or --max-heartbeats CLI flag to actually control the heartbeat limit during documentation generation.
The maxHeartbeats field in Core.Context doesn't affect Lean's internal operations like equation theorem generation (getEqnsFor?). Those use the maxHeartbeats *option* which has a default of 200000. This fix adds maxHeartbeats to the options in both Load.lean and Analyze.lean, so that elaboration operations respect the configured limit.
hargoniX
left a comment
hargoniX
left a comment
There was a problem hiding this comment.
Thanks for implementing this! Just one question, do you plan to do the fix for adapting the new String.toNat? next Lean release yourself or should I put that on my TODO list?
|
I'll clean up the PR to use the new I need to look into the discussion about |
- Removed the parseNatWithUnderscores function and its doc comments with issue references - Simplified getMaxHeartbeats to use flag.as! Nat directly for the CLI flag and s.toNat? for the environment variable - Changed the max-heartbeats flag type from String to Nat in both singleCmd and genCoreCmd - Removed the "Supports underscores as separators" mention from flag descriptions In README.md: - Removed the "Underscores can be used as separators for readability" sentence (the examples still show underscores since they will work in a version of Lean4 that includes this merged PR: leanprover/lean4#11541
I would prefer merging this PR after verifying that it actually works on a version of Lean4 that has @nomeata 's changes. |
|
My planned changes will probably not affect this issue here. The issue here is that |
3 participants
See #335