From 98eb51ae14eeb281648fef6f02f98a333cef382b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 28 Dec 2017 21:39:36 +0100
Subject: Python script checking missing/unnecessary [needs: rebase] label

---
 dev/tools/github-check-prs.py | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100755 dev/tools/github-check-prs.py

(limited to 'dev')

diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
new file mode 100755
index 0000000000..2ba751d07d
--- /dev/null
+++ b/dev/tools/github-check-prs.py
@@ -0,0 +1,29 @@
+#!/usr/bin/env python3
+
+# Requires PyGithub https://pypi.python.org/pypi/PyGithub
+from github import Github
+
+REPO = "coq/coq"
+REBASE_LABEL="needs: rebase"
+
+token = input("Github access token: ")
+
+g = Github(token)
+
+repo = g.get_repo(REPO)
+
+for pull in repo.get_pulls():
+    # if conflicts then dirty
+    # otherwise blocked (because I have no rights)
+    dirty = pull.mergeable_state == "dirty"
+    labelled = False
+    for label in repo.get_issue(pull.number).get_labels():
+        if label.name == REBASE_LABEL:
+            labelled = True
+    if labelled and not dirty:
+        print ("PR #" + str(pull.number) + " is not dirty but is labelled")
+    elif dirty and not labelled:
+        print ("PR #" + str(pull.number) + " is dirty and not labelled")
+    else:
+        # give some feedback so the user can see we didn't crash
+        print ("PR #" + str(pull.number) + " OK")
-- 
cgit v1.2.3


From 2b28380d1d04c0dc2d0899ba3f3489e29015a6fa Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 30 Dec 2017 19:37:49 +0100
Subject: Expound on dependencies for github-check-prs.py

---
 dev/tools/github-check-prs.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
index 2ba751d07d..9688308d92 100755
--- a/dev/tools/github-check-prs.py
+++ b/dev/tools/github-check-prs.py
@@ -1,6 +1,8 @@
 #!/usr/bin/env python3
 
-# Requires PyGithub https://pypi.python.org/pypi/PyGithub
+# Requires PyGithub https://pypi.python.org/pypi/PyGithub, for instance
+# debian package: python3-github
+# nix: nix-shell -p python3 python3Packages.PyGithub --run ./github-check-rebase.py
 from github import Github
 
 REPO = "coq/coq"
-- 
cgit v1.2.3


From 17067aac03eabb8369d587dc91b622642b2673f8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 30 Dec 2017 20:06:26 +0100
Subject: github-check-prs.py: command line option to get token from a file

---
 dev/tools/github-check-prs.py | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
index 9688308d92..74325d3ee5 100755
--- a/dev/tools/github-check-prs.py
+++ b/dev/tools/github-check-prs.py
@@ -4,13 +4,27 @@
 # debian package: python3-github
 # nix: nix-shell -p python3 python3Packages.PyGithub --run ./github-check-rebase.py
 from github import Github
+import argparse
 
 REPO = "coq/coq"
 REBASE_LABEL="needs: rebase"
 
-token = input("Github access token: ")
+parser = argparse.ArgumentParser()
+parser.add_argument("--token-file", type=argparse.FileType('r'))
+args = parser.parse_args()
 
-g = Github(token)
+if args.token_file is None:
+    token = input("Github access token: ")
+else:
+    token = args.token_file.read().rstrip("\n")
+    args.token_file.close()
+
+if token == "":
+    print ("Warning: using the GitHub API without a token")
+    print ("We may run into rate limit issues")
+    g = Github()
+else:
+    g = Github(token)
 
 repo = g.get_repo(REPO)
 
-- 
cgit v1.2.3


From eece27397cb3befe9d4c7cdad65d3a38b61d7a36 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 8 Jan 2018 11:52:51 +0100
Subject: github-check-prs.py: Strip spaces from token from command line

---
 dev/tools/github-check-prs.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
index 74325d3ee5..7c9043e63a 100755
--- a/dev/tools/github-check-prs.py
+++ b/dev/tools/github-check-prs.py
@@ -14,7 +14,7 @@ parser.add_argument("--token-file", type=argparse.FileType('r'))
 args = parser.parse_args()
 
 if args.token_file is None:
-    token = input("Github access token: ")
+    token = input("Github access token: ").strip()
 else:
     token = args.token_file.read().rstrip("\n")
     args.token_file.close()
-- 
cgit v1.2.3


From 49d4ca23a9d3c61df485d152de734cdc6418d89a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 8 Jan 2018 12:11:12 +0100
Subject: github-check-prs.py: print PR URLs when needed.

---
 dev/tools/github-check-prs.py | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
index 7c9043e63a..beb26d9104 100755
--- a/dev/tools/github-check-prs.py
+++ b/dev/tools/github-check-prs.py
@@ -38,8 +38,10 @@ for pull in repo.get_pulls():
             labelled = True
     if labelled and not dirty:
         print ("PR #" + str(pull.number) + " is not dirty but is labelled")
+        print ("("+ pull.html_url +")")
     elif dirty and not labelled:
         print ("PR #" + str(pull.number) + " is dirty and not labelled")
+        print ("("+ pull.html_url +")")
     else:
         # give some feedback so the user can see we didn't crash
         print ("PR #" + str(pull.number) + " OK")
-- 
cgit v1.2.3