Imported Upstream version 8.8.2upstream/8.8.2

11 files changed, 396 insertions, 240 deletions

diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel
deleted file mode 100644
index 8dcc70cf..00000000
--- a/dev/tools/Makefile.devel
+++ /dev/null
@@ -1,74 +0,0 @@
-# to be linked to makefile (lowercase - takes precedence over Makefile)
-# in main directory
-# make devel in main directory should do this for you.
-
-TOPDIR=.
-BASEDIR=
-
-SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
-
-default:	usage noargument
-
-usage::
-	@echo Usage: make \<target\>
-	@echo Targets are:
-
-usage::
-	@echo "  setup-devel	-- set the devel makefile"
-setup-devel:
-	@ln -sfv dev/tools/Makefile.devel makefile
-	@(for i in $(SOURCEDIRS); do \
-	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \
-	done)
-
-
-usage::
-	@echo "  clean-devel	-- clear all devel files"
-clean-devel:
-	echo rm -f makefile .depend.devel
-	echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile)
-
-
-usage::
-	@echo "  coqtop	-- make until the bytecode executable, make the link"
-coqtop:	bin/coqtop.byte
-	ln -sf bin/coqtop.byte coqtop
-
-
-usage::
-	@echo "  quick		-- make bytecode executable and states"
-quick: 
-	$(MAKE) states BEST=byte
-
-include Makefile
-
-include $(TOPDIR)/dev/tools/Makefile.common
-
-# this file is better described in dev/tools/Makefile.dir
-include .depend.devel
-
-#if dev/tools/Makefile.local exists, it is included
-ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),)
-include $(TOPDIR)/dev/tools/Makefile.local
-endif
-
-
-usage::
-	@echo "  total		-- runs coqtop with all theories required"
-total:
-	ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th))))
-
-
-usage::
-	@echo "  run		-- makes and runs bytecode coqtop using ledit and the history file"
-	@echo "		   if you want to pass arguments to coqtop, use make run ARG=<args>"
-run:	$(TOPDIR)/coqtop
-	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS)
-
-
-usage::
-	@echo "  vars		-- echos commands to set COQTOP and COQBIN variables"
-vars:
-	@(cd $(TOPDIR); \
-	echo export COQTOP=`pwd`/ ; \
-	echo export COQBIN=`pwd`/bin/ )
diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir
deleted file mode 100644
index 1a1bb90b..00000000
--- a/dev/tools/Makefile.dir
+++ /dev/null
@@ -1,131 +0,0 @@
-# make a link to this file if you are working hard in one directory of Coq
-#   ln -s ../dev/tools/Makefile.dir Makefile
-# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead
-# this Makefile provides many useful facilities to develop Coq
-# it is not completely compatible with .ml4 files unfortunately
-
-ifndef TOPDIR
-TOPDIR=..
-endif
-
-# this complicated thing should work for subsubdirs as well
-BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||"))
-
-noargs:	dir
-
-test-dir:
-	@echo TOPDIR=$(TOPDIR)
-	@echo BASEDIR=$(BASEDIR)
-
-include $(TOPDIR)/dev/tools/Makefile.common
-
-# make this directory
-dir:
-	$(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR))
-
-# make all cmo's in this directory. Useful in case the main Makefile is not
-# up-to-date
-all:	
-	@( ( for i in *.ml; do \
-	       echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \
-	     done; \
-	     for i in *.ml4; do \
-	       echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \
-	     done ) \
-	  | xargs $(MAKE) -C $(TOPDIR) )
-
-# lists all files that should be compiled in this directory
-list:
-	@(for i in *.mli; do \
-	   ls -l `basename $$i .mli`.cmi; \
-	done)
-	@(for i in *.ml; do \
-	   ls -l `basename $$i .ml`.cmo; \
-	done)
-	@(for i in *.ml4; do \
-	   ls -l `basename $$i .ml4`.cmo; \
-	done)
-
-
-clean::  
-	rm -f *.cmi *.cmo *.cmx *.o
-
-
-# if grammar.cmo files cannot be compiled and main .depend cannot be
-# rebuilt, this is quite useful
-depend:
-	(cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel)
-
-
-# displays the dependency graph of the current directory (vertically,
-# unlike in doc/)
-graph:
-	(ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) &
-
-
-# the pretty entry draws a dependency graph marking red those nodes
-# which do not have their .cmo files 
-
-.INTERMEDIATE: depend.dot depend.2.dot
-.PHONY: depend.ps
-
-depend.dot:
-	ocamldep *.ml *.mli | ocamldot > $@
-
-depend.2.dot:	depend.dot
-	(i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@
-	(for ml in *.ml; do \
-	   base=`basename $$ml .ml`; \
-	   fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \
-	   rest=`echo $$base | cut -c2-`; \
-	   name=`echo $$fst $$rest | tr -d " "`; \
-	   cmo=$$base.cmo; \
-	   if [ ! -e $$cmo ]; then \
-	     echo \"$$name\" [color=red]\; >> $@;\
-	   fi;\
-         done;\
-	 echo } >> $@)
-
-depend.ps:	depend.2.dot
-	dot -Tps $< > $@
-
-clean::
-	rm -f depend.ps
-
-pretty:	depend.ps
-	(gv -spartan $<; rm $<) &
-#	gv -spartan $< &
-
-
-
-# generating file.ml.mli by tricking make to pass -i to ocamlc 
-
-%.ml.mli:	FORCE
-	@(cmo=`basename $@ .ml.mli`.cmo ; \
-	mv -f $$cmo $$cmo.tmp ; \
-	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \
-	echo Generated interface file $@ ; \
-	mv -f $$cmo.tmp $$cmo)
-
-%.annot:	FORCE
-	@(cmo=`basename $@ .annot`.cmo ; \
-	mv -f $$cmo $$cmo.tmp ; \
-	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \
-	echo Generated annotation file $@ ; \
-	mv -f $$cmo.tmp $$cmo)
-
-FORCE:
-
-clean::
-	rm -f *.ml.mli
-
-# this is not perfect but mostly WORKS! It just calls the main makefile
-
-%.cmi:	FORCE
-	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
-
-%.cmo:	FORCE
-	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
-
-coqtop:	
-	$(MAKE) -C $(TOPDIR) bin/coqtop.byte
diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir
deleted file mode 100644
index cb914bd1..00000000
--- a/dev/tools/Makefile.subdir
+++ /dev/null
@@ -1,7 +0,0 @@
-# if you work in a sub/sub-rectory of Coq
-# you should make a link to that makefile 
-#    ln -s ../../dev/tools/Makefile.subdir Makefile
-# in order to have all the facilities of dev/tools/Makefile.dir
-
-TOPDIR=../..
-include $(TOPDIR)/dev/tools/Makefile.dir
diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el
deleted file mode 100644
index 68f54266..00000000
--- a/dev/tools/anomaly-traces-parser.el
+++ /dev/null
@@ -1,28 +0,0 @@
-;; This Elisp snippet adds a regexp parser for the format of Anomaly
-;; backtraces (coqc -bt ...), to the error parser of the Compilation
-;; mode (C-c C-c: "Compile command: ..."). Once the
-;; coq-change-error-alist-for-backtraces function has run, file
-;; locations in traces are recognized and can be jumped from easily
-;; from the *compilation* buffer.
-
-;; You can just copy everything below to your .emacs and this will be
-;; enabled from any compilation command launched from an OCaml file.
-
-(defun coq-change-error-alist-for-backtraces ()
-  "Hook to change the compilation-error-regexp-alist variable, to
-   search the coq backtraces for error locations"
-  (interactive)
-  (add-to-list
-   'compilation-error-regexp-alist-alist
-   '(coq-backtrace
-     "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\
-      lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\
-      \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)"
-     2 (3 . 4) (5 . 6)))
-  (add-to-list 'compilation-error-regexp-alist 'coq-backtrace))
-
-;; this Anomaly parser should be available when one is hacking
-;; on the *OCaml* code of Coq (adding bugs), so we enable it
-;; through the OCaml mode hooks.
-(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces)
-(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces)
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
new file mode 100755
index 00000000..e4359f70
--- /dev/null
+++ b/dev/tools/backport-pr.sh
@@ -0,0 +1,74 @@
+#!/usr/bin/env bash
+
+# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging]
+
+set -e
+
+PRNUM=$1
+OPTION=$2
+
+if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
+    echo "PR #${PRNUM} does not exist."
+    exit 1
+fi
+
+SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?")
+git log master --grep "Merge PR #${PRNUM}" --format="%GG"
+if [[ "${SIGNATURE_STATUS}" != "G" ]]; then
+    echo
+    read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r
+    echo
+    if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+        exit 1
+    fi
+fi
+
+BRANCH=backport-pr-${PRNUM}
+RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../')
+MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/')
+
+if git checkout -b ${BRANCH}; then
+
+    if ! git cherry-pick -x ${RANGE}; then
+        echo "Please fix the conflicts, then exit."
+        bash
+        while ! git cherry-pick --continue; do
+            echo "Please fix the conflicts, then exit."
+            bash
+        done
+    fi
+    git checkout -
+
+else
+
+    echo
+    read -p "Skip directly to merging phase? [y/N] " -n 1 -r
+    echo
+    if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+        exit 1
+    fi
+
+fi
+
+if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+    echo
+    read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
+    echo
+    if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+        exit 1
+    fi
+fi
+
+if [[ "${OPTION}" == "--stop-before-merging" ]]; then
+    exit 0
+fi
+
+git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
+git branch -d ${BRANCH}
+
+# To-Do:
+# - Support for backporting a PR before it is merged
+# - Automatically backport all PRs in the "Waiting to be backported" column using a command like:
+# $ curl -s -H "Authorization: token ${GITHUB_TOKEN}" -H "Accept: application/vnd.github.inertia-preview+json" https://api.github.com/projects/columns/1358120/cards | jq -r '.[].content_url' | grep issue | sed 's/^.*issues\/\([0-9]*\)$/\1/' | tac
+# (The ID of the column must first be obtained through https://api.github.com/repos/coq/coq/projects then https://api.github.com/projects/819866/columns.)
+# - Then move each of the backported PR to the subsequent columns automatically as well...
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
new file mode 100755
index 00000000..e244d9ab
--- /dev/null
+++ b/dev/tools/check-eof-newline.sh
@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+
+# Usage: check-eof-newline.sh [--fix] FILES...
+# Detect missing end of file newlines for FILES.
+# Files are skipped if untracked by git and depending on gitattributes.
+# With --fix, automatically append a newline.
+# Exit status:
+# Without --fix: 1 if any file had a missing newline, 0 otherwise.
+# With --fix: 1 if any non writable file had a missing newline, 0 otherwise.
+
+FIX=
+if [ "$1" = --fix ];
+then
+   FIX=1
+   shift
+fi
+
+CODE=0
+for f in "$@"; do
+    if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \
+           git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \
+           [ -n "$(tail -c 1 "$f")" ]
+    then
+        if [ -n "$FIX" ];
+        then
+            if [ -w "$f" ];
+            then
+                echo >> "$f"
+                echo "Newline appended to file $f!"
+            else
+                echo "File $f is missing a newline and not writable!"
+                CODE=1
+            fi
+        else
+            echo "No newline at end of file $f!"
+            CODE=1
+        fi
+    fi
+done
+
+exit "$CODE"
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
new file mode 100644
index 00000000..62fdaec8
--- /dev/null
+++ b/dev/tools/coqdev.el
@@ -0,0 +1,107 @@
+;;; coqdev.el --- Emacs helpers for Coq development  -*- lexical-binding:t -*-
+
+;; Copyright (C) 2018 The Coq Development Team
+
+;; Maintainer: coqdev@inria.fr
+
+;;; Commentary:
+
+;; Helpers to set compilation commands, proof general variables, etc
+;; for Coq development
+
+;; You can disable individual features without editing this file by
+;; using `remove-hook', for instance
+;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command)
+
+;;; Installation:
+
+;; To use this, with coqdev.el located at /path/to/coqdev.el, add the
+;; following to your init:
+
+;; (add-to-list 'load-path "/path/to/coqdev/")
+;; (require 'coqdev)
+
+;; 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
+;; 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
+;; ./configure to compile Coq it is already too late).
+
+;;; Code:
+
+(defun coqdev-default-directory ()
+  "Return the Coq repository containing `default-directory'."
+  (let ((dir (locate-dominating-file default-directory "META.coq")))
+    (when dir (expand-file-name dir))))
+
+(defun coqdev-setup-compile-command ()
+  "Setup `compile-command' for Coq development."
+  (let ((dir (coqdev-default-directory)))
+    ;; we add a space at the end to make it easy to add arguments (eg -j or target)
+    (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir) " ")))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command)
+
+(defvar camldebug-command-name) ; from camldebug.el (caml package)
+(defvar ocamldebug-command-name) ; from ocamldebug.el (tuareg package)
+(defun coqdev-setup-camldebug ()
+  "Setup ocamldebug for Coq development.
+
+Specifically `camldebug-command-name' and `ocamldebug-command-name'."
+  (let ((dir (coqdev-default-directory)))
+    (when dir
+      (setq-local camldebug-command-name
+                  (concat dir "dev/ocamldebug-coq"))
+      (setq-local ocamldebug-command-name
+                  (concat dir "dev/ocamldebug-coq")))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug)
+
+(defun coqdev-setup-tags ()
+  "Setup `tags-file-name' for Coq development."
+  (let ((dir (coqdev-default-directory)))
+    (when dir (setq-local tags-file-name (concat dir "TAGS")))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-tags)
+
+(defvar coq-prog-args)
+(defvar coq-prog-name)
+
+;; Lets us detect whether there are file local variables
+;; even though PG sets it with `setq' when there's a _Coqproject.
+;; Also makes sense generally, so might make it into PG someday.
+(make-variable-buffer-local 'coq-prog-args)
+(setq-default coq-prog-args nil)
+
+(defun coqdev-setup-proofgeneral ()
+  "Setup Proofgeneral variables for Coq development.
+
+Note that this function is executed before _Coqproject is read if it exists."
+  (let ((dir (coqdev-default-directory)))
+    (when dir
+      (unless coq-prog-args
+        (setq coq-prog-args
+              `("-coqlib" ,dir "-R" ,(concat dir "plugins")
+                "Coq" "-R" ,(concat dir "theories")
+                "Coq")))
+      (setq-local coq-prog-name (concat dir "bin/coqtop")))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)
+
+;; This Elisp snippet adds a regexp parser for the format of Anomaly
+;; backtraces (coqc -bt ...), to the error parser of the Compilation
+;; mode (C-c C-c: "Compile command: ..."). File locations in traces
+;; are recognized and can be jumped from easily in the *compilation*
+;; buffer.
+(defvar compilation-error-regexp-alist-alist)
+(defvar compilation-error-regexp-alist)
+(with-eval-after-load 'compile
+  (add-to-list
+   'compilation-error-regexp-alist-alist
+   '(coq-backtrace
+     "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\
+      lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\
+      \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)"
+     2 (3 . 4) (5 . 6)))
+  (add-to-list 'compilation-error-regexp-alist 'coq-backtrace))
+
+(provide 'coqdev)
+;;; coqdev ends here
diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py
new file mode 100755
index 00000000..beb26d91
--- /dev/null
+++ b/dev/tools/github-check-prs.py
@@ -0,0 +1,47 @@
+#!/usr/bin/env python3
+
+# 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
+import argparse
+
+REPO = "coq/coq"
+REBASE_LABEL="needs: rebase"
+
+parser = argparse.ArgumentParser()
+parser.add_argument("--token-file", type=argparse.FileType('r'))
+args = parser.parse_args()
+
+if args.token_file is None:
+    token = input("Github access token: ").strip()
+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)
+
+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")
+        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")
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
new file mode 100755
index 00000000..9f24960f
--- /dev/null
+++ b/dev/tools/merge-pr.sh
@@ -0,0 +1,50 @@
+#!/usr/bin/env bash
+
+set -e
+
+# This script depends (at least) on git and jq.
+# It should be used like this: dev/tools/merge-pr.sh /PR number/
+
+#TODO: check arguments and show usage if relevant
+
+PR=$1
+
+CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
+git fetch "$REMOTE" "refs/pull/$PR/head"
+
+API=https://api.github.com/repos/coq/coq
+
+BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
+
+COMMIT=$(git rev-parse FETCH_HEAD)
+STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
+
+if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
+  echo "Wrong base branch"
+  read -p "Bypass? [y/N] " -n 1 -r
+  echo
+  if [[ ! $REPLY =~ ^[Yy]$ ]]
+  then
+    exit 1
+  fi
+fi;
+
+if [ "$STATUS" != "success" ]; then
+  echo "CI status is \"$STATUS\""
+  read -p "Bypass? [y/N] " -n 1 -r
+  echo
+  if [[ ! $REPLY =~ ^[Yy]$ ]]
+  then
+    exit 1
+  fi
+fi;
+
+git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e
+
+# TODO: improve this check
+if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
+  echo "******************************************"
+  echo "** WARNING: does this PR have overlays? **"
+  echo "******************************************"
+fi
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
new file mode 100755
index 00000000..dfa95bac
--- /dev/null
+++ b/dev/tools/pre-commit
@@ -0,0 +1,73 @@
+#!/bin/sh
+
+# configure automatically sets up a wrapper at .git/hooks/pre-commit
+# which calls this script (if it exists).
+
+set -e
+
+if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh ||
+        ! git diff-index --check --cached HEAD >/dev/null 2>&1 ;
+then
+    1>&2 echo "Auto fixing whitespace issues..."
+
+    # We fix whitespace in the index and in the working tree
+    # separately to preserve non-added changes.
+    index=$(mktemp "git-fix-ws-index.XXXXXX")
+    fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX")
+    tree=$(mktemp "git-fix-ws-tree.XXXXXX")
+    1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'."
+    1>&2 echo "If an error destroys your changes you can recover using them."
+    1>&2 echo "(The files are cleaned up on success.)"
+    1>&2 echo #newline
+
+    git diff-index -p --cached HEAD > "$index"
+    git diff-index -p HEAD > "$tree"
+
+    # reset work tree and index
+    # NB: untracked files which were not added are untouched
+    git apply --whitespace=nowarn --cached -R "$index"
+    git apply --whitespace=nowarn -R "$tree"
+
+    # Fix index
+    # For end of file newlines we must go through the worktree
+    1>&2 echo "Fixing staged changes..."
+    git apply --cached --whitespace=fix "$index"
+    git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
+    git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
+    git add -u
+    1>&2 echo #newline
+
+    # reset work tree
+    git diff-index -p --cached HEAD > "$fixed_index"
+    # If all changes were bad whitespace changes the patch is empty
+    # making git fail. Don't fail now: we fix the worktree first.
+    if [ -s "$fixed_index" ]
+    then
+        git apply --whitespace=nowarn -R "$fixed_index"
+    fi
+
+    # Fix worktree
+    1>&2 echo "Fixing unstaged changes..."
+    git apply --whitespace=fix "$tree"
+    git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
+    1>&2 echo #newline
+
+    if ! [ -s "$fixed_index" ]
+    then
+        1>&2 echo "No changes after fixing whitespace issues!"
+        exit 1
+    fi
+
+    # Check that we did fix whitespace
+    if ! git diff-index --check --cached HEAD;
+    then
+        1>&2 echo "Auto-fixing whitespace failed: errors remain."
+        1>&2 echo "This may fix itself if you try again."
+        1>&2 echo "(Consider whether the number of errors decreases after each run.)"
+        exit 1
+    fi
+    1>&2 echo "Whitespace issues fixed!"
+
+    # clean up temporary files
+    rm "$index" "$tree" "$fixed_index"
+fi
diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh
new file mode 100755
index 00000000..f8bf6bed
--- /dev/null
+++ b/dev/tools/sudo-apt-get-update.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err
+! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $?