diff options
Diffstat (limited to 'dev')
32 files changed, 343 insertions, 349 deletions
diff --git a/dev/base_db b/dev/base_db index e18ac534ac..155e9591e0 100644 --- a/dev/base_db +++ b/dev/base_db @@ -1,4 +1,5 @@ source core.dbg +load_printer ltac_plugin.cmo load_printer top_printers.cmo install_printer Top_printers.ppid install_printer Top_printers.ppsp diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index c3d895784e..71207bb040 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -434,7 +434,7 @@ function build_prep_overlay { # ------------------------------------------------------------------------------ function load_overlay_data { - if [ -n "${GITLAB_CI+}" ]; then + if [ -n "${GITLAB_CI-}" ]; then export CI_BRANCH="$CI_COMMIT_REF_NAME" if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then export CI_PULL_REQUEST="${CI_BRANCH#pr-}" diff --git a/dev/checker.dbg b/dev/checker.dbg deleted file mode 100644 index b2323b6175..0000000000 --- a/dev/checker.dbg +++ /dev/null @@ -1,6 +0,0 @@ -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 deleted file mode 100644 index 327e636c57..0000000000 --- a/dev/checker_db +++ /dev/null @@ -1,39 +0,0 @@ -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 deleted file mode 100644 index 40ae1a7b05..0000000000 --- a/dev/checker_printers.ml +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* * 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 deleted file mode 100644 index 2f9500c5c3..0000000000 --- a/dev/checker_printers.mli +++ /dev/null @@ -1,54 +0,0 @@ -(************************************************************************) -(* * 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 7853866f62..4709247549 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -26,7 +26,8 @@ our CI. This means that: On the condition that: -- At the time of the submission, your development works with Coq master branch. +- At the time of the submission, your development works with Coq's + `master` branch. - Your development is publicly available in a git repository and we can easily send patches to you (e.g. through pull / merge requests). @@ -60,6 +61,19 @@ performance benchmark. Currently this is done by providing an OPAM package in https://github.com/coq/opam-coq-archive and opening an issue at https://github.com/coq/coq-bench/issues. +### Recommended branching policy. + +It is sometimes the case that you will need to maintain a branch of +your development for particular Coq versions. This is in fact very +likely if your development includes a Coq ML plugin. + +We thus recommend a branching convention that mirrors Coq's branching +policy. Then, you would have a `master` branch that follows Coq's +`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so +on. + +This convention will be supported by tools in the future to make some +developer commands work more seamlessly. Information for developers -------------------------- diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index f422030b53..50d4d21637 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -238,7 +238,7 @@ ######################################################################## # plugin_tutorial ######################################################################## -: "${plugin_tutorial_CI_REF:=14b2976cdf67db788b79d9421ce1e89bd15c7313}" +: "${plugin_tutorial_CI_REF:=master}" : "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" : "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 41e1d1a937..4ddb582414 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-22-V1" +# CACHEKEY: "bionic_coq-V2018-10-30-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.3.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. @@ -53,10 +53,10 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch -ENV COMPILER_EDGE="4.07.0" \ - CAMLP5_VER_EDGE="7.06" \ +ENV COMPILER_EDGE="4.07.1" \ + CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="dune-release.0.3.0" + BASE_OPAM_EDGE="dune-release.1.1.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh new file mode 100755 index 0000000000..4605255d5e --- /dev/null +++ b/dev/ci/user-overlays/08515-command-atts.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then + ltac2_CI_REF=command-atts + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + Equations_CI_REF=command-atts + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + plugin_tutorial_CI_REF=command-atts + plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials +fi diff --git a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh new file mode 100644 index 0000000000..9d723dc7f2 --- /dev/null +++ b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh @@ -0,0 +1,11 @@ +_OVERLAY_BRANCH=name-abstract-univ-context + +if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + Elpi_CI_REF="$_OVERLAY_BRANCH" + Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + Equations_CI_REF="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh new file mode 100644 index 0000000000..bd3e1bf7ff --- /dev/null +++ b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then + plugin_tutorial_CI_REF=pr8671-fix + plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials + +fi diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh new file mode 100644 index 0000000000..98530c825a --- /dev/null +++ b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then + + Elpi_CI_REF=kernel-entries-cleanup + Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi + + Equations_CI_REF=kernel-entries-cleanup + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh new file mode 100644 index 0000000000..81ed91f52b --- /dev/null +++ b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then + + Elpi_CI_REF=master+generalized-evar-printers-pr8688 + Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh new file mode 100644 index 0000000000..8ad8cba243 --- /dev/null +++ b/dev/ci/user-overlays/08844-split-tactics.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then + Equations_CI_REF=split-tactics + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + ltac2_CI_REF=split-tactics + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + fiat_parsers_CI_REF=split-tactics + fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat +fi diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh new file mode 100644 index 0000000000..17eb5fffae --- /dev/null +++ b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then + + Equations_CI_REF=program-hook-obligation-subst + Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 68afe7ee4a..7fb73e447d 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -33,3 +33,11 @@ fi ``` (`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh)) + +### Branching conventions + +We suggest you use the convention of identical branch names for the +Coq branch and the CI project branch used in the overlay. For example, +if your Coq PR is coming from the branch `more_efficient_tc`, and that +breaks `ltac2`, we suggest you create a `ltac2` overlay with a branch +named `more_efficient_tc`. diff --git a/dev/core.dbg b/dev/core.dbg index 972ba701e4..f676b643e4 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,6 +1,7 @@ -source camlp5.dbg load_printer threads.cma load_printer str.cma +load_printer gramlib.cma +load_printer config.cma load_printer clib.cma load_printer dynlink.cma load_printer lib.cma @@ -16,4 +17,3 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer ltac_plugin.cmo diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg new file mode 100644 index 0000000000..cf9c5bd39a --- /dev/null +++ b/dev/core_dune.dbg @@ -0,0 +1,20 @@ +load_printer threads.cma +load_printer str.cma +load_printer gramlib.cma +load_printer config.cma +load_printer clib.cma +load_printer dynlink.cma +load_printer lib.cma +load_printer byterun.cma +load_printer kernel.cma +load_printer library.cma +load_printer engine.cma +load_printer pretyping.cma +load_printer interp.cma +load_printer proofs.cma +load_printer parsing.cma +load_printer printing.cma +load_printer tactics.cma +load_printer vernac.cma +load_printer stm.cma +load_printer toplevel.cma @@ -1,88 +1,6 @@ source core.dbg + +load_printer ltac_plugin.cmo load_printer top_printers.cmo -install_printer Top_printers.pP -install_printer Top_printers.ppfuture -install_printer Top_printers.ppid -install_printer Top_printers.pplab -install_printer Top_printers.ppmbid -install_printer Top_printers.ppdir -install_printer Top_printers.ppmp -install_printer Top_printers.ppcon -install_printer Top_printers.ppproj -install_printer Top_printers.ppkn -install_printer Top_printers.ppmind -install_printer Top_printers.ppind -install_printer Top_printers.ppsp -install_printer Top_printers.ppqualid -install_printer Top_printers.ppclindex -install_printer Top_printers.ppscheme -install_printer Top_printers.ppwf_paths -install_printer Top_printers.ppevar -install_printer Top_printers.ppconstr -install_printer Top_printers.ppsconstr -install_printer Top_printers.ppeconstr -install_printer Top_printers.ppconstr_expr -install_printer Top_printers.ppglob_constr -install_printer Top_printers.pppattern -install_printer Top_printers.ppfconstr -install_printer Top_printers.ppbigint -install_printer Top_printers.ppintset -install_printer Top_printers.ppidset -install_printer Top_printers.ppidmapgen -install_printer Top_printers.ppididmap -install_printer Top_printers.ppconstrunderbindersidmap -install_printer Top_printers.ppevarsubst -install_printer Top_printers.ppunbound_ltac_var_map -install_printer Top_printers.ppclosure -install_printer Top_printers.ppclosedglobconstr -install_printer Top_printers.ppclosedglobconstridmap -install_printer Top_printers.ppglobal -install_printer Top_printers.ppconst -install_printer Top_printers.ppvar -install_printer Top_printers.ppj -install_printer Top_printers.ppsubst -install_printer Top_printers.ppdelta -install_printer Top_printers.pp_idpred -install_printer Top_printers.pp_cpred -install_printer Top_printers.pp_transparent_state -install_printer Top_printers.pp_stack_t -install_printer Top_printers.pp_cst_stack_t -install_printer Top_printers.pp_state_t -install_printer Top_printers.ppmetas -install_printer Top_printers.ppevm -install_printer Top_printers.ppexistentialset -install_printer Top_printers.ppexistentialfilter -install_printer Top_printers.ppclenv -install_printer Top_printers.ppgoalgoal -install_printer Top_printers.ppgoal -install_printer Top_printers.pphintdb -install_printer Top_printers.ppproofview -install_printer Top_printers.ppopenconstr -install_printer Top_printers.pproof -install_printer Top_printers.ppuni -install_printer Top_printers.ppuni_level -install_printer Top_printers.ppuniverse_set -install_printer Top_printers.ppuniverse_instance -install_printer Top_printers.ppuniverse_context -install_printer Top_printers.ppuniverse_context_set -install_printer Top_printers.ppuniverse_subst -install_printer Top_printers.ppuniverse_opt_subst -install_printer Top_printers.ppuniverse_level_subst -install_printer Top_printers.ppevar_universe_context -install_printer Top_printers.ppconstraints -install_printer Top_printers.ppuniverseconstraints -install_printer Top_printers.ppuniverse_context_future -install_printer Top_printers.ppcumulativity_info -install_printer Top_printers.ppabstract_cumulativity_info -install_printer Top_printers.ppuniverses -install_printer Top_printers.ppnamedcontextval -install_printer Top_printers.ppenv -install_printer Top_printers.pptac -install_printer Top_printers.ppobj -install_printer Top_printers.pploc -install_printer Top_printers.pp_argument_type -install_printer Top_printers.pp_generic_argument -install_printer Top_printers.ppgenarginfo -install_printer Top_printers.ppgenargargt -install_printer Top_printers.ppist +source top_printers.dbg diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 000f21c254..318562338d 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -6,19 +6,21 @@ This document describes how patches, submitted as pull requests (PRs) on the ## Code owners -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. +The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of +the code. Sometime there is one principal maintainer and one or several +secondary maintainer(s). Sometimes, it is a team of code owners and all of its +members act as principal maintainers for the component. 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. +maintainer (or the code owner team) for a review. If the PR touches several +parts, all the corresponding owners will be asked for a review. Maintainers are never assigned as reviewer on their own PRs. -If a principal maintainer submits a PR that changes the component they own, they -must assign the secondary maintainer as reviewer. They should also do it if they -know they are not available to do the review. +If a principal maintainer submits a PR or is a co-author of a PR that is +submitted and this PR changes the component they own, they must request a +review from a secondary maintainer. They can also delegate the review if they +know they are not available to do it. ## Reviewing @@ -35,17 +37,29 @@ When maintainers receive a review request, they are expected to: REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. -In all cases, maintainers can delegate reviews to the other maintainer of the -same component, except if it would lead to a maintainer reviewing their own -patch. +When a PR received lots of comments or if the PR has not been opened for long +and the assignee thinks that some other developers might want to comment, +it is recommended that they announce their intention to merge and wait a full +working day (or more if deemed useful) before the actual merge, as a sort of +last call for comments. + +In all cases, maintainers can delegate reviews to the other maintainers, +except if it would lead to a maintainer reviewing their own patch. A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. +When none of the maintainers have commented nor self-assigned a PR in a delay +of five working days, any maintainer of another component who feels comfortable +reviewing the PR can assign it to themselves. To prevent misunderstandings, +maintainers should not hesitate to announce in advance when they shall be +unavailable for more than five working days. + (*) In case a component is touched in a trivial way (adding/removing one file in 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. +say in a comment they think a review is not required from every code owner and +proceed with the merge. ### Breaking changes @@ -54,7 +68,8 @@ those external projects should have been prepared (cf. the relevant sub-section in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). -Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. +Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or +the [`dev/doc/changes.md`](changes.md) 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. @@ -78,9 +93,9 @@ put the approriate label. Otherwise, they are expected to merge the PR using the When CI has a few failures which look spurious, restarting the corresponding jobs is a good way of ensuring this was indeed the case. -To restart a job on Travis, you should connect using your GitHub account; -being part of the Coq organization on GitHub should give you the permission -to do so. +To restart a job on Travis or on AppVeyor, you should connect using your GitHub +account; being part of the Coq organization on GitHub should give you the +permission to do so. To restart a job on GitLab CI, you should sign into GitLab (this can be done using a GitHub account); if you are part of the [Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry" @@ -93,9 +108,10 @@ When the PR has conflicts, the assignee can either: In both cases, CI should be run again. -In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix +In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR +is not a candidate for backporting), it is ok to fix the conflicts in the merge commit (following the same steps as below), and push -to `master` directly. Don't use the GitHub interface to fix these conflicts. +to `master` directly. DON'T USE the GitHub interface to fix these conflicts. To merge the PR proceed in the following way ``` diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 91ab57f1e9..c5ea88aaf6 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -68,6 +68,27 @@ Note that you must invoke the `#rectypes;;` toplevel flag in order to use Coq libraries. The provided `.ocamlinit` file does this automatically. +## ocamldebug + +You can use `ocamldebug` with Dune; after a build, do: + +``` +dune exec dev/dune-dbg +(ocd) source dune_db +``` + +or + +``` +dune exec dev/dune-dbg checker +(ocd) source dune_db +``` + +for the checker. Unfortunately, dependency handling here is not fully +refined, so you need to build enough of Coq once to use this target +[it will then correctly compute the deps and rebuild if you call the +script again] This will be fixed in the future. + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages diff --git a/dev/doc/changes.md b/dev/doc/changes.md index eb5b9ee1d3..b1fdfafd3a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -32,6 +32,12 @@ Macros: - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are deprecated. Use TYPED AS instead. +- coqpp (.mlg) based VERNAC EXTEND accesses attributes through a `#[ x + = att ]` syntax, where `att : 'a Attributes.attribute` and `x` will + be bound with type `'a` in the expression, unlike the old system + where `atts : Vernacexpr.vernac_flags` was bound in the expression + and had to be manually parsed. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index 8f96ac223f..774552237a 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the `Refine.refine` primitive. ```ocaml -val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine typecheck t], [t] is a term with holes under some +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions @@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) ``` -In a first approximation, we can think of `'a Sigma.run` as -`evar_map -> 'a * evar_map`. What the function does is first evaluate the -`Constr.t Sigma.run` argument in the current proof state, and then use the -resulting term as a filler for the proof under focus. All evars that have been -created by the invocation of this thunk are then turned into new goals added in -the order of their creation. +What the function does is first evaluate the `t` argument in the +current proof state, and then use the resulting term as a filler for +the proof under focus. All evars that have been created by the +invocation of this thunk are then turned into new goals added in the +order of their creation. To see how we can use it, let us have a look at an idealized example, the `cut` tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` @@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order. ```ocaml let cut c = - let open Sigma in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (** In this block, we focus on one goal at a time indicated by gl *) let env = Proofview.Goal.env gl in (** Get the context of the goal, essentially [Γ] *) @@ -80,25 +78,22 @@ let cut c = let t = mkArrow c (Vars.lift 1 concl) in (** Build [X -> A]. Note the lifting of [A] due to being on the right hand side of the arrow. *) - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> (** All evars generated by this block will be added as goals *) - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + let sigma, f = Evarutil.new_evar env sigma t in (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity substitution for [Γ] is extracted from the [env] argument, so that one must be careful to pass the correct context here in order for the resulting term to be well-typed. The [p] return value is a proof term used to enforce sigma monotonicity. *) - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + let sigma, x = Evarutil.new_evar env sigma c in (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return [x := Γ ⊢ ?e2{Γ} : X]. *) let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) - Sigma (r, sigma, p +> q) - (** Fills the current hole with [r]. The [p +> q] thingy ensures - monotonicity of sigma. *) - end } - end } + end + end ``` The `Evarutil.new_evar` function is the preferred way to generate evars in diff --git a/dev/dune b/dev/dune new file mode 100644 index 0000000000..bfa2d525c9 --- /dev/null +++ b/dev/dune @@ -0,0 +1,16 @@ +(library + (name top_printers) + (public_name coq.top_printers) + (synopsis "Coq's Debug Printers") + (wrapped false) + (modules :standard) + (libraries coq.toplevel coq.plugins.ltac)) + +(rule + (targets dune-dbg) + (deps dune-dbg.in + ../checker/main.bc + ../topbin/coqtop_byte_bin.bc + ; This is not enough as the call to `ocamlfind` will fail :/ + top_printers.cma) + (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in new file mode 100755 index 0000000000..3f3df23fe1 --- /dev/null +++ b/dev/dune-dbg.in @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +# Run in a proper install dune env. +case $1 in + checker) + exe=_build/default/checker/main.bc + ;; + *) + exe=_build/default/topbin/coqtop_byte_bin.bc + ;; +esac + +ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 93b807d5e3..cf95941de5 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -1,7 +1,7 @@ -(lang dune 1.2) +(lang dune 1.4) ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.07.0))) -(context (opam (switch 4.07.0+flambda))) +(context (opam (switch 4.07.1))) +(context (opam (switch 4.07.1+flambda))) diff --git a/dev/dune_db b/dev/dune_db new file mode 100644 index 0000000000..f920f7c75c --- /dev/null +++ b/dev/dune_db @@ -0,0 +1,6 @@ +source core_dune.dbg + +load_printer ltac_plugin.cma +load_printer top_printers.cma + +source top_printers.dbg diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 85bb04efe0..d330f517be 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -14,40 +14,24 @@ export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH -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/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 \ - -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ - -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ - -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ - -I $COQTOP/plugins/firstorder \ - -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ - -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ - -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ - -I $COQTOP/plugins/ring \ - -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ - -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ - -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 +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/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 \ + -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ + -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ + -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ + -I $COQTOP/plugins/firstorder \ + -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ + -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ + -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ + -I $COQTOP/plugins/ring \ + -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ + -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ + -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ + -I $COQTOP/ide \ + "$@" diff --git a/dev/tools/change-header b/dev/tools/change-header index 61cc866602..687c02f4f1 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' modified=0 kept=0 -for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do +for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do headline=`head -n 1 $i` if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then # Has emacs header diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg new file mode 100644 index 0000000000..eab88c7290 --- /dev/null +++ b/dev/top_printers.dbg @@ -0,0 +1,85 @@ +install_printer Top_printers.pP +install_printer Top_printers.ppfuture +install_printer Top_printers.ppid +install_printer Top_printers.pplab +install_printer Top_printers.ppmbid +install_printer Top_printers.ppdir +install_printer Top_printers.ppmp +install_printer Top_printers.ppcon +install_printer Top_printers.ppproj +install_printer Top_printers.ppkn +install_printer Top_printers.ppmind +install_printer Top_printers.ppind +install_printer Top_printers.ppsp +install_printer Top_printers.ppqualid +install_printer Top_printers.ppclindex +install_printer Top_printers.ppscheme +install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppevar +install_printer Top_printers.ppconstr +install_printer Top_printers.ppsconstr +install_printer Top_printers.ppeconstr +install_printer Top_printers.ppconstr_expr +install_printer Top_printers.ppglob_constr +install_printer Top_printers.pppattern +install_printer Top_printers.ppfconstr +install_printer Top_printers.ppbigint +install_printer Top_printers.ppintset +install_printer Top_printers.ppidset +install_printer Top_printers.ppidmapgen +install_printer Top_printers.ppididmap +install_printer Top_printers.ppconstrunderbindersidmap +install_printer Top_printers.ppevarsubst +install_printer Top_printers.ppunbound_ltac_var_map +install_printer Top_printers.ppclosure +install_printer Top_printers.ppclosedglobconstr +install_printer Top_printers.ppclosedglobconstridmap +install_printer Top_printers.ppglobal +install_printer Top_printers.ppconst +install_printer Top_printers.ppvar +install_printer Top_printers.ppj +install_printer Top_printers.ppsubst +install_printer Top_printers.ppdelta +install_printer Top_printers.pp_idpred +install_printer Top_printers.pp_cpred +install_printer Top_printers.pp_transparent_state +install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_cst_stack_t +install_printer Top_printers.pp_state_t +install_printer Top_printers.ppmetas +install_printer Top_printers.ppevm +install_printer Top_printers.ppexistentialset +install_printer Top_printers.ppexistentialfilter +install_printer Top_printers.ppclenv +install_printer Top_printers.ppgoalgoal +install_printer Top_printers.ppgoal +install_printer Top_printers.pphintdb +install_printer Top_printers.ppproofview +install_printer Top_printers.ppopenconstr +install_printer Top_printers.pproof +install_printer Top_printers.ppuni +install_printer Top_printers.ppuni_level +install_printer Top_printers.ppuniverse_set +install_printer Top_printers.ppuniverse_instance +install_printer Top_printers.ppuniverse_context +install_printer Top_printers.ppuniverse_context_set +install_printer Top_printers.ppuniverse_subst +install_printer Top_printers.ppuniverse_opt_subst +install_printer Top_printers.ppuniverse_level_subst +install_printer Top_printers.ppevar_universe_context +install_printer Top_printers.ppconstraints +install_printer Top_printers.ppuniverseconstraints +install_printer Top_printers.ppuniverse_context_future +install_printer Top_printers.ppcumulativity_info +install_printer Top_printers.ppabstract_cumulativity_info +install_printer Top_printers.ppuniverses +install_printer Top_printers.ppnamedcontextval +install_printer Top_printers.ppenv +install_printer Top_printers.pptac +install_printer Top_printers.ppobj +install_printer Top_printers.pploc +install_printer Top_printers.pp_argument_type +install_printer Top_printers.pp_generic_argument +install_printer Top_printers.ppgenarginfo +install_printer Top_printers.ppgenargargt +install_printer Top_printers.ppist diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 44d44ccc4b..fd08f9ffe8 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -168,8 +168,8 @@ let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty 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:!Detyping.print_universes (Some 2) evd) -let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd) +let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) (Global.env ()) evd) +let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None (Global.env ()) evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = @@ -180,14 +180,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) -let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g)) +let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g)) let pphintdb db = pp(envpp Hints.pr_hint_db_env db) let ppproofview p = let gls,sigma = Proofview.proofview p in - pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma) + pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) (Global.env ()) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) (Global.env ()) evd ++ envpp pr_econstr_env c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) |