In Main.lean:

- 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

Author: NicolasRouquette

Main.lean

@@ -6,21 +6,13 @@ open DocGen4 Lean Cli
 
 def defaultMaxHeartbeats : Nat := 100_000_000
 
-/-- Parse a natural number, allowing underscores as separators (e.g., "100_000_000").
-
- See discussion: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/String.2EtoNat.3F.20and.20String.2EtoInt.3F.20handling.20underscores/with/562357458
- See this related issue: https://github.com/leanprover/lean4/issues/11538
- -/
-def parseNatWithUnderscores (s : String) : Option Nat :=
-  (s.replace "_" "").toNat?
-
 /-- Get maxHeartbeats from CLI flag, falling back to environment variable, then default. -/
 def getMaxHeartbeats (p : Parsed) : IO Nat := do
   match p.flag? "max-heartbeats" with
-  | some flag => pure <| (parseNatWithUnderscores (flag.as! String)).getD defaultMaxHeartbeats
+  | some flag => pure <| flag.as! Nat
   | none => do
     match ← IO.getEnv "DOCGEN_MAX_HEARTBEATS" with
-    | some s => pure <| (parseNatWithUnderscores s).getD defaultMaxHeartbeats
+    | some s => pure <| s.toNat?.getD defaultMaxHeartbeats
     | none => pure defaultMaxHeartbeats
 
 def getTopLevelModules (p : Parsed) : IO (List String) :=  do
@@ -95,18 +87,13 @@ def runBibPrepassCmd (p : Parsed) : IO UInt32 := do
     | _ => throw <| IO.userError "there should be exactly one source file"
   return 0
 
-/--
- See discussion: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/String.2EtoNat.3F.20and.20String.2EtoInt.3F.20handling.20underscores/with/562357458
- If https://github.com/leanprover/lean4/issues/11538 is resolved, change "max-heartbeats" to be of type Nat directly.
- See: https://github.com/leanprover/lean4/pull/11541
- -/
 def singleCmd := `[Cli|
   single VIA runSingleCmd;
   "Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated."
 
   FLAGS:
     b, build : String; "Build directory."
-    "max-heartbeats" : String; "Maximum heartbeats for elaboration (default: 100_000_000). Supports underscores as separators. Can also be set via DOCGEN_MAX_HEARTBEATS env var."
+    "max-heartbeats" : Nat; "Maximum heartbeats for elaboration (default: 100_000_000). Can also be set via DOCGEN_MAX_HEARTBEATS env var."
 
   ARGS:
     module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
@@ -128,7 +115,7 @@ def genCoreCmd := `[Cli|
   FLAGS:
     b, build : String; "Build directory."
     m, manifest : String; "Manifest output, to list all the files generated."
-    "max-heartbeats" : String; "Maximum heartbeats for elaboration (default: 100_000_000). Supports underscores as separators. Can also be set via DOCGEN_MAX_HEARTBEATS env var."
+    "max-heartbeats" : Nat; "Maximum heartbeats for elaboration (default: 100_000_000). Can also be set via DOCGEN_MAX_HEARTBEATS env var."
 
   ARGS:
     module : String; "The module to generate the HTML for."

README.md

@@ -92,7 +92,7 @@ The different options are:
 Generation of equations for definitions is enabled by default, but can be disabled by setting the `DISABLE_EQUATIONS` environment variable to `1`.
 
 ## Max heartbeats
-The maximum number of heartbeats for elaboration can be configured by setting the `DOCGEN_MAX_HEARTBEATS` environment variable. The default is `100_000_000`. Underscores can be used as separators for readability. For example:
+The maximum number of heartbeats for elaboration can be configured by setting the `DOCGEN_MAX_HEARTBEATS` environment variable. The default is `100_000_000`. For example:
 ```
 DOCGEN_MAX_HEARTBEATS=200_000_000 lake build YourLibraryName:docs
 ```