diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-08-10 18:00:58 +0200 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-10 18:00:58 +0200 |
commit | 6162d603f9638a678cc4cc227f41169d4fdc5869 (patch) | |
tree | 4cebcaff1a203e36fe83ed479f077af2a82d9d45 /scripts | |
parent | 4b433258deffec9207451fb30e4103462c704781 (diff) | |
download | vericert-kvx-6162d603f9638a678cc4cc227f41169d4fdc5869.tar.gz vericert-kvx-6162d603f9638a678cc4cc227f41169d4fdc5869.zip |
Add badge for admitted proofs
Diffstat (limited to 'scripts')
-rw-r--r-- | scripts/output.svg | 1 | ||||
-rw-r--r-- | scripts/statistics.py | 36 |
2 files changed, 37 insertions, 0 deletions
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]) |