Skip to content

Commit

Permalink
only print names
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed May 18, 2024
1 parent 7a039e1 commit 4643b24
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 6 deletions.
4 changes: 2 additions & 2 deletions scripts/count_decls.lean
Original file line number Diff line number Diff line change
Expand Up @@ -76,10 +76,10 @@ def mkTallyNames (s : TallyNames) : MetaM TallyNames := do
`Mathlib`, `Batteries` and core. -/
elab "count_decls" : command => do
let (s, _) ← Command.liftCoreM do Meta.MetaM.run do (mkTallyNames {})
logInfo s!"Theorems {s.thms.size}\n{s.thms.toArray}\nData {s.data.size}\n{s.data.toArray}\nPredicates {s.preds.size}\n{s.preds.toArray}\nTypes {s.types.size}\n{s.types.toArray}"
logInfo s!"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}"

--count_decls
count_decls

end PeriodicReports
14 changes: 10 additions & 4 deletions scripts/mathlib_stats.sh
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,11 @@ net=$(awk -v gd="${gdiff}" 'BEGIN{
# Lean-based reports #
######################

newDeclsTots="$(sed 's=^--\(count_decls\)=\1=' scripts/count_decls.lean | lake env lean --stdin)"
newDecls="$(echo "${newDeclsTots}" | awk '((NF == 2) && $2+0 == $2) { print $0 }')"
newDeclsTots="$(sed 's=^--\(count_decls\)=\1=' scripts/count_decls.lean | lake env lean --stdin |
sed 's=[,\]]=,\n=g')"
newDecls="$(echo "${newDeclsTots}" | awk '/[^,]$/) { type=$0 } /,$/ { acc[type]++ } END{
for(t in type) { printf("%s %s", t, acc[t]) }
}')"
# Definitions 73590...
git checkout -q "${oldCommit}"
# 'detached HEAD' state
Expand All @@ -54,8 +57,11 @@ lake exe cache get > /dev/null
# update the `count_decls` and `mathlib_stats` scripts to the latest version
git checkout -q origin/adomani/periodic_reports_dev_custom_action scripts/count_decls.lean scripts/mathlib_stats.sh

oldDeclsTots="$(sed 's=^--\(count_decls\)=\1=' scripts/count_decls.lean | lake env lean --stdin)"
oldDecls="$(echo "${oldDeclsTots}" | awk '((NF == 2) && $2+0 == $2) { print $0 }')"
oldDeclsTots="$(sed 's=^--\(count_decls\)=\1=' scripts/count_decls.lean | lake env lean --stdin |
sed 's=[,\]]=,\n=g')"
oldDecls="$(echo "${oldDeclsTots}" | awk '/[^,]$/) { type=$0 } /,$/ { acc[type]++ } END{
for(t in type) { printf("%s %s", t, acc[t]) }
}')"
# Definitions 73152...

declSummary="$(paste -d' ' <(echo "${newDecls}") <(echo "${oldDecls}") |
Expand Down

0 comments on commit 4643b24

Please sign in to comment.