From 4643b24d730ab08dc8ee950f03e98c08001d42ac Mon Sep 17 00:00:00 2001 From: adomani Date: Sat, 18 May 2024 17:50:19 +0200 Subject: [PATCH] only print names --- scripts/count_decls.lean | 4 ++-- scripts/mathlib_stats.sh | 14 ++++++++++---- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/scripts/count_decls.lean b/scripts/count_decls.lean index 6c2f89bcaa5665..5eee8c3de2c6c5 100644 --- a/scripts/count_decls.lean +++ b/scripts/count_decls.lean @@ -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 diff --git a/scripts/mathlib_stats.sh b/scripts/mathlib_stats.sh index fbdb70933a0900..17a180cd51be4b 100755 --- a/scripts/mathlib_stats.sh +++ b/scripts/mathlib_stats.sh @@ -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 @@ -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}") |