Skip to content

Commit

Permalink
feat: small quality of life improvements in progress tracker (#265)
Browse files Browse the repository at this point in the history
* Sort namespaces alphabetically

 * Valid code for docstring generation
  • Loading branch information
david-christiansen authored Jan 9, 2025
1 parent 7bd1a44 commit 7e93d5b
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions src/verso-manual/VersoManual/Docstring.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1781,11 +1781,13 @@ def progress.descr : BlockDescr where

let tacticPercent := undocTactics.size.toFloat * 100.0 / allTactics.size.toFloat

let namespaces := namespaces.qsort (·.toString ≤ ·.toString)

return {{
<dl>
{{namespaces.map fun ns =>
let wanted := check.findD ns []
let notDocumented := wanted.filter (!ok.contains ·)
let notDocumented := wanted.filter (!ok.contains ·) |>.mergeSort (fun x y => x.toString < y.toString)
let percent := notDocumented.length.toFloat * 100.0 / wanted.length.toFloat
{{
<dt><code>{{ns.toString}}</code></dt>
Expand All @@ -1797,7 +1799,7 @@ def progress.descr : BlockDescr where
</summary>
{{notDocumented |>.map (·.toString) |> String.intercalate ", " }}
<pre>
{{ notDocumented.map ("{docstring " ++ ·.toString ++ "}\n") |> String.join }}
{{ notDocumented.map ("{docstring " ++ ·.toString ++ "}\n\n") |> String.join }}
</pre>
<pre>
"```exceptions\n"
Expand Down

0 comments on commit 7e93d5b

Please sign in to comment.