3 files changed, 214 insertions, 1 deletions
diff --git a/dev/tools/check-owners-pr.sh b/dev/tools/check-owners-pr.sh
new file mode 100755
index 0000000000..d2910279b5
--- /dev/null
+++ b/dev/tools/check-owners-pr.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env sh
+
+usage() {
+    { echo "usage: $0 PR [ARGS]..."
+      echo "A wrapper around check-owners.sh to check owners for a PR."
+      echo "Assumes upstream is the canonical Coq repository."
+      echo "Assumes the PR is against master."
+      echo
+      echo "  PR: PR number"
+      echo "  ARGS: passed through to check-owners.sh"
+    } >&2
+}
+
+case "$1" in
+    "--help"|"-h")
+        usage
+        if [ $# = 1 ]; then exit 0; else exit 1; fi;;
+    "")
+        usage
+        exit 1;;
+esac
+
+PR="$1"
+shift
+
+# this puts both refs in the FETCH_HEAD file but git rev-parse will use the first
+git fetch upstream "+refs/pull/$PR/head" master
+
+head=$(git rev-parse FETCH_HEAD)
+base=$(git merge-base upstream/master "$head")
+
+git diff --name-only -z "$base" "$head" | xargs -0 dev/tools/check-owners.sh "$@"
diff --git a/dev/tools/check-owners.sh b/dev/tools/check-owners.sh
new file mode 100755
index 0000000000..1a97508abb
--- /dev/null
+++ b/dev/tools/check-owners.sh
@@ -0,0 +1,138 @@
+#!/usr/bin/env bash
+
+# Determine CODEOWNERS of the files given in argument
+# For a given commit range:
+# git diff --name-only -z COMMIT1 COMMIT2 | xargs -0 dev/tools/check-owners.sh [opts]
+
+# NB: gitignore files will be messed up if you interrupt the script.
+# You should be able to just move the .gitignore.bak files back manually.
+
+usage() {
+    { echo "usage: $0 [--show-patterns] [--owner OWNER] [FILE]..."
+      echo "  --show-patterns: instead of printing file names print the matching patterns (more compact)"
+      echo "  --owner: show only files/patterns owned by OWNER (use Nobody to see only non-owned files)"
+    } >&2
+}
+
+case "$1" in
+    "--help"|"-h")
+        usage
+        if [ $# = 1 ]; then exit 0; else exit 1; fi
+esac
+
+if ! [ -e .github/CODEOWNERS ]; then
+    >&2 echo "No CODEOWNERS set up or calling from wrong directory."
+    exit 1
+fi
+
+files=()
+show_patterns=false
+
+target_owner=""
+
+while [[ "$#" -gt 0 ]]; do
+    case "$1" in
+        "--show-patterns")
+            show_patterns=true
+            shift;;
+        "--owner")
+            if [[ "$#" = 1 ]]; then
+                >&2 echo "Missing argument to --owner"
+                usage
+                exit 1
+            elif [[ "$target_owner" != "" ]]; then
+                >&2 echo "Only one --owner allowed"
+                usage
+                exit 1
+            fi
+            target_owner="$2"
+            shift 2;;
+        *)
+            files+=("$@")
+            break;;
+    esac
+done
+
+# CODEOWNERS uses .gitignore patterns so we want to use git to parse it
+# The only available tool for that is git check-ignore
+# However it provides no way to use alternate .gitignore files
+# so we rename them temporarily
+
+find . -name .gitignore -print0 | while IFS= read -r -d '' f; do
+    if [ -e "$f.bak" ]; then
+        >&2 echo "$f.bak exists!"
+        exit 1
+    else
+        mv "$f" "$f.bak"
+    fi
+done
+
+# CODEOWNERS is not quite .gitignore patterns:
+# after the pattern is the owner (space separated)
+# git would interpret that as a big pattern containing spaces
+# so we create a valid .gitignore by removing all but the first field
+
+while read -r pat _; do
+    printf '%s\n' "$pat" >> .gitignore
+done < .github/CODEOWNERS
+
+# associative array [file => owner]
+declare -A owners
+
+for f in "${files[@]}"; do
+    data=$(git check-ignore --verbose --no-index "./$f")
+    code=$?
+
+    if [[ "$code" = 1 ]] || ! [[ "$data" =~ .gitignore:.* ]] ; then
+        # no match, or match from non tracked gitignore (eg global gitignore)
+        if [ "$target_owner" != "" ] && [ "$target_owner" != Nobody ] ; then
+            owner=""
+        else
+            owner="Nobody"
+            pat="$f" # no patterns for unowned files
+        fi
+    else
+        # data looks like [.gitignore:$line:$pattern $file]
+        # extract the line to look it up in CODEOWNERS
+        data=${data#'.gitignore:'}
+        line=${data%%:*}
+
+        # NB: supports multiple owners
+        # Does not support secondary owners declared in comment
+        read -r pat fowners < <(sed "${line}q;d" .github/CODEOWNERS)
+
+        owner=""
+        if [ "$target_owner" != "" ]; then
+            for o in $fowners; do # do not quote: multiple owners possible
+                if [ "$o" = "$target_owner" ]; then
+                    owner="$o"
+                fi
+            done
+        else
+            owner="$fowners"
+        fi
+    fi
+
+    if [ "$owner" != "" ]; then
+        if $show_patterns; then
+            owners[$pat]="$owner"
+        else
+            owners[$f]="$owner"
+        fi
+    fi
+done
+
+for f in "${!owners[@]}"; do
+    printf '%s: %s\n' "$f" "${owners[$f]}"
+done | sort -k 2 -k 1 # group by owner
+
+# restore gitignore files
+rm .gitignore
+find . -name .gitignore.bak -print0 | while IFS= read -r -d '' f; do
+    base=${f%.bak}
+    if [ -e "$base" ]; then
+        >&2 echo "$base exists!"
+    else
+        mv "$f" "$base"
+    fi
+done
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 62fdaec802..70a9756e51 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -23,7 +23,7 @@
 
 ;; If you load this file from a git repository, checking out an old
 ;; commit will make it disappear and cause errors for your Emacs
-;; startup. To ignore those errors use (require 'coqdev nil t). If you
+;; startup.  To ignore those errors use (require 'coqdev nil t).  If you
 ;; check out a malicious commit Emacs startup would allow it to run
 ;; arbitrary code, to avoid this you can copy coqdev.el to any
 ;; location and adjust the load path accordingly (of course if you run
@@ -103,5 +103,48 @@ Note that this function is executed before _Coqproject is read if it exists."
      2 (3 . 4) (5 . 6)))
   (add-to-list 'compilation-error-regexp-alist 'coq-backtrace))
 
+(defvar bug-reference-bug-regexp)
+(defvar bug-reference-url-format)
+(defun coqdev-setup-bug-reference-mode ()
+  "Setup `bug-reference-bug-regexp' and `bug-reference-url-format' for Coq.
+
+This does not enable `bug-reference-mode'."
+  (let ((dir (coqdev-default-directory)))
+    (when dir
+      (setq-local bug-reference-bug-regexp "#\\(?2:[0-9]+\\)")
+      (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s"))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode)
+
+(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end)
+  "Add LEFT and RIGHT around the BEG..END.
+Leave the point after RIGHT.  BEG and END default to the bounds
+of the current region.  Leave point OFFSET characters after the
+left quote (if OFFSET is nil, leave the point after the right
+quote)."
+  (unless beg
+    (if (region-active-p)
+        (setq beg (region-beginning) end (region-end))
+      (setq beg (point) end nil)))
+  (save-excursion
+    (goto-char (or end beg))
+    (insert right))
+  (save-excursion
+    (goto-char beg)
+    (insert left))
+  (if (and end (not offset)) ;; Second test handles the ::`` case
+      (goto-char (+ end (length left) (length right)))
+    (goto-char (+ beg (or offset (length left))))))
+
+(defun coqdev-sphinx-rst-coq-action ()
+  "Insert a Sphinx role template or quote the current region."
+  (interactive)
+  (pcase (read-char "Command [gntm:`]?")
+    (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`"))
+    (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`"))
+    (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`"))
+    (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`"))
+    (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1))
+    (?` (coqdev-sphinx-quote-coq-refman-region "``" "``"))))
+
 (provide 'coqdev)
 ;;; coqdev ends here