From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- dev/tools/Makefile.devel | 74 --------------------- dev/tools/Makefile.dir | 131 ------------------------------------- dev/tools/Makefile.subdir | 7 -- dev/tools/anomaly-traces-parser.el | 28 -------- dev/tools/backport-pr.sh | 74 +++++++++++++++++++++ dev/tools/check-eof-newline.sh | 41 ++++++++++++ dev/tools/coqdev.el | 107 ++++++++++++++++++++++++++++++ dev/tools/github-check-prs.py | 47 +++++++++++++ dev/tools/merge-pr.sh | 50 ++++++++++++++ dev/tools/pre-commit | 73 +++++++++++++++++++++ dev/tools/sudo-apt-get-update.sh | 4 ++ 11 files changed, 396 insertions(+), 240 deletions(-) delete mode 100644 dev/tools/Makefile.devel delete mode 100644 dev/tools/Makefile.dir delete mode 100644 dev/tools/Makefile.subdir delete mode 100644 dev/tools/anomaly-traces-parser.el create mode 100755 dev/tools/backport-pr.sh create mode 100755 dev/tools/check-eof-newline.sh create mode 100644 dev/tools/coqdev.el create mode 100755 dev/tools/github-check-prs.py create mode 100755 dev/tools/merge-pr.sh create mode 100755 dev/tools/pre-commit create mode 100755 dev/tools/sudo-apt-get-update.sh (limited to 'dev/tools') 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 \ - @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=" -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 [--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 $? -- cgit v1.2.3