diff options
Diffstat (limited to 'dev')
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 |