diff options
72 files changed, 1064 insertions, 657 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 6c7b7a9a1c..4789d9b6fa 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -333,6 +333,9 @@ azure-pipelines.yml @coq/ci-maintainers /dev/tools/github-check-prs.py @SkySkimmer +/dev/tools/make-changelog.sh @SkySkimmer +# Secondary maintainer @Zimmi48 + /dev/tools/merge-pr.sh @maximedenes # Secondary maintainer @gares 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/checker/check.ml b/checker/check.ml index 69de2536c5..09ecd675f7 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -359,7 +359,7 @@ let intern_from_file ~intern_mode (dir, f) = (* Verification of the unmarshalled values *) validate !Flags.debug Values.v_libsum sd; validate !Flags.debug Values.v_lib md; - validate !Flags.debug Values.(Opt v_opaques) table; + validate !Flags.debug Values.(Opt v_opaquetable) table; Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = if opaque_csts <> None then Safe_typing.Dvivo (digest,udg) diff --git a/checker/values.ml b/checker/values.ml index 6b340635d7..9a2028a96b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -187,10 +187,24 @@ let v_substituted v_a = let v_cstr_subst = v_substituted v_constr -(** NB: Second constructor [Direct] isn't supposed to appear in a .vo *) -let v_lazy_constr = - v_sum "lazy_constr" 0 [|[|List v_subst;v_dp;Int|]|] +let v_ndecl = v_sum "named_declaration" 0 + [| [|v_binder_annot v_id; v_constr|]; (* LocalAssum *) + [|v_binder_annot v_id; v_constr; v_constr|] |] (* LocalDef *) + +let v_nctxt = List v_ndecl + +let v_work_list = + let v_abstr = v_pair v_instance (Array v_id) in + Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|]) + +let v_abstract = + Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |]) +let v_cooking_info = + Tuple ("cooking_info", [|v_work_list; v_abstract|]) + +let v_opaque = + v_sum "opaque" 0 [|[|List v_subst; List v_cooking_info; v_dp; Int|]|] (** kernel/declarations *) @@ -216,7 +230,7 @@ let v_primitive = let v_cst_def = v_sum "constant_def" 0 - [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|] + [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|] let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|] @@ -400,25 +414,9 @@ let v_libsum = let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) -let v_ndecl = v_sum "named_declaration" 0 - [| [|v_binder_annot v_id; v_constr|]; (* LocalAssum *) - [|v_binder_annot v_id; v_constr; v_constr|] |] (* LocalDef *) - -let v_nctxt = List v_ndecl - -let v_work_list = - let v_abstr = v_pair v_instance (Array v_id) in - Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|]) - -let v_abstract = - Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |]) - -let v_cooking_info = - Tuple ("cooking_info", [|v_work_list; v_abstract|]) - let v_delayed_universes = Sum ("delayed_universes", 0, [| [| v_unit |]; [| Int; v_context_set |] |]) -let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Opt (v_pair v_constr v_delayed_universes) |])) +let v_opaquetable = Array (Opt (v_pair v_constr v_delayed_universes)) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) diff --git a/checker/values.mli b/checker/values.mli index 93983eb700..db6b0be250 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -46,5 +46,5 @@ type value = val v_univopaques : value val v_libsum : value val v_lib : value -val v_opaques : value +val v_opaquetable : value val v_stm_seg : value diff --git a/checker/votour.ml b/checker/votour.ml index f0e0cf22ab..5a610e6938 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -366,7 +366,7 @@ let visit_vo f = make_seg "univ constraints of opaque proofs" Values.v_univopaques; make_seg "discharging info" (Opt Any); make_seg "STM tasks" (Opt Values.v_stm_seg); - make_seg "opaque proofs" Values.v_opaques; + make_seg "opaque proofs" Values.v_opaquetable; |] in let repr = if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S) 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/build/windows/patches_coq/ocaml-4.07.1.patch b/dev/build/windows/patches_coq/ocaml-4.07.1.patch index 2d61b5b838..2d61b5b838 100755..100644 --- a/dev/build/windows/patches_coq/ocaml-4.07.1.patch +++ b/dev/build/windows/patches_coq/ocaml-4.07.1.patch diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c index c4c7ec2bff..c4c7ec2bff 100755..100644 --- a/dev/build/windows/patches_coq/pkg-config.c +++ b/dev/build/windows/patches_coq/pkg-config.c 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/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh new file mode 100755 index 0000000000..ea96de970a --- /dev/null +++ b/dev/tools/make-changelog.sh @@ -0,0 +1,25 @@ +#!/bin/sh + +echo "PR number" +read -r PR + +echo "Where? (type a prefix)" +(cd doc/changelog && ls -d */) +read -r where + +where=$(echo doc/changelog/"$where"*) +where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst" + +# shellcheck disable=SC2016 +# the ` are regular strings, this is intended +# use %s for the leading - to avoid looking like an option (not sure +# if necessary but doesn't hurt) +printf '%s bla bla (`#%s <https://github.com/coq/coq/pull/%s>`_, by %s).' - "$PR" "$PR" "$(git config user.name)" > "$where" + +giteditor=$(git config core.editor) +if [ "$giteditor" ]; then + $giteditor "$where" +elif [ "$EDITOR" ]; then + $EDITOR "$where" +else echo "$where" +fi diff --git a/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst b/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst deleted file mode 100644 index d6fc724415..0000000000 --- a/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by - primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_, - fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ - by Vincent Laporte). diff --git a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst new file mode 100644 index 0000000000..580e808baa --- /dev/null +++ b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst @@ -0,0 +1,7 @@ +- Update output generated by :flag:`Printing Dependent Evars Line` flag + used by the Prooftree tool in Proof General. + (`#10489 <https://github.com/coq/coq/pull/10489>`_, + closes `#4504 <https://github.com/coq/coq/issues/4504>`_, + `#10399 <https://github.com/coq/coq/issues/10399>`_ and + `#10400 <https://github.com/coq/coq/issues/10400>`_, + by Jim Fehrle). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 38b3c34209..0148925247 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -718,6 +718,14 @@ Changes in 8.10+beta3 follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_, which added ``uncons`` in 8.10+beta1). +Changes in 8.10.0 +~~~~~~~~~~~~~~~~~ + +- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by + primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_, + fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ + by Vincent Laporte). + Version 8.9 ----------- diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index dc4f91e66b..2d047a1058 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -638,7 +638,11 @@ the induction principle to easily reason about the function. than like this: - .. coqtop:: reset all + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all Function plus (n m : nat) {struct n} : nat := match n with @@ -649,17 +653,22 @@ the induction principle to easily reason about the function. *Limitations* -|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`) +:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of :g:`wrong` in the body of :g:`wrong`: -.. coqtop:: all +.. coqtop:: none + + Require List. + Import List.ListNotations. + +.. coqtop:: all fail - Fail Function wrong (C:nat) : nat := - List.hd 0 (List.map wrong (C::nil)). + Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). For now, dependent cases are not treated for non structurally terminating functions. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 85dfe0e5d2..c910136406 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3005,7 +3005,7 @@ the conversion in hypotheses :n:`{+ @ident}`. flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` and ``cofix``. The ``delta`` flag itself can be refined into - :n:`delta {+ @qualid}` or :n:`delta -{+ @qualid}`, restricting in the first + :n:`delta [ {+ @qualid} ]` or :n:`delta - [ {+ @qualid} ]`, restricting in the first case the constants to unfold to the constants listed, and restricting in the second case the constant to unfold to all but the ones explicitly mentioned. Notice that the ``delta`` flag does not apply to variables bound by a let-in @@ -3049,18 +3049,18 @@ the conversion in hypotheses :n:`{+ @ident}`. This is a synonym for ``lazy beta delta iota zeta``. -.. tacv:: compute {+ @qualid} - cbv {+ @qualid} +.. tacv:: compute [ {+ @qualid} ] + cbv [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. -.. tacv:: compute -{+ @qualid} - cbv -{+ @qualid} +.. tacv:: compute - [ {+ @qualid} ] + cbv - [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. -.. tacv:: lazy {+ @qualid} - lazy -{+ @qualid} +.. tacv:: lazy [ {+ @qualid} ] + lazy - [ {+ @qualid} ] These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` and :n:`lazy beta delta -{+ @qualid} iota zeta`. @@ -3071,7 +3071,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. This algorithm is dramatically more efficient than the algorithm used for the - ``cbv`` tactic, but it cannot be fine-tuned. It is specially interesting for + :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics. @@ -3080,14 +3080,14 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal by compilation to OCaml as described in :cite:`FullReduction`. If Coq is running in native code, it can be - typically two to five times faster than ``vm_compute``. Note however that the + typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive computations. .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this option makes - it possible to profile ``native_compute`` evaluations. + it possible to profile :tacn:`native_compute` evaluations. .. opt:: NativeCompute Profile Filename @string :name: NativeCompute Profile Filename @@ -3097,7 +3097,7 @@ the conversion in hypotheses :n:`{+ @ident}`. will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means you can individually profile multiple uses of - ``native_compute`` in a script. From the Linux command line, run ``perf report`` + :tacn:`native_compute` in a script. From the Linux command line, run ``perf report`` on the profile file to see the results. Consult the ``perf`` documentation for more details. @@ -3153,14 +3153,15 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The ``cbn`` tactic is claimed to be a more principled, faster and more - predictable replacement for ``simpl``. + The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + predictable replacement for :tacn:`simpl`. - The ``cbn`` tactic accepts the same flags as ``cbv`` and ``lazy``. The - behavior of both ``simpl`` and ``cbn`` can be tuned using the - Arguments vernacular command as follows: + The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and + :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn` + can be tuned using the Arguments vernacular command as follows: - + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``: + + A constant can be marked to be never unfolded by :tacn:`cbn` or + :tacn:`simpl`: .. example:: @@ -3169,7 +3170,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus n m : simpl never. After that command an expression like :g:`(minus (S x) y)` is left - untouched by the tactics ``cbn`` and ``simpl``. + untouched by the tactics :tacn:`cbn` and :tacn:`simpl`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the @@ -3184,7 +3185,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by - ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. + :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. The same mechanism can be used to make a constant volatile, i.e. always unfolded. @@ -3206,7 +3207,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus !n !m. After that command, the expression :g:`(minus (S x) y)` is left untouched - by ``simpl``, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + A special heuristic to determine if a constant has to be unfolded can be activated with the following command: @@ -3222,25 +3223,25 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)` even if an extra simplification is possible. - In detail, the tactic ``simpl`` first applies :math:`\beta`:math:`\iota`-reduction. Then, it + In detail, the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`- reduction. But, when no :math:`\iota` rule is applied after unfolding then - :math:`\delta`-reductions are not applied. For instance trying to use ``simpl`` on + :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on :g:`(plus n O) = n` changes nothing. Notice that only transparent constants whose name can be reused in the - recursive calls are possibly unfolded by ``simpl``. For instance a + recursive calls are possibly unfolded by :tacn:`simpl`. For instance a constant defined by :g:`plus' := plus` is possibly unfolded and reused in the recursive calls, but a constant such as :g:`succ := plus (S O)` is - never unfolded. This is the main difference between ``simpl`` and ``cbn``. - The tactic ``cbn`` reduces whenever it will be able to reuse it or not: + never unfolded. This is the main difference between :tacn:`simpl` and :tacn:`cbn`. + The tactic :tacn:`cbn` reduces whenever it will be able to reuse it or not: :g:`succ t` is reduced to :g:`S t`. -.. tacv:: cbn {+ @qualid} - cbn -{+ @qualid} +.. tacv:: cbn [ {+ @qualid} ] + cbn - [ {+ @qualid} ] - These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta` - and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`). + These are respectively synonyms of :n:`cbn beta delta [ {+ @qualid} ] iota zeta` + and :n:`cbn beta delta - [ {+ @qualid} ] iota zeta` (see :tacn:`cbn`). .. tacv:: simpl @pattern @@ -3249,7 +3250,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @pattern at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. @@ -3265,7 +3266,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @qualid at {+ @num} simpl @string at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose + This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). .. flag:: Debug RAKAM diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 2885d6dc33..843459b723 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1012,8 +1012,9 @@ Controlling display .. flag:: Printing Dependent Evars Line - This option controls the printing of the “(dependent evars: …)” line when - ``-emacs`` is passed. + This option controls the printing of the “(dependent evars: …)” information + after each tactic. The information is used by the Prooftree tool in Proof + General. (https://askra.de/software/prooftree) .. _vernac-controlling-the-reduction-strategies: 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/engine/evarutil.ml b/engine/evarutil.ml index c946125d3f..5444d88e47 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -661,26 +661,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids = (* spiwack: a few functions to gather evars on which goals depend. *) let queue_set q is_dependent set = Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set -let queue_term evm q is_dependent c = - queue_set q is_dependent (evars_of_term evm c) +let queue_term q is_dependent c = + queue_set q is_dependent (evar_nodes_of_term c) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in (* Queues evars appearing in the types of the goal (conclusion, then hypotheses), they are all dependent. *) - queue_term evm q true evi.evar_concl; + queue_term q true evi.evar_concl; List.iter begin fun decl -> let open NamedDecl in - queue_term evm q true (NamedDecl.get_type decl); + queue_term q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () - | LocalDef (_,b,_) -> queue_term evm q true b + | LocalDef (_,b,_) -> queue_term q true b end (EConstr.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term evm b in + let subevars = evar_nodes_of_term b in (* evars appearing in the definition of an evar [e] are marked as dependent when [e] is dependent itself: if [e] is a non-dependent goal, then, unless they are reach from another diff --git a/engine/evd.ml b/engine/evd.ml index 6a721a1a8a..099c83abf1 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1403,7 +1403,16 @@ end let evars_of_term evd c = let rec evrec acc c = - match MiniEConstr.kind evd c with + let c = MiniEConstr.whd_evar evd c in + match kind c with + | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) + | _ -> Constr.fold evrec acc c + in + evrec Evar.Set.empty c + +let evar_nodes_of_term c = + let rec evrec acc c = + match kind c with | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) | _ -> Constr.fold evrec acc c in diff --git a/engine/evd.mli b/engine/evd.mli index 132f7bc745..5ab53947f7 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -509,6 +509,10 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option val evars_of_term : evar_map -> econstr -> Evar.Set.t (** including evars in instances of evars *) +val evar_nodes_of_term : econstr -> Evar.Set.t + (** same as evars_of_term but also including defined evars. + For use in printing dependent evars *) + val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t diff --git a/engine/proofview.ml b/engine/proofview.ml index 1f076470c1..d6f5aab1d1 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1247,7 +1247,7 @@ module V82 = struct let top_evars initial { solution=sigma; } = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term sigma c) + Evar.Set.elements (Evd.evar_nodes_of_term c) in CList.flatten (CList.map evars_of_initial initial) diff --git a/ide/coq2.ico b/ide/coq2.ico Binary files differindex bc1732fd99..bc1732fd99 100755..100644 --- a/ide/coq2.ico +++ b/ide/coq2.ico diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 0951b07d49..fae06f7163 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 = @@ -239,14 +239,10 @@ let cook_constant { from = cb; info } = | Undef _ as x -> x | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) | OpaqueDef o -> - OpaqueDef (Opaqueproof.discharge_direct_opaque info o) + OpaqueDef (Opaqueproof.discharge_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/opaqueproof.ml b/kernel/opaqueproof.ml index f0ffd2e073..f0b706e4f5 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -24,7 +24,7 @@ type 'a delayed_universes = | PrivateMonomorphic of 'a | PrivatePolymorphic of int * Univ.ContextSet.t -type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option +type opaque_proofterm = (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; @@ -38,10 +38,10 @@ let drop_mono = function type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation type opaque = - | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) - | Direct of cooking_info list * proofterm +| Indirect of substitution list * cooking_info list * DirPath.t * int (* subst, discharge, lib, index *) + type opaquetab = { - opaque_val : (cooking_info list * proofterm) Int.Map.t; + opaque_val : proofterm Int.Map.t; (** Actual proof terms *) opaque_len : int; (** Size of the above map *) @@ -56,44 +56,33 @@ let empty_opaquetab = { let not_here () = CErrors.user_err Pp.(str "Cannot access opaque delayed proof") -let create cu = Direct ([],cu) - -let turn_indirect dp o tab = match o with - | Indirect (_,_,i) -> - if not (Int.Map.mem i tab.opaque_val) - then CErrors.anomaly (Pp.str "Indirect in a different table.") - else CErrors.anomaly (Pp.str "Already an indirect opaque.") - | Direct (d, cu) -> - (* Invariant: direct opaques only exist inside sections, we turn them - indirect as soon as we are at toplevel. At this moment, we perform - hashconsing of their contents, potentially as a future. *) - let hcons (c, u) = - let c = Constr.hcons c in - let u = match u with - | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) - | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) - in - (c, u) - in - let cu = Future.chain cu hcons in - let id = tab.opaque_len in - let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in - let opaque_dir = - if DirPath.equal dp tab.opaque_dir then tab.opaque_dir - else if DirPath.equal tab.opaque_dir DirPath.initial then dp - else CErrors.anomaly - (Pp.str "Using the same opaque table for multiple dirpaths.") in - let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in - Indirect ([],dp,id), ntab +let create dp cu tab = + let hcons (c, u) = + let c = Constr.hcons c in + let u = match u with + | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) + | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) + in + (c, u) + in + let cu = Future.chain cu hcons in + let id = tab.opaque_len in + let opaque_val = Int.Map.add id cu tab.opaque_val in + let opaque_dir = + if DirPath.equal dp tab.opaque_dir then tab.opaque_dir + else if DirPath.equal tab.opaque_dir DirPath.initial then dp + else CErrors.anomaly + (Pp.str "Using the same opaque table for multiple dirpaths.") in + let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in + Indirect ([], [], dp, id), ntab let subst_opaque sub = function - | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) - | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") +| Indirect (s, ci, dp, i) -> Indirect (sub :: s, ci, dp, i) -let discharge_direct_opaque ci = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d, cu) -> - Direct (ci :: d, cu) +let discharge_opaque info = function +| Indirect (s, ci, dp, i) -> + assert (CList.is_empty s); + Indirect ([], info :: ci, dp, i) let join except cu = match except with | None -> ignore (Future.join cu) @@ -102,25 +91,21 @@ let join except cu = match except with else ignore (Future.join cu) let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> join except cu - | Indirect (_,dp,i) -> - if DirPath.equal dp odp then - let (_, fp) = Int.Map.find i prfs in - join except fp +| Indirect (_,_,dp,i) -> + if DirPath.equal dp odp then + let fp = Int.Map.find i prfs in + join except fp let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (d, cu) -> - let (c, u) = Future.force cu in - access.access_discharge d (c, drop_mono u) - | Indirect (l,dp,i) -> + | Indirect (l,d,dp,i) -> let c, u = if DirPath.equal dp odp then - let (d, cu) = Int.Map.find i prfs in + let cu = Int.Map.find i prfs in let (c, u) = Future.force cu in access.access_discharge d (c, drop_mono u) else - let (d, cu) = access.access_proof dp i in + let cu = access.access_proof dp i in match cu with | None -> not_here () | Some (c, u) -> access.access_discharge d (c, u) @@ -133,21 +118,19 @@ let get_mono (_, u) = match u with | PrivatePolymorphic _ -> Univ.ContextSet.empty let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> - get_mono (Future.force cu) - | Indirect (_,dp,i) -> +| Indirect (_,_,dp,i) -> if DirPath.equal dp odp then - let ( _, cu) = Int.Map.find i prfs in + let cu = Int.Map.find i prfs in get_mono (Future.force cu) else Univ.ContextSet.empty module FMap = Future.UUIDMap let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = - let opaque_table = Array.make n ([], None) in + let opaque_table = Array.make n None in let f2t_map = ref FMap.empty in - let iter n (d, cu) = + let iter n cu = let uid = Future.uuid cu in let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in let c = @@ -160,7 +143,7 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ CErrors.anomaly Pp.(str"Proof object "++int n++str" is not checked nor to be checked") in - opaque_table.(n) <- (d, c) + opaque_table.(n) <- c in let () = Int.Map.iter iter otab in opaque_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 758a9f5107..1870241dcd 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -16,10 +16,7 @@ open Mod_subst Opaque proof terms are special since: - they can be lazily computed and substituted - they are stored in an optionally loaded segment of .vo files - An [opaque] proof terms holds the real data until fully discharged. - In this case it is called [direct]. - When it is [turn_indirect] the data is relocated to an opaque table - and the [opaque] is turned into an index. *) + An [opaque] proof terms holds an index into an opaque table. *) type 'a delayed_universes = | PrivateMonomorphic of 'a @@ -33,12 +30,7 @@ type opaque val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) -val create : proofterm -> opaque - -(** Turn a direct [opaque] into an indirect one. It is your responsibility to - hashcons the inner term beforehand. The integer is an hint of the maximum id - used so far *) -val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab +val create : DirPath.t -> proofterm -> opaquetab -> opaque * opaquetab type work_list = (Univ.Instance.t * Id.t array) Cmap.t * (Univ.Instance.t * Id.t array) Mindmap.t @@ -47,14 +39,14 @@ type cooking_info = { modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } -type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option +type opaque_proofterm = (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); } -(** When stored indirectly, opaque terms are indexed by their library +(** Opaque terms are indexed by their library dirpath and an integer index. The two functions above activate this indirect storage, by telling how to retrieve terms. *) @@ -66,7 +58,7 @@ val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.Context val subst_opaque : substitution -> opaque -> opaque -val discharge_direct_opaque : +val discharge_opaque : cooking_info -> opaque -> opaque val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4268f0a602..9b4d2e69ac 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -591,17 +591,6 @@ let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn in (* This is the only place where we hashcons the contents of a constant body *) let cb = if in_section then cb else Declareops.hcons_const_body cb in - let cb, otab = match cb.const_body with - | OpaqueDef lc when not in_section -> - (* In coqc, opaque constants outside sections will be stored - indirectly in a specific table *) - let od, otab = - Opaqueproof.turn_indirect - (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in - { cb with const_body = OpaqueDef od }, otab - | _ -> cb, (Environ.opaque_tables senv.env) - in - let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with | Undef (Some lev) -> @@ -733,7 +722,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 +730,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; @@ -805,17 +794,25 @@ let export_side_effects mb env (b_ctx, eff) = in translate_seff trusted seff [] env +let push_opaque_proof pf senv = + let o, otab = Opaqueproof.create (library_dp_of_senv senv) pf (Environ.opaque_tables senv.env) in + let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in + senv, o + let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map univs p = - let local = match univs with + let map senv (kn, c) = match c.const_body with + | OpaqueDef p -> + let local = match c.const_universes with | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) in - Opaqueproof.create (Future.from_val (p, local)) + let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in + senv, (kn, { c with const_body = OpaqueDef o }) + | Def _ | Undef _ | Primitive _ as body -> + senv, (kn, { c with const_body = body }) in - let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in - let bodies = List.map map exported in + let senv, bodies = List.fold_left_map map senv exported in let exported = List.map (fun (kn, _) -> kn) exported in (* No delayed constants to declare *) let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in @@ -836,20 +833,25 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen Term_typing.translate_constant Term_typing.Pure senv.env kn ce in let senv = - let delayed_cst = match cb.const_body with - | OpaqueDef fc when not (Declareops.constant_is_polymorphic cb) -> - let map (_, u) = match u with - | Opaqueproof.PrivateMonomorphic ctx -> ctx - | Opaqueproof.PrivatePolymorphic _ -> assert false + let senv, cb, delayed_cst = match cb.const_body with + | OpaqueDef fc -> + let senv, o = push_opaque_proof fc senv in + let delayed_cst = + if not (Declareops.constant_is_polymorphic cb) then + let map (_, u) = match u with + | Opaqueproof.PrivateMonomorphic ctx -> ctx + | Opaqueproof.PrivatePolymorphic _ -> assert false + in + let fc = Future.chain fc map in + match Future.peek_val fc with + | None -> [Later fc] + | Some c -> [Now c] + else [] in - let fc = Future.chain fc map in - begin match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now c] - end - | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] + senv, { cb with const_body = OpaqueDef o }, delayed_cst + | Undef _ | Def _ | Primitive _ as body -> + senv, { cb with const_body = body }, [] in - let cb = map_constant (fun c -> Opaqueproof.create c) cb in let senv = add_constant_aux ~in_section senv (kn, cb) in add_constraints_list delayed_cst senv in @@ -985,6 +987,9 @@ let close_section senv = that are going to be replayed. Those that are not forced are not readded by {!add_constant_aux}. *) let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in + (* Do not revert the opaque table, the discharged opaque constants are + referring to it. *) + let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in let senv = { senv with env; revstruct; sections; univ; objlabels; } in (* Second phase: replay the discharged section contents *) let senv = add_constraints (Now cstrs) senv in 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/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index a98a963207..dc096554c8 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -828,31 +828,31 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk := end in ring_elements set ext rspec pspec sspec dspec rk ltac:(fun arth ext_r morph p_spec s_spec d_spec => - match type of morph with + lazymatch type of morph with | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => let gen_lemma2_0 := constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth C c0 c1 cadd cmul csub copp ceq_b phi morph) in - match p_spec with + lazymatch p_spec with | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec => let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in - match d_spec with + lazymatch d_spec with | @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec => let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in - match s_spec with + lazymatch s_spec with | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec => let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in let lemma1 := constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in fun f => f arth ext_r morph lemma1 lemma2 - | _ => fail 4 "ring: bad sign specification" + | _ => fail "ring: bad sign specification" end - | _ => fail 3 "ring: bad coefficient division specification" + | _ => fail "ring: bad coefficient division specification" end - | _ => fail 2 "ring: bad power specification" + | _ => fail "ring: bad power specification" end - | _ => fail 1 "ring internal error: ring_lemmas, please report" + | _ => fail "ring internal error: ring_lemmas, please report" end). (* Tactic for constant *) diff --git a/printing/printer.ml b/printing/printer.ml index 328082fbc2..10a31ac256 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -635,27 +635,34 @@ let () = optwrite = (fun v -> should_print_dependent_evars := v) } let print_dependent_evars gl sigma seeds = - let constraints = print_evar_constraints gl sigma in - let evars () = - if !should_print_dependent_evars then - let evars = Evarutil.gather_dependent_evars sigma seeds in - let evars = - Evar.Map.fold begin fun e i s -> - let e' = pr_internal_existential_key e in - match i with - | None -> s ++ str" " ++ e' ++ str " open," - | Some i -> - s ++ str " " ++ e' ++ str " using " ++ - Evar.Set.fold begin fun d s -> - pr_internal_existential_key d ++ str " " ++ s - end i (str ",") - end evars (str "") + if !should_print_dependent_evars then + let mt_pp = mt () in + let evars = Evarutil.gather_dependent_evars sigma seeds in + let evars_pp = Evar.Map.fold (fun e i s -> + let e' = pr_internal_existential_key e in + let sep = if s = mt_pp then "" else ", " in + s ++ str sep ++ e' ++ + (match i with + | None -> str ":" ++ (Termops.pr_existential_key sigma e) + | Some i -> + let using = Evar.Set.fold (fun d s -> + s ++ str " " ++ (pr_internal_existential_key d)) + i mt_pp in + str " using" ++ using)) + evars mt_pp + in + let evars_current_pp = match gl with + | None -> mt_pp + | Some gl -> + let evars_current = Evarutil.gather_dependent_evars sigma [ gl ] in + Evar.Map.fold (fun e _ s -> + s ++ str " " ++ (pr_internal_existential_key e)) + evars_current mt_pp in cut () ++ cut () ++ - str "(dependent evars:" ++ evars ++ str ")" - else mt () - in - constraints ++ evars () + str "(dependent evars: " ++ evars_pp ++ + str "; in current goal:" ++ evars_current_pp ++ str ")" + else mt () module GoalMap = Evar.Map @@ -732,6 +739,10 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map else pr_rec 1 (g::l) in + let pr_evar_info gl sigma seeds = + let first_goal = if pr_first then gl else None in + print_evar_constraints gl sigma ++ print_dependent_evars first_goal sigma seeds + in (* Side effect! This has to be made more robust *) let () = match close_cmd with @@ -742,23 +753,21 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map (* Main function *) match goals with | [] -> - begin - let exl = Evd.undefined_map sigma in - if Evar.Map.is_empty exl then - (str"No more subgoals." ++ print_dependent_evars None sigma seeds) - else - let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in - v 0 ((str "No more subgoals," - ++ str " but there are non-instantiated existential variables:" - ++ cut () ++ (hov 0 pei) - ++ print_dependent_evars None sigma seeds - ++ cut () ++ str "You can use Grab Existential Variables.")) - end + let exl = Evd.undefined_map sigma in + if Evar.Map.is_empty exl then + v 0 (str "No more subgoals." ++ pr_evar_info None sigma seeds) + else + let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in + v 0 ((str "No more subgoals," + ++ str " but there are non-instantiated existential variables:" + ++ cut () ++ (hov 0 pei) + ++ pr_evar_info None sigma seeds + ++ cut () ++ str "You can use Grab Existential Variables.")) | g1::rest -> let goals = print_multiple_goals g1 rest in let ngoals = List.length rest+1 in v 0 ( - int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") + int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ print_extra ++ str (if (should_gname()) then ", subgoal 1" else "") ++ (if should_tag() then pr_goal_tag g1 else str"") @@ -766,7 +775,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map ++ (if unfocused=[] then str "" else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() ++ pr_rec (List.length rest + 2) unfocused)) - ++ print_dependent_evars (Some g1) sigma seeds + ++ pr_evar_info (Some g1) sigma seeds ) let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = diff --git a/printing/printer.mli b/printing/printer.mli index d62d3789d3..87b09ff755 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -186,6 +186,7 @@ val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t val print_and_diff : Proof.t option -> Proof.t option -> unit +val print_dependent_evars : Evar.t option -> evar_map -> Evar.t list -> Pp.t (** Declarations for the "Print Assumption" command *) type axiom = diff --git a/stm/stm.ml b/stm/stm.ml index 1042061021..5c6df26cbb 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1056,7 +1056,7 @@ end (* }}} *) (* Wrapper for the proof-closing special path for Qed *) let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t = set_id_for_feedback ?route dummy_doc id; - Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) + Vernacinterp.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly @@ -1083,7 +1083,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t = (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else begin stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - Vernacentries.interp ?verbosely:(Some verbose) ~st expr + Vernacinterp.interp ?verbosely:(Some verbose) ~st expr end (****************************** CRUFT *****************************************) @@ -1743,9 +1743,9 @@ end = struct (* {{{ *) assert (Univ.ContextSet.is_empty uctx) in let pr = Constr.hcons pr in - let (ci, dummy) = p.(bucket) in + let dummy = p.(bucket) in let () = assert (Option.is_empty dummy) in - p.(bucket) <- ci, Some (pr, priv); + p.(bucket) <- Some (pr, priv); Univ.ContextSet.union cst uc, false let check_task name l i = @@ -1970,7 +1970,7 @@ end = struct (* {{{ *) let stm_fail ~st fail f = if fail then - Vernacentries.with_fail ~st f + Vernacinterp.with_fail ~st f else f () @@ -2891,7 +2891,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) |> Exninfo.iraise else - let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in + let proof_mode = Some (Vernacinterp.get_default_proof_mode ()) in let id = VCS.new_node ~id:newtip proof_mode () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 8d600c2859..24976d8c1f 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -51,7 +51,7 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] let options_affecting_stm_scheduling = [ Attributes.universe_polymorphism_option_name; stm_allow_nested_proofs_option_name; - Vernacentries.proof_mode_opt_name; + Vernacinterp.proof_mode_opt_name; Attributes.program_mode_option_name; Proof_using.proof_using_opt_name; ] diff --git a/tactics/declare.ml b/tactics/declare.ml index 32447f31c1..3590146dfb 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -68,7 +68,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; @@ -224,7 +224,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 { @@ -341,7 +341,7 @@ let declare_variable ~name ~kind d = in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); Decls.(add_variable_data name {opaque;kind}); - add_anonymous_leaf (inVariable ()); + ignore(add_leaf name (inVariable ()) : Libobject.object_name); Impargs.declare_var_implicits ~impl name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) diff --git a/tactics/declare.mli b/tactics/declare.mli index d479b75a28..f4bfdb1547 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/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out new file mode 100644 index 0000000000..9ca3fa3357 --- /dev/null +++ b/test-suite/output-coqtop/DependentEvars.out @@ -0,0 +1,91 @@ + +Coq < +Coq < Coq < 1 subgoal + + ============================ + forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R + +(dependent evars: ; in current goal:) + +strange_imp_trans < +strange_imp_trans < No more subgoals. + +(dependent evars: ; in current goal:) + +strange_imp_trans < +Coq < Coq < 1 subgoal + + ============================ + forall P Q : Prop, (P -> Q) /\ P -> Q + +(dependent evars: ; in current goal:) + +modpon < +modpon < No more subgoals. + +(dependent evars: ; in current goal:) + +modpon < +Coq < Coq < +Coq < P1 is declared +P2 is declared +P3 is declared +P4 is declared + +Coq < p12 is declared + +Coq < p123 is declared + +Coq < p34 is declared + +Coq < Coq < 1 subgoal + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + P4 + +(dependent evars: ; in current goal:) + +p14 < +p14 < 4 focused subgoals +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?Q -> P4 + +subgoal 2 is: + ?P -> ?Q +subgoal 3 is: + ?P -> ?Q +subgoal 4 is: + ?P + +(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5) + +p14 < 3 focused subgoals +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?P -> (?Goal2 -> P4) /\ ?Goal2 + +subgoal 2 is: + ?P -> (?Goal2 -> P4) /\ ?Goal2 +subgoal 3 is: + ?P + +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11) + +p14 < +Coq < +Coq < diff --git a/test-suite/output-coqtop/DependentEvars.v b/test-suite/output-coqtop/DependentEvars.v new file mode 100644 index 0000000000..5a59054073 --- /dev/null +++ b/test-suite/output-coqtop/DependentEvars.v @@ -0,0 +1,24 @@ +Set Printing Dependent Evars Line. +Lemma strange_imp_trans : + forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R. +Proof. + auto. +Qed. + +Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q. +Proof. + tauto. +Qed. + +Section eex. + Variables P1 P2 P3 P4 : Prop. + Hypothesis p12 : P1 -> P2. + Hypothesis p123 : (P1 -> P2) -> P3. + Hypothesis p34 : P3 -> P4. + + Lemma p14 : P4. + Proof. + eapply strange_imp_trans. + apply modpon. + Abort. +End eex. diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out new file mode 100644 index 0000000000..29ebba7c86 --- /dev/null +++ b/test-suite/output-coqtop/DependentEvars2.out @@ -0,0 +1,120 @@ + +Coq < +Coq < Coq < 1 subgoal + + ============================ + forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R + +(dependent evars: ; in current goal:) + +strange_imp_trans < +strange_imp_trans < No more subgoals. + +(dependent evars: ; in current goal:) + +strange_imp_trans < +Coq < Coq < 1 subgoal + + ============================ + forall P Q : Prop, (P -> Q) /\ P -> Q + +(dependent evars: ; in current goal:) + +modpon < +modpon < No more subgoals. + +(dependent evars: ; in current goal:) + +modpon < +Coq < Coq < +Coq < P1 is declared +P2 is declared +P3 is declared +P4 is declared + +Coq < p12 is declared + +Coq < p123 is declared + +Coq < p34 is declared + +Coq < Coq < 1 subgoal + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + P4 + +(dependent evars: ; in current goal:) + +p14 < +p14 < Second proof: + +p14 < 4 focused subgoals +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?Q -> P4 + +subgoal 2 is: + ?P -> ?Q +subgoal 3 is: + ?P -> ?Q +subgoal 4 is: + ?P + +(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5) + +p14 < 1 focused subgoal +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?Q -> P4 + +(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5) + +p14 < This subproof is complete, but there are some unfocused goals. +Try unfocusing with "}". + +3 subgoals +(shelved: 2) + +subgoal 1 is: + ?P -> (?Goal2 -> P4) /\ ?Goal2 +subgoal 2 is: + ?P -> (?Goal2 -> P4) /\ ?Goal2 +subgoal 3 is: + ?P + +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:) + +p14 < 3 focused subgoals +(shelved: 2) + + P1, P2, P3, P4 : Prop + p12 : P1 -> P2 + p123 : (P1 -> P2) -> P3 + p34 : P3 -> P4 + ============================ + ?P -> (?Goal2 -> P4) /\ ?Goal2 + +subgoal 2 is: + ?P -> (?Goal2 -> P4) /\ ?Goal2 +subgoal 3 is: + ?P + +(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11) + +p14 < +Coq < +Coq < diff --git a/test-suite/output-coqtop/DependentEvars2.v b/test-suite/output-coqtop/DependentEvars2.v new file mode 100644 index 0000000000..d0f3a4012e --- /dev/null +++ b/test-suite/output-coqtop/DependentEvars2.v @@ -0,0 +1,27 @@ +Set Printing Dependent Evars Line. +Lemma strange_imp_trans : + forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R. +Proof. + auto. +Qed. + +Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q. +Proof. + tauto. +Qed. + +Section eex. + Variables P1 P2 P3 P4 : Prop. + Hypothesis p12 : P1 -> P2. + Hypothesis p123 : (P1 -> P2) -> P3. + Hypothesis p34 : P3 -> P4. + + Lemma p14 : P4. + Proof. + idtac "Second proof:". + eapply strange_imp_trans. + { + apply modpon. + } + Abort. +End eex. 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 113b1fb5d7..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 }} @@ -497,7 +498,7 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true }}} - |"-test-mode" -> Vernacentries.test_mode := true; oval + |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 07466d641e..1f319d2bfd 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -405,7 +405,17 @@ let rec vernac_loop ~state = | Some (VernacShowGoal {gid; sid}) -> let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in - Feedback.msg_notice (Printer.pr_goal_emacs ~proof gid sid); + let goal = Printer.pr_goal_emacs ~proof gid sid in + let evars = + match proof with + | None -> mt() + | Some p -> + let gl = (Evar.unsafe_of_int gid) in + let { Proof.sigma } = Proof.data p in + try Printer.print_dependent_evars (Some gl) sigma [ gl ] + with Not_found -> mt() + in + Feedback.msg_notice (v 0 (goal ++ evars)); vernac_loop ~state | None -> diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v index d808436e13..d808436e13 100755..100644 --- a/user-contrib/Ltac2/Bool.v +++ b/user-contrib/Ltac2/Bool.v diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 88454ff2fb..88454ff2fb 100755..100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v 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 b4875bbdd2..e49277c51b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -360,7 +360,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 diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index d9d993f5b5..afc701edbc 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -33,10 +33,9 @@ ComFixpoint ComProgramFixpoint Record Assumptions -Vernacstate Mltop Topfmt Loadpath Vernacentries - -Misctypes +Vernacstate +Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 87abb9da59..4734ce1fb9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -35,12 +35,6 @@ module NamedDecl = Context.Named.Declaration (** TODO: make this function independent of Ltac *) let (f_interp_redexp, interp_redexp_hook) = Hook.make () -let debug = false - -(* XXX Should move to a common library *) -let vernac_pperr_endline pp = - if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () - (* Utility functions, at some point they should all disappear and instead enviroment/state selection should be done at the Vernac DSL level. *) @@ -468,28 +462,6 @@ let vernac_notation ~atts = let vernac_custom_entry ~module_local s = Metasyntax.declare_custom_entry module_local s -(* Default proof mode, to be set at the beginning of proofs for - programs that cannot be statically classified. *) -let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) -let get_default_proof_mode () = !default_proof_mode - -let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode -let set_default_proof_mode_opt name = - default_proof_mode := - match Pvernac.lookup_proof_mode name with - | Some pm -> pm - | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.declare_string_option Goptions.{ - optdepr = false; - optname = "default proof mode" ; - optkey = proof_mode_opt_name; - optread = get_default_proof_mode_opt; - optwrite = set_default_proof_mode_opt; - } - (***********) (* Gallina *) @@ -2237,115 +2209,9 @@ let vernac_check_guard ~pstate = (str ("Condition violated: ") ++s) in message -(** A global default timeout, controlled by option "Set Default Timeout n". - Use "Unset Default Timeout" to deactivate it (or set it to 0). *) - -let default_timeout = ref None - -(* Timeout *) -let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b = - match !default_timeout, timeout with - | _, Some n - | Some n, None -> - Control.timeout n f x Timeout - | None, None -> - f x - -(* Fail *) -let test_mode = ref false - -(* Restoring the state is the caller's responsibility *) -let with_fail f : (Pp.t, unit) result = - try - let _ = f () in - Error () - with - (* Fail Timeout is a common pattern so we need to support it. *) - | e when CErrors.noncritical e || e = Timeout -> - (* The error has to be printed in the failing state *) - Ok CErrors.(iprint (push e)) - -(* We restore the state always *) -let with_fail ~st f = - let res = with_fail f in - Vernacstate.invalidate_cache (); - Vernacstate.unfreeze_interp_state st; - match res with - | Error () -> - user_err ~hdr:"Fail" (str "The command has not failed!") - | Ok msg -> - if not !Flags.quiet || !test_mode - then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg) - -let locate_if_not_already ?loc (e, info) = - match Loc.get_loc info with - | None -> (e, Option.cata (Loc.add_loc info) info loc) - | Some l -> (e, info) - -let mk_time_header = - (* Drop the time header to print the command, we should indeed use a - different mechanism to `-time` commands than the current hack of - adding a time control to the AST. *) - let pr_time_header vernac = - let vernac = match vernac with - | { v = { control = ControlTime _ :: control; attrs; expr }; loc } -> - CAst.make ?loc { control; attrs; expr } - | _ -> vernac - in - Topfmt.pr_cmd_header vernac - in - fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) - -let interp_control_flag ~time_header (f : control_flag) ~st - (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = - match f with - | ControlFail -> - with_fail ~st (fun () -> fn ~st); - st.Vernacstate.lemmas - | ControlTimeout timeout -> - vernac_timeout ~timeout (fun () -> fn ~st) () - | ControlTime batch -> - let header = if batch then Lazy.force time_header else Pp.mt () in - System.with_time ~batch ~header (fun () -> fn ~st) () - | ControlRedirect s -> - Topfmt.with_output_to_file s (fun () -> fn ~st) () - -(* EJGA: We may remove this, only used twice below *) -let vernac_require_open_lemma ~stack f = - match stack with - | Some stack -> f stack - | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)") - -let interp_typed_vernac c ~stack = - let open Vernacextend in - match c with - | VtDefault f -> f (); stack - | VtNoProof f -> - if Option.has_some stack then - user_err Pp.(str "Command not supported (Open proofs remain)"); - let () = f () in - stack - | VtCloseProof f -> - vernac_require_open_lemma ~stack (fun stack -> - let lemma, stack = Vernacstate.LemmaStack.pop stack in - f ~lemma; - stack) - | VtOpenProof f -> - Some (Vernacstate.LemmaStack.push stack (f ())) - | VtModifyProof f -> - Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack - | VtReadProofOpt f -> - let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in - f ~pstate; - stack - | VtReadProof f -> - vernac_require_open_lemma ~stack - (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate)); - stack - (* We interpret vernacular commands to a DSL that specifies their allowed actions on proof states *) -let rec translate_vernac ~atts v = let open Vernacextend in match v with +let translate_vernac ~atts v = let open Vernacextend in match v with | VernacAbortAll | VernacRestart | VernacUndo _ @@ -2355,6 +2221,9 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacBack _ | VernacAbort _ -> anomaly (str "type_vernac") + | VernacLoad _ -> + anomaly (str "Load is not supported recursively") + (* Syntax *) | VernacSyntaxExtension (infix, sl) -> VtDefault(fun () -> with_module_locality ~atts vernac_syntax_extension infix sl) @@ -2656,141 +2525,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacEndProof pe -> VtCloseProof (vernac_end_proof pe) - | VernacLoad (verbosely,fname) -> - VtNoProof(fun () -> - unsupported_attributes atts; - vernac_load ~verbosely fname) - (* Extensions *) | VernacExtend (opn,args) -> Vernacextend.type_vernac ~atts opn args - -(* "locality" is the prefix "Local" attribute, while the "local" component - * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility. - * loc is the Loc.t of the vernacular command being interpreted. *) -and interp_expr ~atts ~st c = - let stack = st.Vernacstate.lemmas in - vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); - match c with - - (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") - | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") - | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") - | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") - - (* Resetting *) - | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") - | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") - | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - - (* This one is possible to handle here *) - | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - - | v -> - let fv = translate_vernac ~atts v in - interp_typed_vernac ~stack fv - -(* XXX: This won't properly set the proof mode, as of today, it is - controlled by the STM. Thus, we would need access information from - the classifier. The proper fix is to move it to the STM, however, - the way the proof mode is set there makes the task non trivial - without a considerable amount of refactoring. -*) -and vernac_load ~verbosely fname = - let exception End_of_input in - - (* Note that no proof should be open here, so the state here is just token for now *) - let st = Vernacstate.freeze_interp_state ~marshallable:false in - let fname = - Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in - let fname = CUnix.make_suffix fname ".v" in - let input = - let longfname = Loadpath.locate_file fname in - let in_chan = open_utf8_file_in longfname in - Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in - (* Parsing loop *) - let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing - (fun po -> - match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with - | Some x -> x - | None -> raise End_of_input) in - let rec load_loop ~stack = - try - let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in - let stack = - v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) - (parse_sentence proof_mode input) in - load_loop ~stack - with - End_of_input -> - stack - in - let stack = load_loop ~stack:st.Vernacstate.lemmas in - (* If Load left a proof open, we fail too. *) - if Option.has_some stack then - CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); - () - -and interp_control ~st ({ v = cmd } as vernac) = - let time_header = mk_time_header vernac in - List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) - cmd.control - (fun ~st -> - let before_univs = Global.universes () in - let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in - if before_univs == Global.universes () then pstack - else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) - ~st - -(* Interpreting a possibly delayed proof *) -let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = - let stack = st.Vernacstate.lemmas in - let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in - let () = match pe with - | Admitted -> - save_lemma_admitted_delayed ~proof ~info - | Proved (_,idopt) -> - save_lemma_proved_delayed ~proof ~info ~idopt in - stack - -let interp_qed_delayed_control ~proof ~info ~st ~control { loc; v=pe } = - let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in - List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) - control - (fun ~st -> interp_qed_delayed ~proof ~info ~st pe) - ~st - -(* General interp with management of state *) -let () = - declare_int_option - { optdepr = false; - optname = "the default timeout"; - optkey = ["Default";"Timeout"]; - optread = (fun () -> !default_timeout); - optwrite = ((:=) default_timeout) } - -(* Be careful with the cache here in case of an exception. *) -let interp_gen ~verbosely ~st ~interp_fn cmd = - Vernacstate.unfreeze_interp_state st; - try vernac_timeout (fun st -> - let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let ontop = v_mod (interp_fn ~st) cmd in - Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; - Vernacstate.freeze_interp_state ~marshallable:false - ) st - with exn -> - let exn = CErrors.push exn in - let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in - Vernacstate.invalidate_cache (); - iraise exn - -(* Regular interp *) -let interp ?(verbosely=true) ~st cmd = - interp_gen ~verbosely ~st ~interp_fn:interp_control cmd - -let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t = - interp_gen ~verbosely:false ~st - ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index e65f9d3cfe..6368ebeed8 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,25 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** The main interpretation function of vernacular expressions *) -val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t - -(** Execute a Qed but with a proof_object which may contain a delayed - proof and won't be forced *) -val interp_qed_delayed_proof - : proof:Proof_global.proof_object - -> info:Lemmas.Info.t - -> st:Vernacstate.t - -> control:Vernacexpr.control_flag list - -> Vernacexpr.proof_end CAst.t - -> Vernacstate.t - -(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) -val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit - -(** Flag set when the test-suite is called. Its only effect to display - verbose information for [Fail] *) -val test_mode : bool ref +(** Vernac Translation into the Vernac DSL *) +val translate_vernac + : atts:Attributes.vernac_flags + -> Vernacexpr.vernac_expr + -> Vernacextend.typed_vernac (** Vernacular require command *) val vernac_require : @@ -38,8 +24,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr (** Miscellaneous stuff *) val command_focus : unit Proof.focus_kind - -(** Default proof mode set by `start_proof` *) -val get_default_proof_mode : unit -> Pvernac.proof_mode - -val proof_mode_opt_name : string list diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 2725516a76..e29086d726 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -54,7 +54,6 @@ and proof_block_name = string (** open type of delimiters *) type typed_vernac = | VtDefault of (unit -> unit) - | VtNoProof of (unit -> unit) | VtCloseProof of (lemma:Lemmas.t -> unit) | VtOpenProof of (unit -> Lemmas.t) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml new file mode 100644 index 0000000000..c14fc78462 --- /dev/null +++ b/vernac/vernacinterp.ml @@ -0,0 +1,278 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +open Vernacexpr + +(* XXX Should move to a common library *) +let debug = false +let vernac_pperr_endline pp = + if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () + +(* EJGA: We may remove this, only used twice below *) +let vernac_require_open_lemma ~stack f = + match stack with + | Some stack -> f stack + | None -> + CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress)") + +let interp_typed_vernac c ~stack = + let open Vernacextend in + match c with + | VtDefault f -> f (); stack + | VtNoProof f -> + if Option.has_some stack then + CErrors.user_err (Pp.str "Command not supported (Open proofs remain)"); + let () = f () in + stack + | VtCloseProof f -> + vernac_require_open_lemma ~stack (fun stack -> + let lemma, stack = Vernacstate.LemmaStack.pop stack in + f ~lemma; + stack) + | VtOpenProof f -> + Some (Vernacstate.LemmaStack.push stack (f ())) + | VtModifyProof f -> + Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack + | VtReadProofOpt f -> + let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in + f ~pstate; + stack + | VtReadProof f -> + vernac_require_open_lemma ~stack + (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate)); + stack + +(* Default proof mode, to be set at the beginning of proofs for + programs that cannot be statically classified. *) +let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) +let get_default_proof_mode () = !default_proof_mode + +let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode +let set_default_proof_mode_opt name = + default_proof_mode := + match Pvernac.lookup_proof_mode name with + | Some pm -> pm + | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) + +let proof_mode_opt_name = ["Default";"Proof";"Mode"] +let () = + Goptions.declare_string_option Goptions.{ + optdepr = false; + optname = "default proof mode" ; + optkey = proof_mode_opt_name; + optread = get_default_proof_mode_opt; + optwrite = set_default_proof_mode_opt; + } + +(** A global default timeout, controlled by option "Set Default Timeout n". + Use "Unset Default Timeout" to deactivate it (or set it to 0). *) + +let default_timeout = ref None + +(* Timeout *) +let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b = + match !default_timeout, timeout with + | _, Some n + | Some n, None -> + Control.timeout n f x CErrors.Timeout + | None, None -> + f x + +(* Fail *) +let test_mode = ref false + +(* Restoring the state is the caller's responsibility *) +let with_fail f : (Pp.t, unit) result = + try + let _ = f () in + Error () + with + (* Fail Timeout is a common pattern so we need to support it. *) + | e when CErrors.noncritical e || e = CErrors.Timeout -> + (* The error has to be printed in the failing state *) + Ok CErrors.(iprint (push e)) + +(* We restore the state always *) +let with_fail ~st f = + let res = with_fail f in + Vernacstate.invalidate_cache (); + Vernacstate.unfreeze_interp_state st; + match res with + | Error () -> + CErrors.user_err ~hdr:"Fail" (Pp.str "The command has not failed!") + | Ok msg -> + if not !Flags.quiet || !test_mode + then Feedback.msg_notice Pp.(str "The command has indeed failed with message:" ++ fnl () ++ msg) + +let locate_if_not_already ?loc (e, info) = + match Loc.get_loc info with + | None -> (e, Option.cata (Loc.add_loc info) info loc) + | Some l -> (e, info) + +let mk_time_header = + (* Drop the time header to print the command, we should indeed use a + different mechanism to `-time` commands than the current hack of + adding a time control to the AST. *) + let pr_time_header vernac = + let vernac = match vernac with + | { CAst.v = { control = ControlTime _ :: control; attrs; expr }; loc } -> + CAst.make ?loc { control; attrs; expr } + | _ -> vernac + in + Topfmt.pr_cmd_header vernac + in + fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) + +let interp_control_flag ~time_header (f : control_flag) ~st + (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = + match f with + | ControlFail -> + with_fail ~st (fun () -> fn ~st); + st.Vernacstate.lemmas + | ControlTimeout timeout -> + vernac_timeout ~timeout (fun () -> fn ~st) () + | ControlTime batch -> + let header = if batch then Lazy.force time_header else Pp.mt () in + System.with_time ~batch ~header (fun () -> fn ~st) () + | ControlRedirect s -> + Topfmt.with_output_to_file s (fun () -> fn ~st) () + +(* "locality" is the prefix "Local" attribute, while the "local" component + * is the outdated/deprecated "Local" attribute of some vernacular commands + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let rec interp_expr ~atts ~st c = + let stack = st.Vernacstate.lemmas in + vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); + match c with + + (* The STM should handle that, but LOAD bypasses the STM... *) + | VernacAbortAll -> CErrors.user_err (Pp.str "AbortAll cannot be used through the Load command") + | VernacRestart -> CErrors.user_err (Pp.str "Restart cannot be used through the Load command") + | VernacUndo _ -> CErrors.user_err (Pp.str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> CErrors.user_err (Pp.str "UndoTo cannot be used through the Load command") + + (* Resetting *) + | VernacResetName _ -> CErrors.anomaly (Pp.str "VernacResetName not handled by Stm.") + | VernacResetInitial -> CErrors.anomaly (Pp.str "VernacResetInitial not handled by Stm.") + | VernacBack _ -> CErrors.anomaly (Pp.str "VernacBack not handled by Stm.") + + (* This one is possible to handle here *) + | VernacAbort id -> CErrors.user_err (Pp.str "Abort cannot be used through the Load command") + | VernacLoad (verbosely, fname) -> + Attributes.unsupported_attributes atts; + vernac_load ~verbosely fname + | v -> + let fv = Vernacentries.translate_vernac ~atts v in + interp_typed_vernac ~stack fv + +and vernac_load ~verbosely fname = + let exception End_of_input in + + (* Note that no proof should be open here, so the state here is just token for now *) + let st = Vernacstate.freeze_interp_state ~marshallable:false in + let fname = + Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (Pp.str x)) fname in + let fname = CUnix.make_suffix fname ".v" in + let input = + let longfname = Loadpath.locate_file fname in + let in_chan = Util.open_utf8_file_in longfname in + Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in + (* Parsing loop *) + let v_mod = if verbosely then Flags.verbosely else Flags.silently in + let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing + (fun po -> + match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with + | Some x -> x + | None -> raise End_of_input) in + let rec load_loop ~stack = + try + let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in + let stack = + v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) + (parse_sentence proof_mode input) in + load_loop ~stack + with + End_of_input -> + stack + in + let stack = load_loop ~stack:st.Vernacstate.lemmas in + (* If Load left a proof open, we fail too. *) + if Option.has_some stack then + CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); + stack + +and interp_control ~st ({ CAst.v = cmd } as vernac) = + let time_header = mk_time_header vernac in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + cmd.control + (fun ~st -> + let before_univs = Global.universes () in + let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in + if before_univs == Global.universes () then pstack + else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) + ~st + +(* XXX: This won't properly set the proof mode, as of today, it is + controlled by the STM. Thus, we would need access information from + the classifier. The proper fix is to move it to the STM, however, + the way the proof mode is set there makes the task non trivial + without a considerable amount of refactoring. +*) + +(* Interpreting a possibly delayed proof *) +let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = + let stack = st.Vernacstate.lemmas in + let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in + let () = match pe with + | Admitted -> + Lemmas.save_lemma_admitted_delayed ~proof ~info + | Proved (_,idopt) -> + Lemmas.save_lemma_proved_delayed ~proof ~info ~idopt in + stack + +let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } = + let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + control + (fun ~st -> interp_qed_delayed ~proof ~info ~st pe) + ~st + +(* General interp with management of state *) +let () = let open Goptions in + declare_int_option + { optdepr = false; + optname = "the default timeout"; + optkey = ["Default";"Timeout"]; + optread = (fun () -> !default_timeout); + optwrite = ((:=) default_timeout) } + +(* Be careful with the cache here in case of an exception. *) +let interp_gen ~verbosely ~st ~interp_fn cmd = + Vernacstate.unfreeze_interp_state st; + try vernac_timeout (fun st -> + let v_mod = if verbosely then Flags.verbosely else Flags.silently in + let ontop = v_mod (interp_fn ~st) cmd in + Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; + Vernacstate.freeze_interp_state ~marshallable:false + ) st + with exn -> + let exn = CErrors.push exn in + let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in + Vernacstate.invalidate_cache (); + Util.iraise exn + +(* Regular interp *) +let interp ?(verbosely=true) ~st cmd = + interp_gen ~verbosely ~st ~interp_fn:interp_control cmd + +let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t = + interp_gen ~verbosely:false ~st + ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli new file mode 100644 index 0000000000..16849686da --- /dev/null +++ b/vernac/vernacinterp.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** The main interpretation function of vernacular expressions *) +val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t + +(** Execute a Qed but with a proof_object which may contain a delayed + proof and won't be forced *) +val interp_qed_delayed_proof + : proof:Proof_global.proof_object + -> info:Lemmas.Info.t + -> st:Vernacstate.t + -> control:Vernacexpr.control_flag list + -> Vernacexpr.proof_end CAst.t + -> Vernacstate.t + +(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) +val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit + +(** Flag set when the test-suite is called. Its only effect to display + verbose information for [Fail] *) +val test_mode : bool ref + +(** Default proof mode set by `start_proof` *) +val get_default_proof_mode : unit -> Pvernac.proof_mode +val proof_mode_opt_name : string list |