script to count libraries by toolchain

script/count_versions.sh

@@ -0,0 +1,21 @@
+#!/bin/bash
+# Must be run in a copy of the `lean4` repository, and you'll need to login with `gh auth` first.
+for v in $(gh release list | cut -f1) nightly stable
+do
+  sleep 15 # Don't exceed API rate limits!
+  echo -n $v" "
+  count=$(gh search code --filename lean-toolchain -L 1000 "leanprover/lean4:$v" | wc -l)
+  
+  # Check if version number begins with a 'v'
+  if [[ $v == v* ]]; then
+    sleep 5 # Don't exceed API rate limits!
+    # Remove the leading 'v'
+    v_no_v=${v:1}
+    count_no_v=$(gh search code --filename lean-toolchain -L 1000 "leanprover/lean4:$v_no_v" | wc -l)
+    # Sum the two counts
+    total_count=$(($count + $count_no_v))
+    echo $total_count
+  else
+    echo $count
+  fi
+done | awk '{ printf "%-12s %s\n", $1, $2 }'

script/plot_count_versions.py

@@ -0,0 +1,50 @@
+import matplotlib.pyplot as plt
+import pandas as pd
+import numpy as np
+import sys
+from io import StringIO
+
+# Reading data from stdin
+input_data = sys.stdin.read()
+
+# Using StringIO to simulate a file-like object for pandas
+data_io = StringIO(input_data)
+
+# Reading data into DataFrame
+df = pd.read_csv(data_io, sep="\s+", names=['Version', 'Count'])
+
+# Splitting versions into prefix and suffix
+df['Prefix'] = df['Version'].apply(lambda x: x.split('-')[0])
+df['Suffix'] = df['Version'].apply(lambda x: '-'.join(x.split('-')[1:]) if '-' in x else '')
+
+# Grouping and summing by prefix
+grouped = df.groupby('Prefix').sum().reset_index()
+
+# Setting the color map
+color_map = {'': 'blue'}  # Default color for versions without suffix
+suffixes = df['Suffix'].unique()
+greens = plt.cm.Greens(np.linspace(0.3, 0.9, len(suffixes)))
+
+for i, suffix in enumerate(suffixes):
+    if suffix:  # Assign green shades to versions with suffixes
+        color_map[suffix] = greens[i]
+
+# Plotting the bar chart with new color scheme
+plt.figure(figsize=(10, 6))
+for prefix in grouped['Prefix']:
+    subset = df[df['Prefix'] == prefix]
+    bottom = 0
+    for _, row in subset.iterrows():
+        color = color_map[row['Suffix']]
+        plt.bar(prefix, row['Count'], bottom=bottom, label=row['Version'], color=color)
+        bottom += row['Count']
+
+plt.title('Version Contributions with Distinctive Colors')
+plt.xlabel('Version Prefix')
+plt.ylabel('Count')
+plt.xticks(rotation=45)
+plt.legend(title='Version', bbox_to_anchor=(1.05, 1), loc='upper left')
+
+# Save to a file
+output_file_path = 'version_contribution_chart_colored.png'
+plt.savefig(output_file_path)