From 6162d603f9638a678cc4cc227f41169d4fdc5869 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 10 Aug 2020 18:00:58 +0200
Subject: Add badge for admitted proofs

---
 .github/workflows/admitted.yml | 32 ++++++++++++++++++++++++++++++++
 scripts/output.svg             |  1 +
 scripts/statistics.py          | 36 ++++++++++++++++++++++++++++++++++++
 3 files changed, 69 insertions(+)
 create mode 100644 .github/workflows/admitted.yml
 create mode 100644 scripts/output.svg
 create mode 100644 scripts/statistics.py

diff --git a/.github/workflows/admitted.yml b/.github/workflows/admitted.yml
new file mode 100644
index 0000000..7463a10
--- /dev/null
+++ b/.github/workflows/admitted.yml
@@ -0,0 +1,32 @@
+# This is a basic workflow to help you get started with Actions
+
+name: Admitted Icon
+
+# Controls when the action will run. Triggers the workflow on push or pull request
+# events but only for the master branch
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+# A workflow run is made up of one or more jobs that can run sequentially or in parallel
+jobs:
+  # This workflow contains a single job called "build"
+  build:
+    # The type of runner that the job will run on
+    runs-on: ubuntu-latest
+
+    # Steps represent a sequence of tasks that will be executed as part of the job
+    steps:
+    # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
+    - uses: actions/checkout@v2
+
+    # Runs a single command using the runners shell
+    - name: Generate Admitted icon
+      run: python3 scripts/statistics.py src
+
+    - uses: actions/upload-artifact@v2
+      with:
+        name: admitted-icon
+        path: admitted.svg
diff --git a/scripts/output.svg b/scripts/output.svg
new file mode 100644
index 0000000..8829659
--- /dev/null
+++ b/scripts/output.svg
@@ -0,0 +1 @@
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="122" height="20" role="img" aria-label="Admitted Proofs: 99"><title>Admitted Proofs: 99</title><linearGradient id="s" x2="0" y2="100%"><stop offset="0" stop-color="#bbb" stop-opacity=".1"/><stop offset="1" stop-opacity=".1"/></linearGradient><clipPath id="r"><rect width="122" height="20" rx="3" fill="#fff"/></clipPath><g clip-path="url(#r)"><rect width="99" height="20" fill="#555"/><rect x="99" width="23" height="20" fill="#fe7d37"/><rect width="122" height="20" fill="url(#s)"/></g><g fill="#fff" text-anchor="middle" font-family="Verdana,Geneva,DejaVu Sans,sans-serif" text-rendering="geometricPrecision" font-size="110"><text aria-hidden="true" x="505" y="150" fill="#010101" fill-opacity=".3" transform="scale(.1)" textLength="890">Admitted Proofs</text><text x="505" y="140" transform="scale(.1)" fill="#fff" textLength="890">Admitted Proofs</text><text aria-hidden="true" x="1095" y="150" fill="#010101" fill-opacity=".3" transform="scale(.1)" textLength="130">99</text><text x="1095" y="140" transform="scale(.1)" fill="#fff" textLength="130">99</text></g></svg>
\ No newline at end of file
diff --git a/scripts/statistics.py b/scripts/statistics.py
new file mode 100644
index 0000000..927baba
--- /dev/null
+++ b/scripts/statistics.py
@@ -0,0 +1,36 @@
+import urllib.request
+import subprocess
+import sys
+
+
+def collect(d):
+    try:
+        n_admitted = len(subprocess.check_output(
+            ["grep", "-r", "-E", "Admitted", d]).splitlines())
+    except: n_admitted = 0
+
+    try: n_theorems = len(subprocess.check_output(
+            ["grep", "-r", "-E", "Theorem|Lemma|Remark", d]).splitlines())
+    except: n_theorems = 0
+
+    try: n_qed = len(subprocess.check_output(
+            ["grep", "-r", "-E", "Qed|Defined", d]).splitlines())
+    except: n_qed = 0
+
+    return (n_admitted, n_theorems, n_qed)
+
+
+def main(d):
+    n_admitted, _, _ = collect(d)
+
+    url = "https://img.shields.io/badge/Admitted%20Proofs-{}-{}?style=flat".format(
+        str(n_admitted), "orange")
+
+    req = urllib.request.Request(url, headers={"User-Agent": "Mozilla/5.0"})
+    with open("admitted.svg", "wb") as f:
+        with urllib.request.urlopen(req) as r:
+            f.write(r.read())
+
+
+if __name__ == "__main__":
+    main(sys.argv[1])
-- 
cgit