aboutsummaryrefslogtreecommitdiffstats
path: root/scripts
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-08-10 19:01:21 +0200
committerYann Herklotz <git@yannherklotz.com>2020-08-10 19:01:21 +0200
commit8dfd752666c2ab1d87523e9e1caf25b0413d65a7 (patch)
tree0e6804213347c8cfe25911fc45dc7ea9a21f69eb /scripts
parentf07e5886be419f776caaf3dc20f7017fe94512b5 (diff)
downloadvericert-8dfd752666c2ab1d87523e9e1caf25b0413d65a7.tar.gz
vericert-8dfd752666c2ab1d87523e9e1caf25b0413d65a7.zip
Correctly pick colour for the badge
Diffstat (limited to 'scripts')
-rw-r--r--scripts/statistics.py12
1 files changed, 10 insertions, 2 deletions
diff --git a/scripts/statistics.py b/scripts/statistics.py
index 927baba..9ec460d 100644
--- a/scripts/statistics.py
+++ b/scripts/statistics.py
@@ -20,11 +20,19 @@ def collect(d):
return (n_admitted, n_theorems, n_qed)
+def pick_colour(n, m):
+ if n > 0.2 * m: return "red"
+ elif n > 0.1 * m: return "orange"
+ elif n == 0: return "brightgreen"
+ else: return "yellow"
+
+
def main(d):
- n_admitted, _, _ = collect(d)
+ n_admitted, n_theorems, _ = collect(d)
+ colour = pick_colour(n_admitted, n_theorems)
url = "https://img.shields.io/badge/Admitted%20Proofs-{}-{}?style=flat".format(
- str(n_admitted), "orange")
+ str(n_admitted), colour)
req = urllib.request.Request(url, headers={"User-Agent": "Mozilla/5.0"})
with open("admitted.svg", "wb") as f: