From c8712783b4f1a280de1d7dfa0e9e2ad2163a9606 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Sun, 19 May 2024 06:20:53 +0200
Subject: [PATCH] Try printing with formatting

---
 scripts/count_decls.lean | 20 +++++++++++++++++---
 scripts/mathlib_stats.sh |  5 +++--
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/scripts/count_decls.lean b/scripts/count_decls.lean
index 54c8d585e2c273..f809fa0c9be92a 100644
--- a/scripts/count_decls.lean
+++ b/scripts/count_decls.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller, Damiano Testa
 -/
-import Mathlib --.Data.Nat.Defs
+import Mathlib.Data.Nat.Defs
 
 /-!
 # `count_decls` -- a tally of declarations in `Mathlib`
@@ -36,6 +36,19 @@ structure TallyNames where
   types : HashSet Name := {}
   data  : HashSet Name := {}
 
+def toString (t : TallyNames) : String :=
+  let print (h : HashSet Name) : String :=
+    let tot := h.toList.map (·.toString)
+    String.intercalate ",\n" tot ++ ","
+  s!"Theorems
+{print t.thms}
+Data
+{print t.data}
+Predicates
+{print t.preds}
+Types
+{print t.types}"
+
 /-- `MathlibModIdxs env` returns the `ModuleIdx`s corresponding to `Mathlib` files
 that are in the provided environment. -/
 def MathlibModIdxs (env : Environment) : IO (HashSet Nat) := do
@@ -75,8 +88,9 @@ def mkTallyNames (s : TallyNames) : MetaM TallyNames := do
 /-- `count_decls` prints a tally of theorems, types, predicates and data in
 `Mathlib`, `Batteries` and core. -/
 elab "count_decls" : command => do
-  let (s, _) ← Command.liftCoreM do Meta.MetaM.run do (mkTallyNames {})
-  logInfo s!"Theorems\n{s.thms.toArray}\nData\n{s.data.toArray}\nPredicates\n{s.preds.toArray}\nTypes\n{s.types.toArray}"
+  let (s, _) ← Command.liftCoreM do MetaM.run do (mkTallyNames {})
+  IO.println (toString s)
+--  logInfo s!"def newTally :=  }Theorems\n{s.thms.toArray}\nData\n{s.data.toArray}\nPredicates\n{s.preds.toArray}\nTypes\n{s.types.toArray}"
 --  logInfo m!"{s.types.toArray}"
 --  logInfo s!"Theorems {s.thms}\nData {s.data}\nPredicates {s.preds}\nTypes {s.types}"
 
diff --git a/scripts/mathlib_stats.sh b/scripts/mathlib_stats.sh
index ff416a2393b6b2..e2352977a84c90 100755
--- a/scripts/mathlib_stats.sh
+++ b/scripts/mathlib_stats.sh
@@ -48,8 +48,7 @@ net=$(awk -v gd="${gdiff}" 'BEGIN{
 # ...
 # ```
 getCountDecls () {
-  sed 's=^--\(count_decls\)=\1=' scripts/count_decls.lean | lake env lean --stdin |
-    sed -z 's=, *=,\n=g; s=[ [#]==g; s=]=,=g; s=\n\n*=\n=g'
+  sed 's=^--\(count_decls\)=\1=' scripts/count_decls.lean | lake env lean --stdin
 }
 
 # extracts
@@ -120,3 +119,5 @@ printf -- ' Reference commits: old %s, new %s.\n\n' "${oldCommitURL}" "${current
 printf -- '%s, %s total(insertions-deletions)\n\n' "${gdiff}" "${net}"
 
 printf -- 'Declarations:\n%s\n\nTake also a look at the [`Mathlib` stats page](%s).\n' "${declSummary}" "${statsURL}"
+
+printf 'head:\n%s\n\ntail:\n%s\n\n%s' "$(echo "${newDeclsTots}" | head)" "$(echo "${newDeclsTots}" | tail)" "$(echo "${newDeclsTots}" | grep -1 "[^,]$")"