Skip to content

Commit

Permalink
Try printing with formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed May 19, 2024
1 parent 0eaad27 commit 5172e5f
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 4 deletions.
18 changes: 16 additions & 2 deletions scripts/count_decls.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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}"

Expand Down
5 changes: 3 additions & 2 deletions scripts/mathlib_stats.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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\n\ngrep ,.\n%s\n' "$(echo "${newDeclsTots}" | head)" "$(echo "${newDeclsTots}" | tail)" "$(echo "${newDeclsTots}" | grep -1 "[^,]$" | sed 's=---=-/-=')" "$(echo "${newDeclsTots}" | grep ",.")"

0 comments on commit 5172e5f

Please sign in to comment.