aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-elpi.sh10
-rw-r--r--dev/ci/user-overlays/06745-ejgallego-located+vernac.sh13
-rw-r--r--dev/doc/build-system.txt4
-rw-r--r--dev/doc/changes.md8
-rw-r--r--dev/header10
-rwxr-xr-xdev/tools/check-eof-newline.sh31
-rw-r--r--dev/tools/coqdev.el3
-rwxr-xr-xdev/tools/pre-commit73
9 files changed, 150 insertions, 8 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 784da6f97..48e01e9e9 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -144,3 +144,9 @@
########################################################################
: "${Equations_CI_BRANCH:=8.8+alpha}"
: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}"
+
+########################################################################
+# Elpi
+########################################################################
+: "${Elpi_CI_BRANCH:=coq-master}"
+: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}"
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
new file mode 100755
index 000000000..c44e0a655
--- /dev/null
+++ b/dev/ci/ci-elpi.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Elpi_CI_DIR=${CI_BUILD_DIR}/elpi
+
+git_checkout ${Elpi_CI_BRANCH} ${Elpi_CI_GITURL} ${Elpi_CI_DIR}
+
+( cd ${Elpi_CI_DIR} && make && make install )
diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
new file mode 100644
index 000000000..d1d61fec2
--- /dev/null
+++ b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
@@ -0,0 +1,13 @@
+if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then
+ ltac2_CI_BRANCH=located+vernac
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=located+vernac
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ fiat_parsers_CI_BRANCH=located+vernac
+ fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+ Elpi_CI_BRANCH=located+vernac
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+fi
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 1c4fd2eba..fd3101613 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -143,7 +143,9 @@ file list(s):
These files are also used by the experimental ocamlbuild plugin,
which is quite touchy about them : be careful with order,
duplicated entries, whitespace errors, and do not mention .mli there.
- - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
+ If module B depends on module A, then B should be after A in the .mllib
+ file.
+- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
- The definitions in Makefile.common might have to be adapted too.
- If your file needs a specific rule, add it to Makefile.build
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 16a31790a..ab78b0956 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -49,6 +49,14 @@ We changed the type of the following functions:
a functional way. The old style of passing `evar_map`s as references
is not supported anymore.
+Changes in the abstract syntax tree:
+
+- The practical totality of the AST has been nodified using
+ `CAst.t`. This means that all objects coming from parsing will be
+ indeed wrapped in a `CAst.t`. `Loc.located` is on its way to
+ deprecation. Some minor interfaces changes have resulted from
+ this.
+
We have changed the representation of the following types:
- `Lib.object_prefix` is now a record instead of a nested tuple.
diff --git a/dev/header b/dev/header
index bf7bdc169..7c3ee6004 100644
--- a/dev/header
+++ b/dev/header
@@ -1,7 +1,9 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
index 9e4c8661d..e244d9ab8 100755
--- a/dev/tools/check-eof-newline.sh
+++ b/dev/tools/check-eof-newline.sh
@@ -1,13 +1,40 @@
#!/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
- echo "No newline at end of file $f!"
- CODE=1
+ 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
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 8c55be283..62fdaec80 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -39,7 +39,8 @@
(defun coqdev-setup-compile-command ()
"Setup `compile-command' for Coq development."
(let ((dir (coqdev-default-directory)))
- (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir))))))
+ ;; 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)
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
new file mode 100755
index 000000000..c9cdee84a
--- /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.XXXXX")
+ fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXX")
+ tree=$(mktemp "git-fix-ws-tree.XXXXX")
+ 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 --cached -R "$index"
+ git apply -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 -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 19:03:45 +0000