aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/build/windows/makecoq_mingw.sh29
-rw-r--r--dev/build/windows/patches_coq/lablgtk-2.18.3.patch44
-rw-r--r--dev/ci/README.md102
-rwxr-xr-xdev/ci/ci-basic-overlay.sh12
-rw-r--r--dev/ci/ci-common.sh4
-rwxr-xr-xdev/ci/ci-compcert.sh1
-rwxr-xr-xdev/ci/ci-cross-crypto.sh11
-rwxr-xr-xdev/ci/ci-pidetop.sh13
-rwxr-xr-xdev/ci/ci-vst.sh6
-rw-r--r--dev/ci/docker/README.md65
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile46
-rwxr-xr-xdev/ci/docker/bionic_coq/hooks/post_push8
-rw-r--r--dev/ci/gitlab.bat50
-rw-r--r--dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh6
-rw-r--r--dev/doc/MERGING.md5
-rw-r--r--dev/doc/changes.md11
-rwxr-xr-xdev/tools/check-owners-pr.sh32
-rwxr-xr-xdev/tools/check-owners.sh138
-rw-r--r--dev/tools/coqdev.el45
-rwxr-xr-xdev/tools/pre-commit6
-rw-r--r--dev/top_printers.mli2
21 files changed, 566 insertions, 70 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 18f1a2f165..3608f7305d 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -144,24 +144,24 @@ LOGTARGET=other
# Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
log1() {
- "$@" > "$LOGS/$LOGTARGET-$1.log" 2> "$LOGS/$LOGTARGET-$1.err"
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1.log" | sed -e "s/^/$LOGTARGET-$1.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1.err" | sed -e "s/^/$LOGTARGET-$1.err: /" 1>&2)
}
# Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
log2() {
- "$@" > "$LOGS/$LOGTARGET-$1-$2.log" 2> "$LOGS/$LOGTARGET-$1-$2.err"
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2.log" | sed -e "s/^/$LOGTARGET-$1-$2.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2.err" | sed -e "s/^/$LOGTARGET-$1-$2.err: /" 1>&2)
}
# Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
log_1_3() {
- "$@" > "$LOGS/$LOGTARGET-$1-$3.log" 2> "$LOGS/$LOGTARGET-$1-$3.err"
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3.log" | sed -e "s/^/$LOGTARGET-$1-$3.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3.err" | sed -e "s/^/$LOGTARGET-$1-$3.err: /" 1>&2)
}
# Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
logn() {
LOGTARGETEX=$1
shift
- "$@" > "$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2> "$LOGS/$LOGTARGET-$LOGTARGETEX.err"
+ "$@" > >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.log" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.log: /") 2> >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.err" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.err: /" 1>&2)
}
###################### 'UNFIX' SED #####################
@@ -954,11 +954,26 @@ function make_lablgtk {
# lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
- # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html for the make || true + strip
- logn make-world-pre make world || true
- "$TARGET_ARCH-strip.exe" --strip-unneeded src/dlllablgtk2.dll
+ # lablgtk binary needs to be stripped - otherwise flexdll goes wild
+ # Fix version 1: explicit strip after failed build - this randomly fails in CI
+ # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html
+ # logn make-world-pre make world || true
+ # $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll
+
+ # Fix version 2: Strip by passing linker argument rather than explicit call to strip
+ # See https://github.com/alainfrisch/flexdll/issues/6
+ # Argument to ocamlmklib: -ldopt "-link -Wl,-s"
+ # -ldopt is the okamlmklib linker prefix option
+ # -link is the flexlink linker prefix option
+ # -Wl, is the gcc (linker driver) linker prefix option
+ # -s is the gnu linker option for stripping symbols
+ # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch
log2 make world
+
+ # lablgtk does not escape FINDLIBDIR path, which can contain backslashes
+ sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make
+
log2 make install
log2 make clean
build_post
diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
index 0691c1fc8f..23c303135d 100644
--- a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
+++ b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
@@ -1,6 +1,12 @@
-diff -u -r lablgtk-2.18.3/configure lablgtk-2.18.3.patched/configure
---- lablgtk-2.18.3/configure 2014-10-29 08:51:05.000000000 +0100
-+++ lablgtk-2.18.3.patched/configure 2015-10-29 08:58:08.543985500 +0100
+diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with:
+difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1
+TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz
+FOLDER= lablgtk-2.18.3
+TARSTRIP= 1
+TARPREFIX= lablgtk-2.18.3/
+ORIGFOLDER= lablgtk-2.18.3.orig
+--- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100
++++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200
@@ -2667,7 +2667,7 @@
fi
@@ -10,10 +16,8 @@ diff -u -r lablgtk-2.18.3/configure lablgtk-2.18.3.patched/configure
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5
$as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;}
OCAMLFIND=no
-
-diff -u -r lablgtk-2.18.3/src/glib.mli lablgtk-2.18.3.patched/src/glib.mli
---- lablgtk-2.18.3/src/glib.mli 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3.patched/src/glib.mli 2016-01-25 09:50:59.884715200 +0100
+--- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200
@@ -75,6 +75,7 @@
type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
type id
@@ -22,10 +26,8 @@ diff -u -r lablgtk-2.18.3/src/glib.mli lablgtk-2.18.3.patched/src/glib.mli
val add_watch :
cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
val remove : id -> unit
-
-diff -u -r lablgtk-2.18.3/src/glib.ml lablgtk-2.18.3.patched/src/glib.ml
---- lablgtk-2.18.3/src/glib.ml 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3.patched/src/glib.ml 2016-01-25 09:50:59.891715900 +0100
+--- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200
@@ -72,6 +72,8 @@
type id
external channel_of_descr : Unix.file_descr -> channel
@@ -35,10 +37,22 @@ diff -u -r lablgtk-2.18.3/src/glib.ml lablgtk-2.18.3.patched/src/glib.ml
external remove : id -> unit = "ml_g_source_remove"
external add_watch :
cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
-
-diff -u -r lablgtk-2.18.3/src/ml_glib.c lablgtk-2.18.3.patched/src/ml_glib.c
---- lablgtk-2.18.3/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3.patched/src/ml_glib.c 2016-01-25 09:50:59.898716600 +0100
+--- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200
+@@ -461,9 +461,9 @@
+ do rm -f "$(BINDIR)"/$$f; done
+
+ lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS)
+- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
+ lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx)
+- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
+ lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS)
+
+ lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS)
+--- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200
@@ -25,6 +25,8 @@
#include <string.h>
#include <locale.h>
diff --git a/dev/ci/README.md b/dev/ci/README.md
index bb13587e94..dee3d2aff7 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -36,9 +36,8 @@ On the condition that:
- You do not push, to the branches that we test, commits that haven't been
first tested to compile with the corresponding branch(es) of Coq.
-- Your development compiles in less than 35 minutes with just two threads.
- If this is not the case, consider adding a "lite" target that compiles just
- part of it.
+- You maintain a reasonable build time for your development, or you provide
+ a "lite" target that we can use.
In case you forget to comply with these last three conditions, we would reach
out to you and give you a 30-day grace period during which your development
@@ -54,9 +53,10 @@ Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at
set the corresponding variables in
[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding
target to [`Makefile.ci`](/Makefile.ci); add new jobs to
-[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that
-this new target is run. **Do not hesitate to submit an incomplete pull request
-if you need help to finish it.**
+[`.gitlab-ci.yml`](/.gitlab-ci.yml),
+[`.circleci/config.yml`](/.circleci/config.yml) and
+[`.travis.yml`](/.travis.yml) so that this new target is run. **Do not
+hesitate to submit an incomplete pull request if you need help to finish it.**
You may also be interested in having your development tested in our
performance benchmark. Currently this is done by providing an OPAM package
@@ -71,24 +71,39 @@ When you submit a pull request (PR) on Coq GitHub repository, this will
automatically launch a battery of CI tests. The PR will not be integrated
unless these tests pass.
-Currently, we have two CI platforms:
+We are currently running tests on the following platforms:
-- Travis is the main CI platform. It tests the compilation of Coq, of the
+- GitLab CI is the main CI platform. It tests the compilation of Coq, of the
documentation, and of CoqIDE on Linux with several versions of OCaml /
camlp5, and with warnings as errors; it runs the test-suite and tests the
- compilation of several external developments. It also tests the compilation
- of Coq on OS X.
+ compilation of several external developments.
+
+- Circle CI runs tests that are redundant with GitLab CI and may be removed
+ eventually.
+
+- Travis CI is used to test the compilation of Coq and run the test-suite on
+ macOS. It also runs a linter that checks whitespace discipline. A
+ [pre-commit hook](/dev/tools/pre-commit) is automatically installed by
+ `./configure`. It should allow complying with this discipline without pain.
- AppVeyor is used to test the compilation of Coq and run the test-suite on
Windows.
-You can anticipate the results of these tests prior to submitting your PR
-by having them run of your fork of Coq, on GitHub or GitLab. This can be
-especially helpful given that our Travis platform is often overloaded and
-therefore there can be a significant delay before these tests are actually
-run on your PR. To take advantage of this, simply create a Travis account
-and link it to your GitHub account, or activate the pipelines on your GitLab
-fork.
+You can anticipate the results of most of these tests prior to submitting your
+PR by running GitLab CI on your private branches. To do so follow these steps:
+
+1. Log into GitLab CI (the easiest way is to sign in with your GitHub account).
+2. Click on "New Project".
+3. Choose "CI / CD for external repository" then click on "GitHub".
+4. Find your fork of the Coq repository and click on "Connect".
+5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project).
+6. You are encouraged to go to the CI / CD general settings and increase the
+ timeout from 1h to 2h for better reliability.
+
+Now everytime you push (including force-push unless you changed the default
+GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and
+CI will be run. You will receive an e-mail with a report of the failures if
+there are some.
You can also run one CI target locally (using `make ci-somedev`).
@@ -97,36 +112,53 @@ so that it doesn't, or provide a branch fixing these developments (or at
least work with the author of the development / other Coq developers to
prepare these fixes). Then, add an overlay in
[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there)
-in a separate commit in your PR.
+as part of your PR.
The process to merge your PR is then to submit PRs to the external
development repositories, merge the latter first (if the fixes are
-backward-compatible), drop the overlay commit and merge the PR on Coq then.
+backward-compatible), and merge the PR on Coq then.
See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
-Travis specific information
----------------------------
+Advanced GitLab CI information
+------------------------------
-Travis rebuilds all of Coq's executables and stdlib for each job. Coq
-is built with `./configure -local`, then used for the job's test.
-
-
-GitLab specific information
----------------------------
-
-GitLab is set up to use the "build artifact" feature to avoid
-rebuilding Coq. In one job, Coq is built with `./configure -prefix
-install` and `make install` is run, then the `install` directory
+GitLab CI is set up to use the "build artifact" feature to avoid
+rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci`
+and `make install` is run, then the `_install_ci` directory
persists to and is used by the next jobs.
Artifacts can also be downloaded from the GitLab repository.
Currently, available artifacts are:
- the Coq executables and stdlib, in three copies varying in
- architecture and Ocaml version used to build Coq.
-- the Coq documentation, in two different copies varying in the OCaml
- version used to build Coq
+ architecture and OCaml version used to build Coq.
+- the Coq documentation, built only in the `build:base` job. When submitting
+ a documentation PR, this can help reviewers checking the rendered result.
As an exception to the above, jobs testing that compilation triggers
-no Ocaml warnings build Coq in parallel with other tests.
+no OCaml warnings build Coq in parallel with other tests.
+
+### GitLab and Windows
+
+
+If your repository has access to runners tagged `windows`, setting the
+secret variable `WINDOWS` to `enabled` will add jobs building Windows
+versions of Coq (32bit and 64bit).
+
+The Windows jobs are enabled on Coq's repository, where pipelines for
+pull requests run.
+
+### GitLab and Docker
+
+System and opam packages are installed in a Docker image. The image is
+automatically built and uploaded to your GitLab registry, and is
+loaded by subsequent jobs.
+
+The Docker building job reuses the uploaded image if it is available,
+but if you wish to save more time you can skip the job by setting
+`SKIP_DOCKER` to `true`.
+
+This means you will need to change its value when the Docker image
+needs to be updated. You can do so for a single pipeline by starting
+it through the web interface.
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5cee72cc73..b7faea13ed 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -91,6 +91,12 @@
: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}"
########################################################################
+# cross-crypto
+########################################################################
+: "${cross_crypto_CI_BRANCH:=master}"
+: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}"
+
+########################################################################
# fiat_parsers
########################################################################
: "${fiat_parsers_CI_BRANCH:=master}"
@@ -156,3 +162,9 @@
########################################################################
: "${fcsl_pcm_CI_BRANCH:=master}"
: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}"
+
+########################################################################
+# pidetop
+########################################################################
+: "${pidetop_CI_BRANCH:=v8.9}"
+: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 189734a0bc..2a14ed352a 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -10,6 +10,10 @@ if [ -n "${GITLAB_CI}" ];
then
export COQBIN="$PWD/_install_ci/bin"
export CI_BRANCH="$CI_COMMIT_REF_NAME"
+ if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
+ then
+ export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+ fi
else
if [ -n "${TRAVIS}" ];
then
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index fbdeff20c9..8d490591b6 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert"
-opam install -j "$NJOBS" -y menhir
git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}"
( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh
new file mode 100755
index 0000000000..a0d3aa6551
--- /dev/null
+++ b/dev/ci/ci-cross-crypto.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto"
+
+git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}"
+( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive )
+
+( cd "${cross_crypto_CI_DIR}" && make )
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
new file mode 100755
index 0000000000..d04b9637c0
--- /dev/null
+++ b/dev/ci/ci-pidetop.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop"
+
+git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
+
+( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top )
+
+echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 3c0044bfe9..79001c547b 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -8,6 +8,6 @@ VST_CI_DIR="${CI_BUILD_DIR}/VST"
# opam install -j ${NJOBS} -y menhir
git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}"
-# Targets are: msl veric floyd progs , we remove progs to save time
-# Patch to avoid the upper version limit
-( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd )
+# We have to omit progs as otherwise we timeout on Travis; on Gitlab
+# we will be able to just use `make`
+( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs )
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
new file mode 100644
index 0000000000..8e677f6f2b
--- /dev/null
+++ b/dev/ci/docker/README.md
@@ -0,0 +1,65 @@
+## Overall Docker Setup for Coq's CI.
+
+This directory provides Docker images to be used by Coq's CI. The
+images do support Docker autobuild on `hub.docker.com`
+
+Autobuild is the preferred build method [see below]; if you are a
+member of the `coqci` organization, the automated build will push the
+image to the `coqci/name:$VERSION` tag using a Docker hub hook.
+
+## Updating the Image and Syncronization with CI files
+
+Unfortunately, at this point some manual synchronization is needed
+between the `Dockerfile` and `.gitlab-ci.yml`. In particular, the
+checklist is:
+
+- check the name and version of the image setup in `hooks/post_push`
+ have to match.
+- check `COMPILER` variables do match.
+
+Once you are sure the variables are right, then proceed to trigger an
+autobuild or do a manual build, et voilà !
+
+## Docker Autobuilding.
+
+We provide basic support for auto-building, see:
+
+https://docs.docker.com/docker-cloud/builds/advanced/
+
+If you are member of the `coqci` Docker organization, trigger an
+autobuild in your account and the image will be pushed to it as we
+set the proper tag in `hooks/post_push`.
+
+We still need to figure out how properly setup a more automated,
+organization-wide auto-building process.
+
+## Manual Building
+
+You can also manually build and push any image:
+
+- Build the image `docker build -t base:$VERSION .`
+
+To upload/push to your hub:
+
+- Create a https://hub.docker.com account.
+- Login into your space `docker login --username=$USER`
+- Push the image:
+ + `docker tag base:$VERSION $USER/base:$VERSION`
+ + `docker push $USER/base:$VERSION`
+
+Now your docker image is ready to be used. To upload to `coqci`:
+- `docker tag base:$VERSION coqci/base:$VERSION`
+- `docker push coqci/base:$VERSION`
+
+## Debugging / Misc
+
+To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>`
+
+Each `RUN` command creates an "layer", thus a Docker build is
+incremental and it always help to put things updated more often at the
+end.
+
+## Possible Improvements:
+
+- Use ARG for customizing versions, centralize variable setup;
+- Learn more about Docker registry for GITLAB https://gitlab.com/coq/coq/container_registry .
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
new file mode 100644
index 0000000000..689d203a16
--- /dev/null
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -0,0 +1,46 @@
+FROM ubuntu:bionic
+LABEL maintainer="e@x80.org"
+
+ENV DEBIAN_FRONTEND="noninteractive"
+
+RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \
+ libgtk2.0-dev libgtksourceview2.0-dev \
+ texlive-latex-extra texlive-fonts-recommended hevea \
+ python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip
+
+RUN pip3 install antlr4-python3-runtime
+
+# Basic OPAM setup
+ENV NJOBS="2" \
+ OPAMROOT=/root/.opamcache \
+ OPAMROOTISOK="true"
+
+# Base opam is the set of base packages required by Coq
+ENV COMPILER="4.02.3" \
+ BASE_OPAM="num ocamlfind jbuilder ounit"
+
+RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update
+
+# Setup of the base switch; CI_OPAM contains Coq's CI dependencies.
+ENV CAMLP5_VER="6.14" \
+ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" \
+ CI_OPAM="menhir elpi ocamlgraph"
+
+RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \
+ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
+
+# base+32bit switch
+RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
+ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER
+
+# BE switch
+ENV COMPILER_BE="4.06.1" \
+ CAMLP5_VER_BE="7.05" \
+ COQIDE_OPAM_BE="lablgtk.2.18.6 conf-gtksourceview.2"
+
+RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \
+ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE
+
+# BE+flambda switch
+RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \
+ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE $CI_OPAM
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
new file mode 100755
index 0000000000..307680aa51
--- /dev/null
+++ b/dev/ci/docker/bionic_coq/hooks/post_push
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+COQCI_VERSION=V2018-05-07-V2
+docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION
+docker push $DOCKER_REPO:$COQCI_VERSION
+
+docker tag $IMAGE_NAME coqci/base:$COQCI_VERSION
+docker push coqci/base:$COQCI_VERSION
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
new file mode 100644
index 0000000000..70278e6d09
--- /dev/null
+++ b/dev/ci/gitlab.bat
@@ -0,0 +1,50 @@
+@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+if %ARCH% == 32 (
+ SET ARCHLONG=i686
+ SET CYGROOT=C:\cygwin
+ SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+ SET ARCHLONG=x86_64
+ SET CYGROOT=C:\cygwin64
+ SET SETUP=setup-x86_64.exe
+)
+
+powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
+SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
+SET DESTCOQ=C:\coq%ARCH%_inst
+SET COQREGTESTING=Y
+SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
+
+if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
+if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+
+call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+ -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
+ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+ -addon=bignums -make=N ^
+ -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
+7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+
+REM DO NOT echo the signing command below, as this would leak secrets in the logs
+IF DEFINED WIN_CERTIFICATE_PATH (
+ IF DEFINED WIN_CERTIFICATE_PASSWORD (
+ ECHO Signing package
+ @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
+ signtool verify /pa dev\nsis\*.exe
+ )
+)
+
+GOTO :EOF
+
+:ErrorExit
+ ECHO ERROR %0 failed
+ EXIT /b 1
diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
new file mode 100644
index 0000000000..517088a247
--- /dev/null
+++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then
+
+ ltac2_CI_BRANCH=fast-constr-match-no-context
+ ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 84ff94c66a..a466124c1c 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -109,9 +109,8 @@ There are two cases to consider:
The merge script passes option `-S` to `git merge` to ensure merge commits
are signed. Consequently, it depends on the GnuPG command utility being
-installed and a GPG key being available. Here is a short tutorial to
-creating your own GPG key:
-<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/>
+installed and a GPG key being available. Here is a short documentation on
+how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/.
The script depends on a few other utilities. If you are a Nix user, the
simplest way of getting them is to run `nix-shell` first.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 2bad21bb20..6d7c0d3688 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -4,7 +4,7 @@
Proof engine
- More functions have been changed to use `EConstr`, notably the
+- More functions have been changed to use `EConstr`, notably the
functions in `Evd`, and in particular `Evd.define`.
Note that the core function `EConstr.to_constr` now _enforces_ by
@@ -18,6 +18,10 @@ Proof engine
that setting this flag to false is deprecated so it is only meant to
be used as to help port pre-EConstr code.
+- A few type alias have been deprecated, in all cases the message
+ should indicate what the canonical form is. An important change is
+ the move of `Globnames.global_reference` to `Names.GlobRef.t`.
+
## Changes between Coq 8.7 and Coq 8.8
### Bug tracker
@@ -94,6 +98,11 @@ Declaration of printers for arguments used only in vernac command
happen. An alternative is to register the corresponding argument as
a value, using "Geninterp.register_val0 wit None".
+Types Alias deprecation and type relocation.
+
+- A few type alias have been deprecated, in all cases the message
+ should indicate what the canonical form is.
+
### STM API
The STM API has seen a general overhaul. The main change is the
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
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index b56925c370..ad2f2f93e7 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -14,9 +14,9 @@ then
# 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")
+ 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.)"
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index dad6dcc1c0..c23ba964c2 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -87,7 +87,7 @@ val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit
val ppclosedglobconstridmap :
Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit
-val ppglobal : Globnames.global_reference -> unit
+val ppglobal : Names.GlobRef.t -> unit
val ppconst :
Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 00:41:35 +0000