diff options
33 files changed, 195 insertions, 135 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f0403a7318..0ebf69f50f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -70,8 +70,6 @@ before_script: - config/coq_config.py - test-suite/misc/universes/all_stdlib.v expire_in: 1 week - variables: - timeout: "" script: - set -e @@ -84,8 +82,8 @@ before_script: - echo 'end:coq.config' - echo 'start:coq.build' - - $timeout make -j "$NJOBS" byte - - $timeout make -j "$NJOBS" world $EXTRA_TARGET + - make -j "$NJOBS" byte + - make -j "$NJOBS" world $EXTRA_TARGET - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' @@ -164,7 +162,7 @@ before_script: - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - - $timeout make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all + - make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" COQFLAGS="${COQFLAGS}" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -172,8 +170,6 @@ before_script: - test-suite/logs # Gitlab doesn't support yet "expire_in: never" so we use the instance default # expire_in: never - variables: - timeout: "" # set dependencies when using .validate-template: @@ -279,7 +275,7 @@ build:base+async: variables: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" COQUSERFLAGS: "-async-proofs on" - timeout: "timeout 100m" + timeout: 100m allow_failure: true # See https://github.com/coq/coq/issues/9658 only: variables: @@ -290,7 +286,7 @@ build:quick: variables: COQ_EXTRA_CONF: "-native-compiler no" QUICK: "1" - timeout: "timeout 100m" + timeout: 100m allow_failure: true # See https://github.com/coq/coq/issues/9637 only: variables: @@ -327,7 +323,7 @@ pkg:opam: - opam pin add --kind=path coqide.$COQ_VERSION . - set +e variables: - COQ_VERSION: "8.10" + COQ_VERSION: "8.11" OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" only: *full-ci @@ -515,7 +511,7 @@ test-suite:base+async: - build:base variables: COQFLAGS: "-async-proofs on -async-proofs-cache force" - timeout: "timeout 100m" + timeout: 100m allow_failure: true only: variables: @@ -685,6 +681,9 @@ plugin:ci-mtac2: plugin:ci-paramcoq: extends: .ci-template +plugin:ci-perennial: + extends: .ci-template-flambda + plugin:plugin-tutorial: stage: stage-1 dependencies: [] diff --git a/META.coq.in b/META.coq.in index f7922e0ac2..0baacbc82e 100644 --- a/META.coq.in +++ b/META.coq.in @@ -1,7 +1,7 @@ # TODO: Generate automatically with Dune description = "The Coq Proof Assistant Plugin API" -version = "8.10" +version = "8.11" directory = "" requires = "" @@ -9,7 +9,7 @@ requires = "" package "config" ( description = "Coq Configuration Variables" - version = "8.10" + version = "8.11" directory = "config" @@ -19,7 +19,7 @@ package "config" ( package "clib" ( description = "Base General Coq Library" - version = "8.10" + version = "8.11" directory = "clib" requires = "str, unix, threads" @@ -31,7 +31,7 @@ package "clib" ( package "lib" ( description = "Base Coq-Specific Library" - version = "8.10" + version = "8.11" directory = "lib" @@ -45,7 +45,7 @@ package "lib" ( package "vm" ( description = "Coq VM" - version = "8.10" + version = "8.11" directory = "kernel/byterun" @@ -64,7 +64,7 @@ package "vm" ( package "kernel" ( description = "Coq's Kernel" - version = "8.10" + version = "8.11" directory = "kernel" @@ -78,7 +78,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.10" + version = "8.11" requires = "coq.kernel" @@ -92,7 +92,7 @@ package "library" ( package "engine" ( description = "Coq Tactic Engine" - version = "8.10" + version = "8.11" requires = "coq.library" directory = "engine" @@ -105,7 +105,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.10" + version = "8.11" requires = "coq.engine" directory = "pretyping" @@ -118,7 +118,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.10" + version = "8.11" requires = "coq.pretyping" directory = "interp" @@ -131,7 +131,7 @@ package "interp" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.10" + version = "8.11" requires = "coq.interp" directory = "proofs" @@ -144,7 +144,7 @@ package "proofs" ( package "gramlib" ( description = "Coq Grammar Engine" - version = "8.10" + version = "8.11" requires = "coq.lib" directory = "gramlib/.pack" @@ -156,7 +156,7 @@ package "gramlib" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.10" + version = "8.11" requires = "coq.gramlib, coq.proofs" directory = "parsing" @@ -169,7 +169,7 @@ package "parsing" ( package "printing" ( description = "Coq Printing Engine" - version = "8.10" + version = "8.11" requires = "coq.parsing" directory = "printing" @@ -182,7 +182,7 @@ package "printing" ( package "tactics" ( description = "Coq Basic Tactics" - version = "8.10" + version = "8.11" requires = "coq.printing" directory = "tactics" @@ -195,7 +195,7 @@ package "tactics" ( package "vernac" ( description = "Coq Vernacular Interpreter" - version = "8.10" + version = "8.11" requires = "coq.tactics" directory = "vernac" @@ -208,7 +208,7 @@ package "vernac" ( package "stm" ( description = "Coq State Transactional Machine" - version = "8.10" + version = "8.11" requires = "coq.vernac" directory = "stm" @@ -221,7 +221,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.10" + version = "8.11" requires = "num, coq.stm" directory = "toplevel" @@ -234,7 +234,7 @@ package "toplevel" ( package "idetop" ( description = "Coq IDE Libraries" - version = "8.10" + version = "8.11" requires = "coq.toplevel" directory = "ide" @@ -247,7 +247,7 @@ package "idetop" ( package "ide" ( description = "Coq IDE Libraries" - version = "8.10" + version = "8.11" requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3" directory = "ide" @@ -260,7 +260,7 @@ package "ide" ( package "ideprotocol" ( description = "Coq IDE protocol" - version = "8.10" + version = "8.11" requires = "coq.toplevel" directory = "ide/protocol" @@ -273,14 +273,14 @@ package "ideprotocol" ( package "plugins" ( description = "Coq built-in plugins" - version = "8.10" + version = "8.11" directory = "plugins" package "ltac" ( description = "Coq LTAC Plugin" - version = "8.10" + version = "8.11" requires = "coq.stm" directory = "ltac" @@ -293,7 +293,7 @@ package "plugins" ( package "tauto" ( description = "Coq tauto plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "ltac" @@ -305,7 +305,7 @@ package "plugins" ( package "omega" ( description = "Coq omega plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "omega" @@ -317,7 +317,7 @@ package "plugins" ( package "micromega" ( description = "Coq micromega plugin" - version = "8.10" + version = "8.11" requires = "num,coq.plugins.ltac" directory = "micromega" @@ -329,7 +329,7 @@ package "plugins" ( package "setoid_ring" ( description = "Coq newring plugin" - version = "8.10" + version = "8.11" requires = "" directory = "setoid_ring" @@ -341,7 +341,7 @@ package "plugins" ( package "extraction" ( description = "Coq extraction plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "extraction" @@ -353,7 +353,7 @@ package "plugins" ( package "cc" ( description = "Coq cc plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "cc" @@ -365,7 +365,7 @@ package "plugins" ( package "firstorder" ( description = "Coq ground plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "firstorder" @@ -377,7 +377,7 @@ package "plugins" ( package "rtauto" ( description = "Coq rtauto plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "rtauto" @@ -389,7 +389,7 @@ package "plugins" ( package "btauto" ( description = "Coq btauto plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "btauto" @@ -401,7 +401,7 @@ package "plugins" ( package "funind" ( description = "Coq recdef plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.extraction" directory = "funind" @@ -413,7 +413,7 @@ package "plugins" ( package "nsatz" ( description = "Coq nsatz plugin" - version = "8.10" + version = "8.11" requires = "num,coq.plugins.ltac" directory = "nsatz" @@ -425,7 +425,7 @@ package "plugins" ( package "rsyntax" ( description = "Coq rsyntax plugin" - version = "8.10" + version = "8.11" requires = "" directory = "syntax" @@ -437,7 +437,7 @@ package "plugins" ( package "int63syntax" ( description = "Coq int63syntax plugin" - version = "8.10" + version = "8.11" requires = "" directory = "syntax" @@ -449,7 +449,7 @@ package "plugins" ( package "string_notation" ( description = "Coq string_notation plugin" - version = "8.10" + version = "8.11" requires = "" directory = "syntax" @@ -461,7 +461,7 @@ package "plugins" ( package "derive" ( description = "Coq derive plugin" - version = "8.10" + version = "8.11" requires = "" directory = "derive" @@ -473,7 +473,7 @@ package "plugins" ( package "ssrmatching" ( description = "Coq ssrmatching plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ltac" directory = "ssrmatching" @@ -485,7 +485,7 @@ package "plugins" ( package "ssreflect" ( description = "Coq ssreflect plugin" - version = "8.10" + version = "8.11" requires = "coq.plugins.ssrmatching" directory = "ssr" diff --git a/Makefile.ci b/Makefile.ci index de03ee8e84..60d4b68f53 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -35,6 +35,7 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ + ci-perennial \ ci-quickchick \ ci-relation_algebra \ ci-sf \ diff --git a/Makefile.ide b/Makefile.ide index 081d15a1a2..39c6c8ad1e 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -264,7 +264,7 @@ $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents $(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents $(MKDIR) $@ - $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.so $@ + $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.dylib $@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib @@ -273,8 +273,8 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib { "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ > $@/gtk-3.0/gdk-pixbuf.loaders - { "$(GTKBIN)/gtk-query-immodules-3.0" $@/../immodules/*.so |\ - sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ + { "$(GTKBIN)/gtk-query-immodules-3.0" $@/../immodules/*.dylib |\ + sed -e "s!/.*\(/immodules/.*.dylib\)!@executable_path/../Resources/\1!" |\ sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ > $@/gtk-3.0/gtk-immodules.loaders $(MKDIR) $@/pango @@ -283,7 +283,7 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib $(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) $(MKDIR) $@ macpack -d ../Resources/lib $(COQIDEINAPP) - for i in $@/../loaders/*.so $@/../immodules/*.so; \ + for i in $@/../loaders/*.so $@/../immodules/*.dylib; \ do \ macpack -d ../lib $$i; \ done diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 38ea915f3c..31dcae0f82 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -58,8 +58,8 @@ jobs: displayName: 'Install system dependencies' env: HOMEBREW_NO_AUTO_UPDATE: "1" - HBCORE_DATE: "2019-06-16" - HBCORE_REF: "944a5b7d83e4b81c749d93831b514607bdd2b6a1" + HBCORE_DATE: "2019-09-03" + HBCORE_REF: "44ee64cf4b9f2d2bf000758d356db0c77425e42e" - script: | set -e diff --git a/configure.ml b/configure.ml index d7370b28c1..e59a41a8d4 100644 --- a/configure.ml +++ b/configure.ml @@ -12,11 +12,11 @@ #load "str.cma" open Printf -let coq_version = "8.10+alpha" -let coq_macos_version = "8.9.90" (** "[...] should be a string comprised of +let coq_version = "8.11+alpha" +let coq_macos_version = "8.10.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 8991 -let state_magic = 58991 +let vo_magic = 81091 +let state_magic = 581091 let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; diff --git a/default.nix b/default.nix index 2d101eed57..19afc2bd1b 100644 --- a/default.nix +++ b/default.nix @@ -29,7 +29,7 @@ , shell ? false # We don't use lib.inNixShell because that would also apply # when in a nix-shell of some package depending on this one. -, coq-version ? "8.10-git" +, coq-version ? "8.11-git" }: with pkgs; diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 3923fea30e..8db0087e3c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -311,3 +311,10 @@ : "${argosy_CI_REF:=master}" : "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}" : "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}" + +######################################################################## +# perennial +######################################################################## +: "${perennial_CI_REF:=master}" +: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" +: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh new file mode 100755 index 0000000000..f3be66e814 --- /dev/null +++ b/dev/ci/ci-perennial.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download perennial + +# required by Perennial's coqc.py build wrapper +export LC_ALL=C.UTF-8 + +( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false ) diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 452160ea5a..1c486b024d 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -2,6 +2,11 @@ ## As soon as the previous version branched off master ## +In principle, these steps should be undertaken by the RM of the next +release. Unfortunately, we have not yet been able to nominate RMs +early enough in the process for this person to be known at that point +in time. + - [ ] 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 @@ -54,25 +59,39 @@ - [ ] 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). + + The command that was used in the previous versions to get the list + of contributors for this version is `git shortlog -s -n + VX.X+alpha..master | cut -f2 | sort -k 2`. Note that the ordering is + approximative as it will misplace people with middle names. It is + also probably not correctly handling `Co-authored-by` info that we + have been using more lately, so should probably be updated to + account for this. ## On the date of the feature freeze ## - [ ] Create the new version branch `vX.X` (using this name will ensure that the branch will be automatically protected). +- [ ] Pin the versions of libraries and plugins in + `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it + exists, a branch dedicated to compatibility with the corresponding + Coq branch). - [ ] 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. +- [ ] Start a new project to track PR backporting. The project should + have a "Request X.X+beta1 inclusion" column for the PRs that were + merged in `master` that are to be considered for backporting, and a + "Shipped in X.X+beta1" columns to put what was backported. A message + to **@coqbot** in the milestone description tells it to + automatically add merged PRs to the "Request ... inclusion" column + and backported PRs to the "Shipped in ..." column. See previous + milestones for examples. When moving to the next milestone + (e.g. X.X.0), you can clear and remove the "Request X.X+beta1 + inclusion" column and create new "Request X.X.0 inclusion" and + "Shipped in X.X.0" columns. + + The release manager is the person responsible for merging PRs that + target the version branch and backporting appropriate PRs that are + merged into `master`. - [ ] 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. @@ -80,6 +99,11 @@ ## Before the beta release date ## - [ ] Ensure the Credits chapter has been updated. +- [ ] Prepare the release notes (see e.g., + [#10833](https://github.com/coq/coq/pull/10833)): in a PR against the `master` + branch, move the contents from all files of `doc/changelog/` that appear in + the release branch into the manual `doc/sphinx/changes.rst`. Merge that PR + into the `master` branch and backport it to the version branch. - [ ] 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 @@ -120,6 +144,7 @@ ## At the final release time ## +- [ ] Prepare the release notes (see above) - [ ] In a PR: - Change the version name from X.X.0 and the magic numbers (see [#7271](https://github.com/coq/coq/pull/7271/files)). diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index d1b98b94a3..75c8c6c1ea 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -627,5 +627,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq88.v theories/Compat/Coq89.v theories/Compat/Coq810.v + theories/Compat/Coq811.v </dd> </dl> diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 0951b07d49..b88a2e6194 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -161,7 +161,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Id.Set.t option; } let expmod_constr_subst cache modlist subst c = @@ -242,11 +242,7 @@ let cook_constant { from = cb; info } = OpaqueDef (Opaqueproof.discharge_direct_opaque info o) | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in - let const_hyps = - Context.Named.fold_outside (fun decl hyps -> - List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) - hyps) - hyps0 ~init:cb.const_hyps in + let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in let typ = abstract_constant_type (expmod cb.const_type) hyps in { cook_body = body; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 671cdf51fe..83a8b9edfc 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Names.Id.Set.t option; } val cook_constant : recipe -> Opaqueproof.opaque result diff --git a/kernel/entries.ml b/kernel/entries.ml index 47e2f72b0e..1e6bc14935 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -61,7 +61,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; (* List of section variables *) - const_entry_secctx : Constr.named_context option; + const_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -70,7 +70,7 @@ type definition_entry = { type section_def_entry = { secdef_body : constr; - secdef_secctx : Constr.named_context option; + secdef_secctx : Id.Set.t option; secdef_feedback : Stateid.t option; secdef_type : types option; } @@ -78,7 +78,7 @@ type section_def_entry = { type 'a opaque_entry = { opaque_entry_body : 'a; (* List of section variables *) - opaque_entry_secctx : Constr.named_context; + opaque_entry_secctx : Id.Set.t; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; @@ -88,7 +88,7 @@ type 'a opaque_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Constr.named_context option * types in_universes_entry * inline + Id.Set.t option * types in_universes_entry * inline type primitive_entry = { prim_entry_type : types option; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4268f0a602..1069d9a62c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -733,7 +733,7 @@ let constant_entry_of_side_effect eff = if Declareops.is_opaque cb then OpaqueEff { opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - opaque_entry_secctx = cb.const_hyps; + opaque_entry_secctx = Context.Named.to_vars cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; @@ -741,7 +741,7 @@ let constant_entry_of_side_effect eff = else DefinitionEff { const_entry_body = p; - const_entry_secctx = Some cb.const_hyps; + const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps); const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; diff --git a/kernel/section.ml b/kernel/section.ml index 4a9b222798..babd9fe7a1 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -146,19 +146,11 @@ let empty_segment = { abstr_uctx = AUContext.empty; } -let extract_hyps sec vars hyps = - (* FIXME: this code is fishy. It is supposed to check that declared section - variables are an ordered subset of the ambient ones, but it doesn't check - e.g. uniqueness of naming nor convertibility of the section data. *) - let rec aux ids hyps = match ids, hyps with - | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) -> - decl :: aux ids hyps - | _ :: ids, hyps -> - aux ids hyps - | [], _ -> [] - in - let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in - aux ids hyps +let extract_hyps sec vars used = + (* Keep the section-local segment of variables *) + let vars = List.firstn sec.sec_context vars in + (* Only keep the part that is used by the declaration *) + List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars let section_segment_of_entry vars e hyps sections = (* [vars] are the named hypotheses, [hyps] the subset that is declared by the @@ -180,12 +172,14 @@ let section_segment_of_entry vars e hyps sections = let segment_of_constant env con s = let body = Environ.lookup_constant con env in let vars = Environ.named_context env in - section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s + let used = Context.Named.to_vars body.Declarations.const_hyps in + section_segment_of_entry vars (SecDefinition con) used s let segment_of_inductive env mind s = let mib = Environ.lookup_mind mind env in let vars = Environ.named_context env in - section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s + let used = Context.Named.to_vars mib.Declarations.mind_hyps in + section_segment_of_entry vars (SecInductive mind) used s let instance_from_variable_context = List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b65e62ba30..f70b2960cf 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -221,9 +221,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in - let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in - let inferred_set, declared_set = mk_set inferred, mk_set declared in + let check declared_set inferred_set = if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in let n = List.length l in @@ -239,11 +237,6 @@ let build_constant_declaration env result = str "Proof using " ++ declared_vars ++ fnl () ++ str "to" ++ fnl () ++ str "Proof using " ++ inferred_vars) in - let sort l = - List.filter (fun decl -> - let id = NamedDecl.get_id decl in - List.exists (NamedDecl.get_id %> Names.Id.equal id) l) - (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in @@ -252,7 +245,7 @@ let build_constant_declaration env result = | None -> if List.is_empty context_ids then (* Empty section context: no need to check *) - [], def + Id.Set.empty, def else (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) @@ -264,16 +257,19 @@ let build_constant_declaration env result = (* Opaque definitions always come with their section variables *) assert false in - keep_hyps env (Id.Set.union ids_typ ids_def), def + Environ.really_needed env (Id.Set.union ids_typ ids_def), def | Some declared -> + let needed = Environ.really_needed env declared in + (* Transitive closure ensured by the upper layers *) + let () = assert (Id.Set.equal needed declared) in (* We use the declared set and chain a check of correctness *) - sort declared, + declared, match def with | Undef _ | Primitive _ as x -> x (* nothing to check *) | Def cs as x -> let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Mod_subst.force_constr cs) in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) @@ -281,12 +277,13 @@ let build_constant_declaration env result = let kont c = let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in check declared inferred in OpaqueDef (iter kont lc) in let univs = result.cook_universes in + let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in let tps = let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in Option.map Cemitcodes.from_val res @@ -317,7 +314,10 @@ let translate_recipe env _kn r = let univs = result.cook_universes in let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in let tps = Option.map Cemitcodes.from_val res in - { const_hyps = Option.get result.cook_context; + let hyps = Option.get result.cook_context in + (* Trust the set of section hypotheses generated by Cooking *) + let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in + { const_hyps = hyps; const_body = result.cook_body; const_type = result.cook_type; const_body_code = tps; diff --git a/lib/flags.ml b/lib/flags.ml index f09dc48f5d..7676665fe9 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -60,7 +60,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_8 | V8_9 | Current +type compat_version = V8_8 | V8_9 | V8_10 | Current let compat_version = ref Current @@ -71,6 +71,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_9, V8_9 -> 0 | V8_9, _ -> -1 | _, V8_9 -> 1 + | V8_10, V8_10 -> 0 + | V8_10, _ -> -1 + | _, V8_10 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -79,6 +82,7 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | V8_8 -> "8.8" | V8_9 -> "8.9" + | V8_10 -> "8.10" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index 185a5f8425..3f72cc4b91 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -48,7 +48,7 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_8 | V8_9 | Current +type compat_version = V8_8 | V8_9 | V8_10 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/tactics/declare.ml b/tactics/declare.ml index e418240d3a..b6a0d9f39a 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -72,7 +72,7 @@ type constant_obj = { type 'a proof_entry = { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) - proof_entry_secctx : Constr.named_context option; + proof_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) proof_entry_feedback : Stateid.t option; proof_entry_type : Constr.types option; @@ -228,7 +228,7 @@ let cast_opaque_proof_entry e = ids_typ, vars in let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in - keep_hyps env (Id.Set.union hyp_typ hyp_def) + Environ.really_needed env (Id.Set.union hyp_typ hyp_def) | Some hyps -> hyps in { diff --git a/tactics/declare.mli b/tactics/declare.mli index 4cb876cecb..da66a2713c 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,7 +23,7 @@ open Entries type 'a proof_entry = { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) - proof_entry_secctx : Constr.named_context option; + proof_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) proof_entry_feedback : Stateid.t option; proof_entry_type : Constr.types option; diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index a2929e45cd..b723922642 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -36,7 +36,7 @@ type opacity_flag = Opaque | Transparent type t = { endline_tactic : Genarg.glob_generic_argument option - ; section_vars : Constr.named_context option + ; section_vars : Id.Set.t option ; proof : Proof.t ; udecl: UState.universe_decl (** Initial universe declarations *) @@ -128,7 +128,7 @@ let set_used_variables ps l = if not (Option.is_empty ps.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), { ps with section_vars = Some ctx} + (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) } let get_open_goals ps = let Proof.{ goals; stack; shelf } = Proof.data ps.proof in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index d15e23c2cc..b9d1b37a11 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -17,7 +17,7 @@ type t (* Should be moved into a proper view *) val get_proof : t -> Proof.t val get_proof_name : t -> Names.Id.t -val get_used_variables : t -> Constr.named_context option +val get_used_variables : t -> Names.Id.Set.t option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : t -> UState.universe_decl diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 81469d79c3..fd6101bf89 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq810. +Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index afeb57f9f2..f774cef44f 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(* -*- coq-prog-args: ("-compat" "8.9") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. Import Coq.Compat.Coq810. Import Coq.Compat.Coq89. -Import Coq.Compat.Coq88. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..20eef955b4 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. +Import Coq.Compat.Coq810. +Import Coq.Compat.Coq89. +Import Coq.Compat.Coq88. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index c8f75915c8..1c5ccc1a92 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq811. Import Coq.Compat.Coq810. -Import Coq.Compat.Coq89. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? diff --git a/theories/Compat/Coq810.v b/theories/Compat/Coq810.v index d24af2186f..c611d356ce 100644 --- a/theories/Compat/Coq810.v +++ b/theories/Compat/Coq810.v @@ -9,3 +9,5 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.10 *) + +Require Export Coq.Compat.Coq811. diff --git a/theories/Compat/Coq811.v b/theories/Compat/Coq811.v new file mode 100644 index 0000000000..4a9a041d4e --- /dev/null +++ b/theories/Compat/Coq811.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.11 *) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index c85b656171..acbd96f699 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -178,7 +178,8 @@ let add_compat_require opts v = match v with | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false) | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) - | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) + | Flags.V8_10 -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) + | Flags.Current -> add_vo_require opts "Coq.Compat.Coq811" None (Some false) let add_load_vernacular opts verb s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 8a94a010a0..efcb2635be 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -62,7 +62,8 @@ let make_bullet s = | _ -> assert false let parse_compat_version = let open Flags in function - | "8.10" -> Current + | "8.11" -> Current + | "8.10" -> V8_10 | "8.9" -> V8_9 | "8.8" -> V8_8 | ("8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 42d1a1f3fc..c7a588d2b4 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -359,7 +359,7 @@ let save_lemma_admitted ~(lemma : t) : unit = let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) + Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None in let universes = Proof_global.get_initial_euctx lemma.proof in let ctx = UState.check_univ_decl ~poly universes udecl in |