aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml19
-rw-r--r--Makefile.ci1
-rw-r--r--Makefile.ide8
-rw-r--r--azure-pipelines.yml4
-rwxr-xr-xdev/ci/ci-basic-overlay.sh7
-rwxr-xr-xdev/ci/ci-perennial.sh12
-rw-r--r--dev/doc/release-process.md6
-rw-r--r--kernel/cooking.ml8
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/entries.ml8
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/section.ml24
-rw-r--r--kernel/term_typing.ml28
-rw-r--r--tactics/declare.ml4
-rw-r--r--tactics/declare.mli2
-rw-r--r--tactics/proof_global.ml4
-rw-r--r--tactics/proof_global.mli2
-rw-r--r--vernac/lemmas.ml2
18 files changed, 80 insertions, 65 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e527986ef7..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:
@@ -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/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/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 ea268f9d4e..1c486b024d 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -99,6 +99,11 @@ in time.
## 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
@@ -139,6 +144,7 @@ in time.
## 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/kernel/cooking.ml b/kernel/cooking.ml
index 0951b07d49..b88a2e6194 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,7 +161,7 @@ type 'opaque result = {
cook_universes : universes;
cook_relevance : Sorts.relevance;
cook_inline : inline;
- cook_context : Constr.named_context option;
+ cook_context : Id.Set.t option;
}
let expmod_constr_subst cache modlist subst c =
@@ -242,11 +242,7 @@ let cook_constant { from = cb; info } =
OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
| Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
in
- let const_hyps =
- Context.Named.fold_outside (fun decl hyps ->
- List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
- hyps)
- hyps0 ~init:cb.const_hyps in
+ let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in
let typ = abstract_constant_type (expmod cb.const_type) hyps in
{
cook_body = body;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 671cdf51fe..83a8b9edfc 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -23,7 +23,7 @@ type 'opaque result = {
cook_universes : universes;
cook_relevance : Sorts.relevance;
cook_inline : inline;
- cook_context : Constr.named_context option;
+ cook_context : Names.Id.Set.t option;
}
val cook_constant : recipe -> Opaqueproof.opaque result
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 47e2f72b0e..1e6bc14935 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -61,7 +61,7 @@ type mutual_inductive_entry = {
type definition_entry = {
const_entry_body : constr;
(* List of section variables *)
- const_entry_secctx : Constr.named_context option;
+ const_entry_secctx : Id.Set.t option;
(* State id on which the completion of type checking is reported *)
const_entry_feedback : Stateid.t option;
const_entry_type : types option;
@@ -70,7 +70,7 @@ type definition_entry = {
type section_def_entry = {
secdef_body : constr;
- secdef_secctx : Constr.named_context option;
+ secdef_secctx : Id.Set.t option;
secdef_feedback : Stateid.t option;
secdef_type : types option;
}
@@ -78,7 +78,7 @@ type section_def_entry = {
type 'a opaque_entry = {
opaque_entry_body : 'a;
(* List of section variables *)
- opaque_entry_secctx : Constr.named_context;
+ opaque_entry_secctx : Id.Set.t;
(* State id on which the completion of type checking is reported *)
opaque_entry_feedback : Stateid.t option;
opaque_entry_type : types;
@@ -88,7 +88,7 @@ type 'a opaque_entry = {
type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
- Constr.named_context option * types in_universes_entry * inline
+ Id.Set.t option * types in_universes_entry * inline
type primitive_entry = {
prim_entry_type : types option;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4268f0a602..1069d9a62c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -733,7 +733,7 @@ let constant_entry_of_side_effect eff =
if Declareops.is_opaque cb then
OpaqueEff {
opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
- opaque_entry_secctx = cb.const_hyps;
+ opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
opaque_entry_feedback = None;
opaque_entry_type = cb.const_type;
opaque_entry_universes = univs;
@@ -741,7 +741,7 @@ let constant_entry_of_side_effect eff =
else
DefinitionEff {
const_entry_body = p;
- const_entry_secctx = Some cb.const_hyps;
+ const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps);
const_entry_feedback = None;
const_entry_type = Some cb.const_type;
const_entry_universes = univs;
diff --git a/kernel/section.ml b/kernel/section.ml
index 4a9b222798..babd9fe7a1 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -146,19 +146,11 @@ let empty_segment = {
abstr_uctx = AUContext.empty;
}
-let extract_hyps sec vars hyps =
- (* FIXME: this code is fishy. It is supposed to check that declared section
- variables are an ordered subset of the ambient ones, but it doesn't check
- e.g. uniqueness of naming nor convertibility of the section data. *)
- let rec aux ids hyps = match ids, hyps with
- | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) ->
- decl :: aux ids hyps
- | _ :: ids, hyps ->
- aux ids hyps
- | [], _ -> []
- in
- let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in
- aux ids hyps
+let extract_hyps sec vars used =
+ (* Keep the section-local segment of variables *)
+ let vars = List.firstn sec.sec_context vars in
+ (* Only keep the part that is used by the declaration *)
+ List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars
let section_segment_of_entry vars e hyps sections =
(* [vars] are the named hypotheses, [hyps] the subset that is declared by the
@@ -180,12 +172,14 @@ let section_segment_of_entry vars e hyps sections =
let segment_of_constant env con s =
let body = Environ.lookup_constant con env in
let vars = Environ.named_context env in
- section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s
+ let used = Context.Named.to_vars body.Declarations.const_hyps in
+ section_segment_of_entry vars (SecDefinition con) used s
let segment_of_inductive env mind s =
let mib = Environ.lookup_mind mind env in
let vars = Environ.named_context env in
- section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s
+ let used = Context.Named.to_vars mib.Declarations.mind_hyps in
+ section_segment_of_entry vars (SecInductive mind) used s
let instance_from_variable_context =
List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b65e62ba30..f70b2960cf 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -221,9 +221,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let build_constant_declaration env result =
let open Cooking in
let typ = result.cook_type in
- let check declared inferred =
- let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
- let inferred_set, declared_set = mk_set inferred, mk_set declared in
+ let check declared_set inferred_set =
if not (Id.Set.subset inferred_set declared_set) then
let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
let n = List.length l in
@@ -239,11 +237,6 @@ let build_constant_declaration env result =
str "Proof using " ++ declared_vars ++ fnl () ++
str "to" ++ fnl () ++
str "Proof using " ++ inferred_vars) in
- let sort l =
- List.filter (fun decl ->
- let id = NamedDecl.get_id decl in
- List.exists (NamedDecl.get_id %> Names.Id.equal id) l)
- (named_context env) in
(* We try to postpone the computation of used section variables *)
let hyps, def =
let context_ids = List.map NamedDecl.get_id (named_context env) in
@@ -252,7 +245,7 @@ let build_constant_declaration env result =
| None ->
if List.is_empty context_ids then
(* Empty section context: no need to check *)
- [], def
+ Id.Set.empty, def
else
(* No declared section vars, and non-empty section context:
we must look at the body NOW, if any *)
@@ -264,16 +257,19 @@ let build_constant_declaration env result =
(* Opaque definitions always come with their section variables *)
assert false
in
- keep_hyps env (Id.Set.union ids_typ ids_def), def
+ Environ.really_needed env (Id.Set.union ids_typ ids_def), def
| Some declared ->
+ let needed = Environ.really_needed env declared in
+ (* Transitive closure ensured by the upper layers *)
+ let () = assert (Id.Set.equal needed declared) in
(* We use the declared set and chain a check of correctness *)
- sort declared,
+ declared,
match def with
| Undef _ | Primitive _ as x -> x (* nothing to check *)
| Def cs as x ->
let ids_typ = global_vars_set env typ in
let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
- let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+ let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
check declared inferred;
x
| OpaqueDef lc -> (* In this case we can postpone the check *)
@@ -281,12 +277,13 @@ let build_constant_declaration env result =
let kont c =
let ids_typ = global_vars_set env typ in
let ids_def = global_vars_set env c in
- let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+ let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
check declared inferred
in
OpaqueDef (iter kont lc)
in
let univs = result.cook_universes in
+ let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
let tps =
let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
Option.map Cemitcodes.from_val res
@@ -317,7 +314,10 @@ let translate_recipe env _kn r =
let univs = result.cook_universes in
let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
let tps = Option.map Cemitcodes.from_val res in
- { const_hyps = Option.get result.cook_context;
+ let hyps = Option.get result.cook_context in
+ (* Trust the set of section hypotheses generated by Cooking *)
+ let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
+ { const_hyps = hyps;
const_body = result.cook_body;
const_type = result.cook_type;
const_body_code = tps;
diff --git a/tactics/declare.ml b/tactics/declare.ml
index e418240d3a..b6a0d9f39a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -72,7 +72,7 @@ type constant_obj = {
type 'a proof_entry = {
proof_entry_body : 'a Entries.const_entry_body;
(* List of section variables *)
- proof_entry_secctx : Constr.named_context option;
+ proof_entry_secctx : Id.Set.t option;
(* State id on which the completion of type checking is reported *)
proof_entry_feedback : Stateid.t option;
proof_entry_type : Constr.types option;
@@ -228,7 +228,7 @@ let cast_opaque_proof_entry e =
ids_typ, vars
in
let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
- keep_hyps env (Id.Set.union hyp_typ hyp_def)
+ Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
| Some hyps -> hyps
in
{
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 4cb876cecb..da66a2713c 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -23,7 +23,7 @@ open Entries
type 'a proof_entry = {
proof_entry_body : 'a Entries.const_entry_body;
(* List of section variables *)
- proof_entry_secctx : Constr.named_context option;
+ proof_entry_secctx : Id.Set.t option;
(* State id on which the completion of type checking is reported *)
proof_entry_feedback : Stateid.t option;
proof_entry_type : Constr.types option;
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index a2929e45cd..b723922642 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -36,7 +36,7 @@ type opacity_flag = Opaque | Transparent
type t =
{ endline_tactic : Genarg.glob_generic_argument option
- ; section_vars : Constr.named_context option
+ ; section_vars : Id.Set.t option
; proof : Proof.t
; udecl: UState.universe_decl
(** Initial universe declarations *)
@@ -128,7 +128,7 @@ let set_used_variables ps l =
if not (Option.is_empty ps.section_vars) then
CErrors.user_err Pp.(str "Used section variables can be declared only once");
(* EJGA: This is always empty thus we should modify the type *)
- (ctx, []), { ps with section_vars = Some ctx}
+ (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) }
let get_open_goals ps =
let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index d15e23c2cc..b9d1b37a11 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -17,7 +17,7 @@ type t
(* Should be moved into a proper view *)
val get_proof : t -> Proof.t
val get_proof_name : t -> Names.Id.t
-val get_used_variables : t -> Constr.named_context option
+val get_used_variables : t -> Names.Id.Set.t option
(** Get the universe declaration associated to the current proof. *)
val get_universe_decl : t -> UState.universe_decl
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42d1a1f3fc..c7a588d2b4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -359,7 +359,7 @@ let save_lemma_admitted ~(lemma : t) : unit =
let env = Global.env () in
let ids_typ = Environ.global_vars_set env typ in
let ids_def = Environ.global_vars_set env pproof in
- Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
+ Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
| _ -> None in
let universes = Proof_global.get_initial_euctx lemma.proof in
let ctx = UState.check_univ_decl ~poly universes udecl in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:24:47 +0000