aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include3
-rw-r--r--dev/build/windows/makecoq_mingw.sh33
-rw-r--r--dev/build/windows/patches_coq/lablgtk-2.18.3.patch44
-rw-r--r--dev/checker.dbg6
-rw-r--r--dev/checker_db39
-rw-r--r--dev/checker_printers.ml73
-rw-r--r--dev/checker_printers.mli54
-rw-r--r--dev/ci/README.md138
-rw-r--r--dev/ci/appveyor.sh2
-rwxr-xr-x[-rw-r--r--]dev/ci/ci-basic-overlay.sh28
-rw-r--r--dev/ci/ci-common.sh12
-rwxr-xr-xdev/ci/ci-compcert.sh1
-rwxr-xr-xdev/ci/ci-cross-crypto.sh11
-rwxr-xr-xdev/ci/ci-fcsl-pcm.sh12
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh5
-rwxr-xr-xdev/ci/ci-geocoq.sh4
-rwxr-xr-xdev/ci/ci-iris-lambda-rust.sh15
-rwxr-xr-xdev/ci/ci-math-classes.sh2
-rwxr-xr-xdev/ci/ci-math-comp.sh11
-rwxr-xr-xdev/ci/ci-mtac2.sh (renamed from dev/ci/ci-metacoq.sh)6
-rwxr-xr-xdev/ci/ci-pidetop.sh24
-rwxr-xr-xdev/ci/ci-unimath.sh5
-rwxr-xr-xdev/ci/ci-vst.sh5
-rw-r--r--dev/ci/docker/README.md36
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile49
-rw-r--r--dev/ci/gitlab.bat50
-rw-r--r--dev/ci/user-overlays/06859-ejgallego-stm+top.sh6
-rw-r--r--dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh12
-rw-r--r--dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh21
-rw-r--r--dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh6
-rw-r--r--dev/ci/user-overlays/README.md17
-rw-r--r--dev/core.dbg3
-rw-r--r--dev/doc/MERGING.md58
-rw-r--r--dev/doc/changes.md42
-rw-r--r--dev/doc/coq-src-description.txt6
-rw-r--r--dev/doc/debugging.md2
-rw-r--r--dev/doc/release-process.md100
-rw-r--r--dev/ocamldebug-coq.run20
-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/merge-pr.sh8
-rwxr-xr-xdev/tools/pre-commit6
-rw-r--r--dev/top_printers.ml10
-rw-r--r--dev/top_printers.mli6
45 files changed, 1033 insertions, 173 deletions
diff --git a/dev/base_include b/dev/base_include
index e76044f41..2f5d8aa84 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -15,7 +15,6 @@
#directory "tactics";;
#directory "printing";;
#directory "grammar";;
-#directory "intf";;
#directory "stm";;
#directory "vernac";;
@@ -232,7 +231,7 @@ let _ = Flags.in_toplevel := true
let _ = Constrextern.set_extern_reference
(fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
-let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
let _ =
print_string
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 18f1a2f16..ecc45735f 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 #####################
@@ -847,7 +847,7 @@ function make_ocaml {
function make_ocaml_tools {
make_findlib
- make_menhir
+ # make_menhir
make_camlp5
}
@@ -856,7 +856,7 @@ function make_ocaml_tools {
function make_ocaml_libs {
make_findlib
make_lablgtk
- make_stdint
+ # make_stdint
}
##### FINDLIB Ocaml library manager #####
@@ -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 0691c1fc8..23c303135 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/checker.dbg b/dev/checker.dbg
new file mode 100644
index 000000000..b2323b617
--- /dev/null
+++ b/dev/checker.dbg
@@ -0,0 +1,6 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer clib.cma
+load_printer dynlink.cma
+load_printer lib.cma
+load_printer check.cma
diff --git a/dev/checker_db b/dev/checker_db
new file mode 100644
index 000000000..327e636c5
--- /dev/null
+++ b/dev/checker_db
@@ -0,0 +1,39 @@
+source checker.dbg
+
+load_printer checker_printers.cmo
+
+install_printer Checker_printers.pP
+
+install_printer Checker_printers.ppfuture
+
+install_printer Checker_printers.ppid
+install_printer Checker_printers.pplab
+install_printer Checker_printers.ppmbid
+install_printer Checker_printers.ppdir
+install_printer Checker_printers.ppmp
+install_printer Checker_printers.ppcon
+install_printer Checker_printers.ppproj
+install_printer Checker_printers.ppkn
+install_printer Checker_printers.ppmind
+install_printer Checker_printers.ppind
+
+install_printer Checker_printers.ppbigint
+
+install_printer Checker_printers.ppintset
+install_printer Checker_printers.ppidset
+
+install_printer Checker_printers.ppidmapgen
+
+install_printer Checker_printers.ppididmap
+
+install_printer Checker_printers.ppuni
+install_printer Checker_printers.ppuni_level
+install_printer Checker_printers.ppuniverse_set
+install_printer Checker_printers.ppuniverse_instance
+install_printer Checker_printers.ppauniverse_context
+install_printer Checker_printers.ppuniverse_context
+install_printer Checker_printers.ppconstraints
+install_printer Checker_printers.ppuniverse_context_future
+install_printer Checker_printers.ppuniverses
+
+install_printer Checker_printers.pploc
diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml
new file mode 100644
index 000000000..40ae1a7b0
--- /dev/null
+++ b/dev/checker_printers.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(* * 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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open Names
+open Univ
+
+let pp x = Pp.pp_with Format.std_formatter x
+
+(** Future printer *)
+
+let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
+
+(* name printers *)
+let ppid id = pp (Id.print id)
+let pplab l = pp (Label.print l)
+let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
+let ppdir dir = pp (DirPath.print dir)
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
+let ppcon con = pp(Constant.debug_print con)
+let ppproj con = pp(Constant.debug_print (Projection.constant con))
+let ppkn kn = pp(str (KerName.to_string kn))
+let ppmind kn = pp(MutInd.debug_print kn)
+let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
+
+(* term printers *)
+let ppbigint n = pp (str (Bigint.to_string n));;
+
+let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
+let ppintset l = pp (prset int (Int.Set.elements l))
+let ppidset l = pp (prset Id.print (Id.Set.elements l))
+
+let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
+
+let pridmap pr l =
+ let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in
+ prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
+let ppidmap pr l = pp (pridmap pr l)
+
+let pridmapgen l =
+ let dom = Id.Set.elements (Id.Map.domain l) in
+ if dom = [] then str "[]" else
+ str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]"
+let ppidmapgen l = pp (pridmapgen l)
+
+let prididmap = pridmap (fun _ -> Id.print)
+let ppididmap = ppidmap (fun _ -> Id.print)
+
+let pP s = pp (hov 0 s)
+
+(* proof printers *)
+let ppuni u = pp(Universe.pr u)
+let ppuni_level u = pp (Level.pr u)
+
+let ppuniverse_set l = pp (LSet.pr l)
+let ppuniverse_instance l = pp (Instance.pr l)
+let ppauniverse_context l = pp (AUContext.pr Level.pr l)
+let ppuniverse_context l = pp (pr_universe_context Level.pr l)
+let ppconstraints c = pp (pr_constraints Level.pr c)
+let ppuniverse_context_future c =
+ let ctx = Future.force c in
+ ppuniverse_context ctx
+let ppuniverses u = pp (Univ.pr_universes u)
+
+let pploc x = let (l,r) = Loc.unloc x in
+ print_string"(";print_int l;print_string",";print_int r;print_string")"
diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli
new file mode 100644
index 000000000..2f9500c5c
--- /dev/null
+++ b/dev/checker_printers.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(* * 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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Printers for the ocaml toplevel. *)
+
+val pp : Pp.t -> unit
+val pP : Pp.t -> unit (* with surrounding box *)
+
+val ppfuture : 'a Future.computation -> unit
+
+val ppid : Names.Id.t -> unit
+val pplab : Names.Label.t -> unit
+val ppmbid : Names.MBId.t -> unit
+val ppdir : Names.DirPath.t -> unit
+val ppmp : Names.ModPath.t -> unit
+val ppcon : Names.Constant.t -> unit
+val ppproj : Names.Projection.t -> unit
+val ppkn : Names.KerName.t -> unit
+val ppmind : Names.MutInd.t -> unit
+val ppind : Names.inductive -> unit
+
+val ppbigint : Bigint.bigint -> unit
+
+val ppintset : Int.Set.t -> unit
+val ppidset : Names.Id.Set.t -> unit
+
+val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t
+val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit
+
+val pridmapgen : 'a Names.Id.Map.t -> Pp.t
+val ppidmapgen : 'a Names.Id.Map.t -> unit
+
+val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t
+val ppididmap : Names.Id.t Names.Id.Map.t -> unit
+
+(* Universes *)
+val ppuni : Univ.Universe.t -> unit
+val ppuni_level : Univ.Level.t -> unit (* raw *)
+val ppuniverse_set : Univ.LSet.t -> unit
+val ppuniverse_instance : Univ.Instance.t -> unit
+val ppauniverse_context : Univ.AUContext.t -> unit
+val ppuniverse_context : Univ.UContext.t -> unit
+val ppconstraints : Univ.Constraint.t -> unit
+val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
+val ppuniverses : Univ.universes -> unit
+
+val pploc : Loc.t -> unit
diff --git a/dev/ci/README.md b/dev/ci/README.md
index bb13587e9..697a160ca 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,62 +71,110 @@ 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:
-You can also run one CI target locally (using `make ci-somedev`).
+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.
-Whenever your PR breaks tested developments, you should either adapt it
-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.
+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.
-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.
+You can also run one CI target locally (using `make ci-somedev`).
See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
-
-Travis specific 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
+### Breaking changes
+
+When your PR breaks an external project we test in our CI, you must prepare a
+patch (or ask someone to prepare a patch) to fix the project:
+
+1. Fork the external project, create a new branch, push a commit adapting
+ the project to your changes.
+2. Test your pull request with your adapted version of the external project by
+ adding an overlay file to your pull request (cf.
+ [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)).
+3. Fixes to external libraries (pure Coq projects) *must* be backward
+ compatible (i.e. they should also work with the development version of Coq,
+ and the latest stable version). This will allow you to open a PR on the
+ external project repository to have your changes merged *before* your PR on
+ Coq can be integrated.
+
+ On the other hand, patches to plugins (projects linking to the Coq ML API)
+ can very rarely be made backward compatible and plugins we test will
+ generally have a dedicated branch per Coq version.
+ You can still open a pull request but the merging will be requested by the
+ developer who merges the PR on Coq. There are plans to improve this, cf.
+ [#6724](https://github.com/coq/coq/issues/6724).
+
+Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file.
+
+Advanced GitLab CI information
+------------------------------
+
+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.
+
+**IMPORTANT**: When updating Coq's CI docker image, you must modify
+the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`,
+and `Dockerfile`.
+
+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/appveyor.sh b/dev/ci/appveyor.sh
index 93e7bd99a..c72705c7f 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -5,5 +5,5 @@ tar -xf opam64.tar.xz
bash opam64/install.sh
opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
eval "$(opam config env)"
-opam install -y ocamlfind camlp5
+opam install -y ocamlfind camlp5 ounit
cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 48e01e9e9..5c882ee85 100644..100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -11,6 +11,8 @@
########################################################################
: "${mathcomp_CI_BRANCH:=master}"
: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}"
+: "${oddorder_CI_BRANCH:=master}"
+: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}"
########################################################################
# UniMath
@@ -19,13 +21,13 @@
: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
########################################################################
-# Unicoq + Metacoq
+# Unicoq + Mtac2
########################################################################
: "${unicoq_CI_BRANCH:=master}"
: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}"
-: "${metacoq_CI_BRANCH:=master}"
-: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
+: "${mtac2_CI_BRANCH:=master-sync}"
+: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}"
########################################################################
# Mathclasses + Corn
@@ -91,6 +93,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}"
@@ -142,7 +150,7 @@
########################################################################
# Equations
########################################################################
-: "${Equations_CI_BRANCH:=8.8+alpha}"
+: "${Equations_CI_BRANCH:=master}"
: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}"
########################################################################
@@ -150,3 +158,15 @@
########################################################################
: "${Elpi_CI_BRANCH:=coq-master}"
: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}"
+
+########################################################################
+# fcsl-pcm
+########################################################################
+: "${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 189734a0b..f867fd189 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
@@ -67,11 +71,6 @@ git_checkout()
echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
}
-checkout_mathcomp()
-{
- git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}"
-}
-
make()
{
# +x: add x only if defined
@@ -89,7 +88,8 @@ install_ssreflect()
{
echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
- checkout_mathcomp "${mathcomp_CI_DIR}"
+ git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
( cd "${mathcomp_CI_DIR}/mathcomp" && \
sed -i.bak '/ssrtest/d' Make && \
sed -i.bak '/odd_order/d' Make && \
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index fbdeff20c..8d490591b 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 000000000..a0d3aa655
--- /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-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh
new file mode 100755
index 000000000..fdc4c729b
--- /dev/null
+++ b/dev/ci/ci-fcsl-pcm.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+fcsl_pcm_CI_DIR="${CI_BUILD_DIR}/fcsl-pcm"
+
+install_ssreflect
+
+git_checkout "${fcsl_pcm_CI_BRANCH}" "${fcsl_pcm_CI_GITURL}" "${fcsl_pcm_CI_DIR}"
+
+( cd "${fcsl_pcm_CI_DIR}" && make )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 6c8dce5bd..feabf72d4 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -6,6 +6,9 @@ ci_dir="$(dirname "$0")"
fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto"
git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}"
+
( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
-( cd "${fiat_crypto_CI_DIR}" && make lite )
+fiat_crypto_CI_TARGETS1="printlite lite lite-display"
+fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index bd1d88993..920272bcf 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,6 +7,4 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
-( cd "${GeoCoq_CI_DIR}" && \
- ./configure-ci.sh && \
- make )
+( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index b019fa059..1af0f634c 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -9,27 +9,20 @@ lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust"
install_ssreflect
-# Add or update the opam repo we need for dependency resolution
-opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev
-
# Setup lambdaRust first
git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}"
# Extract required version of Iris
-Iris_VERSION=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o)
-Iris_URL=$(opam show "coq-iris.$Iris_VERSION" -f upstream-url)
-read -r -a Iris_URL_PARTS <<< "$(echo "$Iris_URL" | tr '#' ' ')"
+Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
# Setup Iris
-git_checkout "${Iris_CI_BRANCH}" "${Iris_URL_PARTS[0]}" "${Iris_CI_DIR}" "${Iris_URL_PARTS[1]}"
+git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}"
# Extract required version of std++
-stdpp_VERSION=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o)
-stdpp_URL=$(opam show "coq-stdpp.$stdpp_VERSION" -f upstream-url)
-read -r -a stdpp_URL_PARTS <<< "$(echo "$stdpp_URL" | tr '#' ' ')"
+stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
# Setup std++
-git_checkout "${stdpp_CI_BRANCH}" "${stdpp_URL_PARTS[0]}" "${stdpp_CI_DIR}" "${stdpp_URL_PARTS[1]}"
+git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}"
# Build std++
( cd "${stdpp_CI_DIR}" && make && make install )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 4fc06e895..6a064b297 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -7,4 +7,4 @@ math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes"
git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}"
-( cd "${math_classes_CI_DIR}" && make && make install )
+( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 8c6b910bb..20328baf2 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -5,11 +5,10 @@ ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
+oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order"
-checkout_mathcomp "${mathcomp_CI_DIR}"
+git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}"
-# odd_order takes too much time for travis.
-( cd "${mathcomp_CI_DIR}/mathcomp" && \
- sed -i.bak '/PFsection/d' Make && \
- sed -i.bak '/stripped_odd_order_theorem/d' Make && \
- make Makefile.coq && make -f Makefile.coq all )
+( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install )
+( cd "${oddorder_CI_DIR}/" && make )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-mtac2.sh
index a66dc1e76..1372acb8e 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
+mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
# Setup UniCoq
@@ -14,6 +14,6 @@ git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
# Setup MetaCoq
-git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}"
+git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
-( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
+( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
new file mode 100755
index 000000000..2ac4d2167
--- /dev/null
+++ b/dev/ci/ci-pidetop.sh
@@ -0,0 +1,24 @@
+#!/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}"
+
+# Travis / Gitlab have different filesystem layout due to use of
+# `-local`. We need to improve this divergence but if we use Dune this
+# "local" oddity goes away automatically so not bothering...
+if [ -d "$COQBIN/../lib/coq" ]; then
+ COQOCAMLLIB="$COQBIN/../lib/"
+ COQLIB="$COQBIN/../lib/coq/"
+else
+ COQOCAMLLIB="$COQBIN/../"
+ COQLIB="$COQBIN/../"
+fi
+
+( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install )
+
+echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 62a949f59..aa20fe1ff 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -7,7 +7,4 @@ UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath"
git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}"
-( cd "${UniMath_CI_DIR}" && \
- sed -i.bak '/Folds/d' Makefile && \
- sed -i.bak '/HomologicalAlgebra/d' Makefile && \
- make BUILD_COQ=no )
+( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 3c0044bfe..7a097eaab 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -5,9 +5,6 @@ ci_dir="$(dirname "$0")"
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 )
+( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true )
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
new file mode 100644
index 000000000..919e2a735
--- /dev/null
+++ b/dev/ci/docker/README.md
@@ -0,0 +1,36 @@
+## 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` and Gitlab's
+private registry.
+
+Gitlab CI will build and tag a Docker by default for every job if the
+`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this
+variable is usually set to `false` indeed to avoid booting a useless
+job.
+
+## 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`
+
+## 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;
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
new file mode 100644
index 000000000..a1178ee2a
--- /dev/null
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -0,0 +1,49 @@
+# CACHEKEY: "bionic_coq-V2018-05-07-V2"
+# ^^ Update when modifying this file.
+
+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/gitlab.bat b/dev/ci/gitlab.bat
new file mode 100644
index 000000000..70278e6d0
--- /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/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
new file mode 100644
index 000000000..ca0076b46
--- /dev/null
+++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then
+ pidetop_CI_BRANCH=stm+top
+ pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git
+fi
diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh
new file mode 100644
index 000000000..7e554684e
--- /dev/null
+++ b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; then
+
+ # Equations_CI_BRANCH=ssr+correct_packing
+ # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ # ltac2_CI_BRANCH=ssr+correct_packing
+ # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Elpi_CI_BRANCH=api+vernac_expr_iso
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+fi
diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
new file mode 100644
index 000000000..ea9cd8ee0
--- /dev/null
+++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then
+
+ # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550
+ #
+ # equations
+ # ltac2
+
+ # The below developments should instead use a backwards compatible fix.
+ #
+ # color
+ # iris-lambda-rust
+ # math-classes
+ # formal-topology
+
+ ltac2_CI_BRANCH=tactics+push_fix_naming_out
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=tactics+push_fix_naming_out
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
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 000000000..517088a24
--- /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/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index a7474e324..aec2dfe0a 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,8 +1,21 @@
# Add overlays for your pull requests in this directory
-An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+When your pull request breaks an external project we test in our CI and you
+have prepared a branch with the fix, you can add an "overlay" to your pull
+request to test it with the adapted version of the external project.
-The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+An overlay is a file which defines where to look for the patched version so that
+testing is possible. It redefines some variables from
+[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh):
+give the name of your branch using a `_CI_BRANCH` variable and the location of
+your fork using a `_CI_GITURL` variable.
+
+Moreover, the file contains very simple logic to test the pull request number
+or branch name and apply it only in this case.
+
+The name of your overlay file should start with a five-digit pull request
+number, followed by a dash, anything (for instance your GitHub nickname
+and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
Example: `00669-maximedenes-ssr-merge.sh` containing
diff --git a/dev/core.dbg b/dev/core.dbg
index 57c136900..972ba701e 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -2,8 +2,8 @@ source camlp5.dbg
load_printer threads.cma
load_printer str.cma
load_printer clib.cma
-load_printer lib.cma
load_printer dynlink.cma
+load_printer lib.cma
load_printer kernel.cma
load_printer library.cma
load_printer engine.cma
@@ -16,5 +16,4 @@ load_printer tactics.cma
load_printer vernac.cma
load_printer stm.cma
load_printer toplevel.cma
-load_printer intf.cma
load_printer ltac_plugin.cmo
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 3a2df6a81..65457b63a 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -1,8 +1,8 @@
# Merging changes in Coq
-This document describes how patches (submitted as pull requests
-on the `master` branch) should be
-merged into the main repository (https://github.com/coq/coq).
+This document describes how patches, submitted as pull requests (PRs) on the
+`master` branch, should be merged into the main repository
+(https://github.com/coq/coq).
## Code owners
@@ -10,8 +10,8 @@ The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
system, two owners. One is the principal maintainer of the component, the other
is the secondary maintainer.
-When a pull request is submitted, GitHub will automatically ask the principal
-maintainer for a review. If the pull request touches several parts, all the
+When a PR is submitted, GitHub will automatically ask the principal
+maintainer for a review. If the PR touches several parts, all the
corresponding principal maintainers will be asked for a review.
Maintainers are never assigned as reviewer on their own PRs.
@@ -43,10 +43,31 @@ A maintainer is expected to be reasonably reactive, but no specific timeframe is
given for reviewing.
(*) In case a component is touched in a trivial way (adding/removing one file in
-a `Makefile`, etc), or by applying a systematic process (global renaming,
-deprecationg propagation, etc) that has been reviewed globally, the assignee can
+a `Makefile`, etc), or by applying a systematic refactoring process (global
+renaming for instance) that has been reviewed globally, the assignee can
say in a comment they think a review is not required and proceed with the merge.
+### Breaking changes
+
+If the PR breaks compatibility of some external projects in CI, then fixes to
+those external projects should have been prepared (cf. the relevant sub-section
+in the [CI README](/dev/ci/README.md#Breaking-changes) and the PR can be tested
+with these fixes thanks to ["overlays"](/dev/ci/user-overlays/README.md).
+
+Moreover the PR must absolutely update the [`CHANGES`](/CHANGES) file.
+
+If overlays are missing, ask the author to prepare them and label the PR with
+the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
+
+When fixes are ready, there are two cases to consider:
+
+- For patches that are backward compatible (best scenario), you should get the
+ external project maintainers to integrate them before merging the PR.
+- For patches that are not backward compatible (which is often the case when
+ patching plugins after an update to the Coq API), you can proceed to merge
+ the PR and then notify the external project maintainers they can merge the
+ patch.
+
## Merging
Once all reviewers approved the PR, the assignee is expected to check that CI
@@ -70,7 +91,7 @@ To merge the PR proceed in the following way
```
$ git checkout master
$ git pull
-$ dev/tools/merge-pr XXXX
+$ dev/tools/merge-pr.sh XXXX
$ git push upstream
```
where `XXXX` is the number of the PR to be merged and `upstream` is the name
@@ -89,29 +110,12 @@ DON'T USE the GitHub interface for merging, since it will prevent the automated
backport script from operating properly, generates bad commit messages, and a
messy history when there are conflicts.
-### What to do if the PR has overlays
-
-If the PR breaks compatibility of some developments in CI, then the author must
-have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md))
-and the PR must absolutely update the `CHANGES` file.
-
-There are two cases to consider:
-
-- If the patch is backward compatible (best scenario), then you should get
- upstream maintainers to integrate it before merging the PR.
-- If the patch is not backward compatible (which is often the case when
- patching plugins after an update to the Coq API), then you can proceed to
- merge the PR and then notify upstream they can merge the patch. This is a
- less preferable scenario because it is probably going to create
- spurious CI failures for unrelated PRs.
-
### Merge script dependencies
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 1a24f23e5..774a77c8a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,10 +2,43 @@
### ML API
+Misctypes
+
+ Syntax for universe sorts and kinds has been moved from `Misctypes`
+ to `Glob_term`, as these are turned into kernel terms by
+ `Pretyping`.
+
Proof engine
- More functions have been changed to use `EConstr`, notably the
- functions in `Evd`.
+- 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
+ default that the resulting term is ground, that is to say, free of
+ Evars. This is usually what you want, as open terms should be of
+ type `EConstr.t` to benefit from the invariants the `EConstr` API is
+ meant to guarantee.
+
+ In case you'd like to violate this API invariant, you can use the
+ `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note
+ 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`.
+
+ML Libraries used by Coq
+
+- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
+ Array.Smart.map.
+- Uniformization of some names, e.g. Array.Smart.fold_left_map instead
+ of Array.smartfoldmap.
+
+### Unit testing
+
+ The test suite now allows writing unit tests against OCaml code in the Coq
+ code base. Those unit tests create a dependency on the OUnit test framework.
## Changes between Coq 8.7 and Coq 8.8
@@ -83,6 +116,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/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index b3d49b7e5..764d48295 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -17,12 +17,6 @@ toplevel
Special components
------------------
-intf :
-
- Contains mli-only interfaces, many of them providing a.s.t.
- used for dialog bewteen coq components. Ex: Constrexpr.constr_expr
- produced by parsing and transformed by interp.
-
grammar :
Camlp5 syntax extensions. The file grammar/grammar.cma is used
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index fd3cbd1bc..14a1cc693 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -47,7 +47,7 @@ Debugging with ocamldebug from Emacs
7. some hints:
- To debug a failure/error/anomaly, add a breakpoint in
- Vernac.vernac_com at the with clause of the "try ... interp com
+ `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com
with ..." block, then go "back" a few steps to find where the
failure/error/anomaly has been raised
- Alternatively, for an error or an anomaly, add breakpoints in the middle
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
new file mode 100644
index 000000000..1821a181f
--- /dev/null
+++ b/dev/doc/release-process.md
@@ -0,0 +1,100 @@
+# Release process #
+
+## As soon as the previous version branched off master ##
+
+- [ ] Create a new issue to track the release process where you can copy-paste
+ the present checklist.
+- [ ] Change the version name to the next major version and the magic numbers
+ (see [#7008](https://github.com/coq/coq/pull/7008/files)).
+- [ ] Put the corresponding alpha tag using `git tag -s`.
+ The `VX.X+alpha` tag marks the first commit to be in `master` and not in the
+ branch of the previous version.
+- [ ] Create the `X.X+beta1` milestone if it did not already exist.
+- [ ] Decide the release calendar with the team (freeze date, beta date, final
+ release date) and put this information in the milestone (using the
+ description and due date fields).
+
+## About one month before the beta ##
+
+- [ ] Create the `X.X.0` milestone and set its due date.
+- [ ] Send an announcement of the upcoming freeze on Coqdev and ask people to
+ remove from the beta milestone what they already know won't be ready on time
+ (possibly postponing to the `X.X.0` milestone for minor bug fixes,
+ infrastructure and documentation updates).
+- [ ] Determine which issues should / must be fixed before the beta, add them
+ to the beta milestone, possibly with a
+ ["priority: blocker"](https://github.com/coq/coq/labels/priority%3A%20blocker)
+ label. Make sure that all these issues are assigned (and that the assignee
+ provides an ETA).
+- [ ] Ping the development coordinator (**@mattam82**) to get him started on
+ the update to the Credits chapter of the reference manual.
+ See also [#7058](https://github.com/coq/coq/issues/7058).
+ The command to get the list of contributors for this version is
+ `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2`
+ (the ordering is approximative as it will misplace people with middle names).
+
+## On the date of the feature freeze ##
+
+- [ ] Create the new version branch `vX.X` and
+ [protect it](https://github.com/coq/coq/settings/branches)
+ (activate the "Protect this branch", "Require pull request reviews before
+ merging" and "Restrict who can push to this branch" guards).
+- [ ] Remove all remaining unmerged feature PRs from the beta milestone.
+- [ ] Start a new project to track PR backporting. The proposed model is to
+ have a "X.X-only PRs" column for the rare PRs on the stable branch, a
+ "Request X.X inclusion" column for the PRs that were merged in `master` that
+ are to be considered for backporting, a "Waiting for CI" column to put the
+ PRs in the process of being backported, and "Shipped in ..." columns to put
+ what was backported. (The release manager is the person responsible for
+ merging PRs that target the version branch and backporting appropriate PRs
+ that are merged into `master`).
+ A message to **@coqbot** in the milestone description tells it to
+ automatically add merged PRs to the "Request X.X inclusion" column.
+- [ ] Delay non-blocking issues to the appropriate milestone and ensure
+ blocking issues are solved. If required to solve some blocking issues,
+ it is possible to revert some feature PRs in the version branch only.
+
+## Before the beta release date ##
+
+- [ ] Ensure the Credits chapter has been updated.
+- [ ] Ensure an empty `CompatXX.v` file has been created.
+- [ ] Ensure that an appropriate version of the plugins we will distribute with
+ Coq has been tagged.
+- [ ] Have some people test the recently auto-generated Windows and MacOS
+ packages.
+- [ ] Change the version name from alpha to beta1 (see
+ [#7009](https://github.com/coq/coq/pull/7009/files)).
+ We generally do not update the magic numbers at this point.
+- [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+
+### These steps are the same for all releases (beta, final, patch-level) ###
+
+- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that
+ package managers can start preparing package updates.
+- [ ] Draft a release on GitHub.
+- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and
+ upload them on GitHub.
+- [ ] Prepare a page of news on the website with the link to the GitHub release
+ (see [coq/www#63](https://github.com/coq/www/pull/63)).
+- [ ] Upload the new version of the reference manual to the website.
+ *TODO: setup some continuous deployment for this.*
+- [ ] Merge the website update, publish the release
+ and send annoucement e-mails.
+- [ ] Ping **@Zimmi48** to publish a new version on Zenodo.
+ *TODO: automate this.*
+- [ ] Close the milestone
+
+## At the final release time ##
+
+- [ ] Change the version name to X.X.0 and the magic numbers (see
+ [#7271](https://github.com/coq/coq/pull/7271/files)).
+- [ ] Put the `VX.X.0` tag.
+
+Repeat the generic process documented above for all releases.
+
+- [ ] Switch the default version of the reference manual on the website.
+
+## At the patch-level release time ##
+
+We generally do not update the magic numbers at this point (see
+[`2881a18`](https://github.com/coq/coq/commit/2881a18)).
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index f3e60edea..2bec09de2 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -14,11 +14,19 @@
export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
-exec $OCAMLDEBUG \
+GUESS_CHECKER=
+for arg in "$@"; do
+ if [ "${arg##*/}" = coqchk.byte ]; then
+ GUESS_CHECKER=1
+ fi
+done
+
+if [ -z "$GUESS_CHECKER" ]; then
+ exec $OCAMLDEBUG \
-I $CAMLP5LIB -I +threads \
-I $COQTOP \
-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
- -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
+ -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-I $COQTOP/library -I $COQTOP/engine \
-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
-I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
@@ -35,3 +43,11 @@ exec $OCAMLDEBUG \
-I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \
-I $COQTOP/ide \
"$@"
+else
+ exec $OCAMLDEBUG \
+ -I $CAMLP5LIB -I +threads \
+ -I $COQTOP \
+ -I $COQTOP/config -I $COQTOP/clib \
+ -I $COQTOP/lib -I $COQTOP/checker \
+ "$@"
+fi
diff --git a/dev/tools/check-owners-pr.sh b/dev/tools/check-owners-pr.sh
new file mode 100755
index 000000000..d2910279b
--- /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 000000000..1a97508ab
--- /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 62fdaec80..70a9756e5 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/merge-pr.sh b/dev/tools/merge-pr.sh
index 1c94f630f..00d04e6b3 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -5,7 +5,7 @@ set -o pipefail
API=https://api.github.com/repos/coq/coq
OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq"
-OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq"
+OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq"
# This script depends (at least) on git (>= 2.7) and jq.
# It should be used like this: dev/tools/merge-pr.sh /PR number/
@@ -91,8 +91,10 @@ fi
REMOTE_URL=$(git remote get-url "$REMOTE" --all)
if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \
[ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \
- [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}" ] && \
- [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}.git" ]; then
+ [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}" ] && \
+ [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \
+ [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \
+ [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then
error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL"
error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index b56925c37..ad2f2f93e 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.ml b/dev/top_printers.ml
index f9b402586..cb1abc4a9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -162,8 +162,8 @@ let pp_state_t n = pp (Reductionops.pr_state n)
(* proof printers *)
let pr_evar ev = Pp.int (Evar.repr ev)
let ppmetas metas = pp(Termops.pr_metaset metas)
-let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
-let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd)
let pr_existentialset evars =
prlist_with_sep spc pr_evar (Evar.Set.elements evars)
let ppexistentialset evars =
@@ -203,17 +203,17 @@ let pproof p = pp(Proof.pr_proof p)
let ppuni u = pp(Universe.pr u)
let ppuni_level u = pp (Level.pr u)
-let prlev = Universes.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes
let ppuniverse_set l = pp (LSet.pr prlev l)
let ppuniverse_instance l = pp (Instance.pr prlev l)
let ppuniverse_context l = pp (pr_universe_context prlev l)
let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
-let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
+let ppuniverse_opt_subst l = pp (UnivSubst.pr_universe_opt_subst l)
let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l)
let ppconstraints c = pp (pr_constraints Level.pr c)
-let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
+let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)
let ppuniverse_context_future c =
let ctx = Future.force c in
ppuniverse_context ctx
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index dad6dcc1c..63d7d5805 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
@@ -139,11 +139,11 @@ val ppuniverse_instance : Univ.Instance.t -> unit
val ppuniverse_context : Univ.UContext.t -> unit
val ppuniverse_context_set : Univ.ContextSet.t -> unit
val ppuniverse_subst : Univ.universe_subst -> unit
-val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit
+val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit
val ppuniverse_level_subst : Univ.universe_level_subst -> unit
val ppevar_universe_context : UState.t -> unit
val ppconstraints : Univ.Constraint.t -> unit
-val ppuniverseconstraints : Universes.Constraints.t -> unit
+val ppuniverseconstraints : UnivProblem.Set.t -> unit
val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit