wip: verso in docstrings

src/Lean/Elab/DocString/Builtin/Postponed.lean

@@ -144,25 +144,26 @@ private def checkDocStringPostponed (declName : Name) (doc : VersoDocString) : C
 /--
 Runs the postponed checks in all docstrings, reporting on the result.
 -/
-def checkPostponed : TermElabM Unit := do
+def checkPostponed (roots : List Name) : TermElabM Unit := do
   let mut checked : Array (Name × Stats) := #[]
   let st := versoDocStringExt.toEnvExtension.getState (← getEnv)
   for (decl, docs) in ← getBuiltinVersoDocStrings do
     let ((), out) ← checkDocStringPostponed decl docs |>.run {}
     if out.total > 0 then
       checked := checked.push (decl, out)
-  for mod in st.importedEntries do
-    for (decl, docs) in mod do
-      let ((), out) ← checkDocStringPostponed decl docs |>.run {}
-      if out.total > 0 then
-        checked := checked.push (decl, out)
+  for (mod, name) in st.importedEntries.zip (← getEnv).header.moduleNames do
+    if roots.any (·.isPrefixOf name) then
+      for (decl, docs) in mod do
+        let ((), out) ← checkDocStringPostponed decl docs |>.run {}
+        if out.total > 0 then
+          checked := checked.push (decl, out)
   for (decl, docs) in st.state do
     let ((), out) ← checkDocStringPostponed decl docs |>.run {}
     if out.total > 0 then
       checked := checked.push (decl, out)
 
   let msg : MessageData :=
-    .trace { cls := `checks } m!"Postponed checks: {checked.size} declarations, \
+    .trace { cls := `checks } m!"Postponed checks for {.andList <| roots.map toMessageData}: {checked.size} declarations, \
         {checked.map (·.2.passed) |>.sum} passed, \
         {checked.map (·.2.failed.size) |>.sum} failed" <|
       checked.map fun (declName, stats) =>

src/Std/Time/Date/Unit/Basic.lean

@@ -14,6 +14,8 @@ public import Std.Time.Date.Unit.Week
 
 public section
 
+set_option doc.verso true
+
 /-!
 This module defines various units used for measuring, counting, and converting between days, months,
 years, weekdays, and weeks of the year.
@@ -29,14 +31,14 @@ open Internal
 namespace Day.Offset
 
 /--
-Convert `Week.Offset` into `Day.Offset`.
+Converts {lean}`Week.Offset` into {lean}`Day.Offset`.
 -/
 @[inline]
 def ofWeeks (week : Week.Offset) : Day.Offset :=
   week.mul 7 |>.cast (by decide +kernel)
 
 /--
-Convert `Day.Offset` into `Week.Offset`.
+Convert {lean}`Day.Offset` into {lean}`Week.Offset`.
 -/
 @[inline]
 def toWeeks (day : Day.Offset) : Week.Offset :=

src/Std/Time/Date/Unit/Day.lean

@@ -16,9 +16,10 @@ namespace Day
 open Lean Internal
 
 set_option linter.all true
+set_option doc.verso true
 
 /--
-`Ordinal` represents a bounded value for days, which ranges between 1 and 31.
+{name}`Ordinal` represents a bounded value for days, which ranges between 1 and 31.
 -/
 @[expose] def Ordinal := Bounded.LE 1 31
 deriving Repr, DecidableEq, LE, LT
@@ -41,8 +42,8 @@ instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
 instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
 
 /--
-`Offset` represents an offset in days. It is defined as an `Int` with a base unit of 86400
-(the number of seconds in a day).
+{name}`Offset` represents an offset in days. It is defined as an {name}`Int` with a base unit of
+86400 (the number of seconds in a day).
 -/
 @[expose] def Offset : Type := UnitVal 86400
 deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
@@ -64,15 +65,15 @@ instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd (UnitVal _)
 namespace Ordinal
 
 /--
-Creates an `Ordinal` from an integer, ensuring the value is within bounds.
+Creates an {name}`Ordinal` from an integer, ensuring the value is within bounds.
 -/
 @[inline]
 def ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 31) : Ordinal :=
   Bounded.LE.mk data h
 
 /--
-`OfYear` represents the day ordinal within a year, which can be bounded between 1 and 365 or 366,
-depending on whether it's a leap year.
+{name}`OfYear` represents the day ordinal within a year, which can be bounded between 1 and 365 or
+366, depending on whether it's a leap year.
 -/
 @[expose] def OfYear (leap : Bool) := Bounded.LE 1 (.ofNat (if leap then 366 else 365))
 
@@ -93,7 +94,7 @@ instance : LawfulEqOrd (OfYear leap) := inferInstanceAs <| LawfulEqOrd (Bounded.
 namespace OfYear
 
 /--
-Creates an ordinal for a specific day within the year, ensuring that the provided day (`data`)
+Creates an ordinal for a specific day within the year, ensuring that the provided day ({name}`data`)
 is within the valid range for the year, which can be 1 to 365 or 366 for leap years.
 -/
 @[inline]
@@ -121,15 +122,15 @@ def ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 31 := by decide) : Ordinal :
   Bounded.LE.ofNat' data h
 
 /--
-Creates an ordinal from a `Fin` value, ensuring it is within the valid range for days of the month (1 to 31).
-If the `Fin` value is 0, it is converted to 1.
+Creates an ordinal from a {name}`Fin` value, ensuring it is within the valid range for days of the
+month (1 to 31). If the {name}`Fin` value is 0, it is converted to 1.
 -/
 @[inline]
 def ofFin (data : Fin 32) : Ordinal :=
   Bounded.LE.ofFin' data (by decide)
 
 /--
-Converts an `Ordinal` to an `Offset`.
+Converts an {name}`Ordinal` to an {name}`Offset`.
 -/
 @[inline]
 def toOffset (ordinal : Ordinal) : Offset :=
@@ -138,7 +139,7 @@ def toOffset (ordinal : Ordinal) : Offset :=
 namespace OfYear
 
 /--
-Converts an `OfYear` ordinal to a `Offset`.
+Converts an {name}`OfYear` ordinal to a {name}`Offset`.
 -/
 def toOffset (ofYear : OfYear leap) : Offset :=
   UnitVal.ofInt ofYear.val
@@ -149,91 +150,91 @@ end Ordinal
 namespace Offset
 
 /--
-Converts an `Offset` to an `Ordinal`.
+Converts an {name}`Offset` to an {name}`Ordinal`.
 -/
 @[inline]
 def toOrdinal (off : Day.Offset) (h : off.val ≥ 1 ∧ off.val ≤ 31) : Ordinal :=
   Bounded.LE.mk off.val h
 
 /--
-Creates an `Offset` from a natural number.
+Creates an {name}`Offset` from a natural number.
 -/
 @[inline]
 def ofNat (data : Nat) : Day.Offset :=
   UnitVal.ofInt data
 
 /--
-Creates an `Offset` from an integer.
+Creates an {name}`Offset` from an integer.
 -/
 @[inline]
 def ofInt (data : Int) : Day.Offset :=
   UnitVal.ofInt data
 
 /--
-Convert `Day.Offset` into `Nanosecond.Offset`.
+Converts {name}`Day.Offset` into {name}`Nanosecond.Offset`.
 -/
 @[inline]
 def toNanoseconds (days : Day.Offset) : Nanosecond.Offset :=
   days.mul 86400000000000 |>.cast (by decide +kernel)
 
 /--
-Convert `Nanosecond.Offset` into `Day.Offset`.
+Converts {name}`Nanosecond.Offset` into {name}`Day.Offset`.
 -/
 @[inline]
 def ofNanoseconds (ns : Nanosecond.Offset) : Day.Offset :=
   ns.ediv 86400000000000 |>.cast (by decide +kernel)
 
 /--
-Convert `Day.Offset` into `Millisecond.Offset`.
+Converts {name}`Day.Offset` into {name}`Millisecond.Offset`.
 -/
 @[inline]
 def toMilliseconds (days : Day.Offset) : Millisecond.Offset :=
   days.mul 86400000 |>.cast (by decide +kernel)
 
 /--
-Convert `Millisecond.Offset` into `Day.Offset`.
+Converts {name}`Millisecond.Offset` into {name}`Day.Offset`.
 -/
 @[inline]
 def ofMilliseconds (ms : Millisecond.Offset) : Day.Offset :=
   ms.ediv 86400000 |>.cast (by decide +kernel)
 
 /--
-Convert `Day.Offset` into `Second.Offset`.
+Converts {name}`Day.Offset` into {name}`Second.Offset`.
 -/
 @[inline]
 def toSeconds (days : Day.Offset) : Second.Offset :=
   days.mul 86400 |>.cast (by decide +kernel)
 
 /--
-Convert `Second.Offset` into `Day.Offset`.
+Converts {name}`Second.Offset` into {name}`Day.Offset`.
 -/
 @[inline]
 def ofSeconds (secs : Second.Offset) : Day.Offset :=
   secs.ediv 86400 |>.cast (by decide +kernel)
 
 /--
-Convert `Day.Offset` into `Minute.Offset`.
+Converts {name}`Day.Offset` into {name}`Minute.Offset`.
 -/
 @[inline]
 def toMinutes (days : Day.Offset) : Minute.Offset :=
   days.mul 1440 |>.cast (by decide +kernel)
 
 /--
-Convert `Minute.Offset` into `Day.Offset`.
+Converts {name}`Minute.Offset` into {name}`Day.Offset`.
 -/
 @[inline]
 def ofMinutes (minutes : Minute.Offset) : Day.Offset :=
   minutes.ediv 1440 |>.cast (by decide +kernel)
 
 /--
-Convert `Day.Offset` into `Hour.Offset`.
+Converts {name}`Day.Offset` into {name}`Hour.Offset`.
 -/
 @[inline]
 def toHours (days : Day.Offset) : Hour.Offset :=
   days.mul 24 |>.cast (by decide +kernel)
 
 /--
-Convert `Hour.Offset` into `Day.Offset`.
+Converts {name}`Hour.Offset` into {name}`Day.Offset`.
 -/
 @[inline]
 def ofHours (hours : Hour.Offset) : Day.Offset :=

src/Std/Time/Date/Unit/Month.lean

@@ -17,9 +17,10 @@ open Std.Internal
 open Internal
 
 set_option linter.all true
+set_option doc.verso true
 
 /--
-`Ordinal` represents a bounded value for months, which ranges between 1 and 12.
+{name}`Ordinal` represents a bounded value for months, which ranges between 1 and 12.
 -/
 @[expose] def Ordinal := Bounded.LE 1 12
 deriving Repr, DecidableEq, LE, LT
@@ -43,7 +44,7 @@ instance : TransOrd Ordinal := inferInstanceAs <| TransOrd (Bounded.LE 1 _)
 instance : LawfulEqOrd Ordinal := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _)
 
 /--
-`Offset` represents an offset in months. It is defined as an `Int`.
+{name}`Offset` represents an offset in months. It is defined as an {name}`Int`.
 -/
 @[expose] def Offset : Type := Int
 deriving Repr, DecidableEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE
@@ -64,7 +65,8 @@ instance : TransOrd Offset := inferInstanceAs <| TransOrd Int
 instance : LawfulEqOrd Offset := inferInstanceAs <| LawfulEqOrd Int
 
 /--
-`Quarter` represents a value between 1 and 4, inclusive, corresponding to the four quarters of a year.
+{name}`Quarter` represents a value between 1 and 4, inclusive, corresponding to the four quarters of
+a year.
 -/
 @[expose] def Quarter := Bounded.LE 1 4
 deriving Repr, DecidableEq, LT, LE
@@ -83,7 +85,7 @@ instance : LawfulEqOrd Quarter := inferInstanceAs <| LawfulEqOrd (Bounded.LE 1 _
 namespace Quarter
 
 /--
-Determine the `Quarter` by the month.
+Determine the {name}`Quarter` by the month.
 -/
 def ofMonth (month : Month.Ordinal) : Quarter :=
   month
@@ -96,14 +98,14 @@ end Quarter
 namespace Offset
 
 /--
-Creates an `Offset` from a natural number.
+Creates an {name}`Offset` from a natural number.
 -/
 @[inline]
 def ofNat (data : Nat) : Offset :=
   Int.ofNat data
 
 /--
-Creates an `Offset` from an integer.
+Creates an {name}`Offset` from an integer.
 -/
 @[inline]
 def ofInt (data : Int) : Offset :=
@@ -174,28 +176,28 @@ The ordinal value representing the month of December.
 @[inline] def december : Ordinal := 12
 
 /--
-Converts a `Ordinal` into a `Offset`.
+Converts a {name}`Ordinal` into a {name}`Offset`.
 -/
 @[inline]
 def toOffset (month : Ordinal) : Offset :=
   month.val
 
 /--
-Creates an `Ordinal` from an integer, ensuring the value is within bounds.
+Creates an {name}`Ordinal` from an integer, ensuring the value is within bounds.
 -/
 @[inline]
 def ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 12) : Ordinal :=
   Bounded.LE.mk data h
 
 /--
-Creates an `Ordinal` from a `Nat`, ensuring the value is within bounds.
+Creates an {name}`Ordinal` from a {name}`Nat`, ensuring the value is within bounds.
 -/
 @[inline]
 def ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 12 := by decide) : Ordinal :=
   Bounded.LE.ofNat' data h
 
 /--
-Converts a `Ordinal` into a `Nat`.
+Converts a {name}`Ordinal` into a {name}`Nat`.
 -/
 @[inline]
 def toNat (month : Ordinal) : Nat := by
@@ -204,15 +206,15 @@ def toNat (month : Ordinal) : Nat := by
   | ⟨.negSucc s, h⟩ => nomatch h.left
 
 /--
-Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds, if its 0 then its converted
+Creates an {name}`Ordinal` from a {name}`Fin`, ensuring the value is within bounds, if its 0 then its converted
 to 1.
 -/
 @[inline]
 def ofFin (data : Fin 13) : Ordinal :=
   Bounded.LE.ofFin' data (by decide)
 
 /--
-Transforms `Month.Ordinal` into `Second.Offset`.
+Transforms {name}`Month.Ordinal` into {name}`Second.Offset`.
 -/
 def toSeconds (leap : Bool) (month : Ordinal) : Second.Offset :=
   let daysAcc := #[0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334]
@@ -223,21 +225,21 @@ def toSeconds (leap : Bool) (month : Ordinal) : Second.Offset :=
     else time
 
 /--
-Transforms `Month.Ordinal` into `Minute.Offset`.
+Transforms {name}`Month.Ordinal` into {name}`Minute.Offset`.
 -/
 @[inline]
 def toMinutes (leap : Bool) (month : Ordinal) : Minute.Offset :=
   toSeconds leap month |>.toMinutes
 
 /--
-Transforms `Month.Ordinal` into `Hour.Offset`.
+Transforms {name}`Month.Ordinal` into {name}`Hour.Offset`.
 -/
 @[inline]
 def toHours (leap : Bool) (month : Ordinal) : Hour.Offset :=
   toMinutes leap month |>.toHours
 
 /--
-Transforms `Month.Ordinal` into `Day.Offset`.
+Transforms {name}`Month.Ordinal` into {name}`Day.Offset`.
 -/
 @[inline]
 def toDays (leap : Bool) (month : Ordinal) : Day.Offset :=
@@ -280,7 +282,7 @@ theorem days_gt_27 (leap : Bool) (i : Month.Ordinal) : days leap i > 27 := by
     decide +revert
 
 /--
-Returns the number of days until the `month`.
+Returns the number of days until the {name}`month`.
 -/
 def cumulativeDays (leap : Bool) (month : Ordinal) : Day.Offset := by
   let ⟨months, p⟩ := cumulativeSizes
@@ -307,8 +309,8 @@ theorem difference_eq (p : month.val ≤ 11) :
   | ⟨12, _⟩ => contradiction
 
 /--
-Checks if a given day is valid for the specified month and year. For example, `29/02` is valid only
-if the year is a leap year.
+Checks if a given day is valid for the specified month and year. For example, February 29 is valid
+only if the year is a leap year.
 -/
 abbrev Valid (leap : Bool) (month : Month.Ordinal) (day : Day.Ordinal) : Prop :=
   day.val ≤ (days leap month).val