aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml7
-rw-r--r--dev/ci/README-developers.md7
-rw-r--r--engine/evd.ml6
-rw-r--r--engine/evd.mli1
-rw-r--r--engine/uState.ml2
-rw-r--r--engine/uState.mli2
-rw-r--r--test-suite/.csdp.cache.test-suite (renamed from test-suite/.csdp.cache)bin329899 -> 329899 bytes
-rw-r--r--test-suite/Makefile7
-rwxr-xr-xtest-suite/coq-makefile/template/init.sh22
-rw-r--r--vernac/auto_ind_decl.ml8
-rw-r--r--vernac/comDefinition.ml2
-rw-r--r--vernac/declare.ml31
-rw-r--r--vernac/declare.mli6
-rw-r--r--vernac/obligations.ml7
14 files changed, 56 insertions, 52 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b728f94159..fe8370e849 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -366,12 +366,11 @@ pkg:opam:
dependencies: []
script:
- set -e
- - opam pin add --kind=path coq.$COQ_VERSION .
- - opam pin add --kind=path coqide-server.$COQ_VERSION .
- - opam pin add --kind=path coqide.$COQ_VERSION .
+ - opam pin add --kind=path coq.dev .
+ - opam pin add --kind=path coqide-server.dev .
+ - opam pin add --kind=path coqide.dev .
- set +e
variables:
- COQ_VERSION: "8.13"
OPAM_SWITCH: "edge"
OPAM_VARIANT: "+flambda"
only: *full-ci
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index d5c6096100..801e29ac95 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -179,6 +179,11 @@ but if you wish to save more time you can skip the job by setting
This means you will need to change its value when the Docker image
needs to be updated. You can do so for a single pipeline by starting
-it through the web interface.
+it through the web interface. Here is a direct link that you can use
+to trigger such a build:
+`https://gitlab.com/coq/coq/pipelines/new?var[SKIP_DOCKER]=false&ref=pr-XXXXX`.
+Note that this link will give a 404 error if you are not logged in or
+a member of the Coq organization on GitLab. To request to join the
+Coq organization, go to https://gitlab.com/coq to request access.
See also [`docker/README.md`](docker/README.md).
diff --git a/engine/evd.ml b/engine/evd.ml
index 5642145f6d..ff13676818 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -697,8 +697,7 @@ let empty = {
extras = Store.empty;
}
-let from_env e =
- { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) }
+let from_env e = { empty with universes = UState.from_env e }
let from_ctx ctx = { empty with universes = ctx }
@@ -862,9 +861,6 @@ let universe_subst evd =
let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
{evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'}
-let merge_universe_subst evd subst =
- {evd with universes = UState.merge_subst evd.universes subst }
-
let with_context_set ?loc rigid d (a, ctx) =
(merge_context_set ?loc rigid d ctx, a)
diff --git a/engine/evd.mli b/engine/evd.mli
index c6c4a71b22..d9b7bd76e7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -636,7 +636,6 @@ val merge_universe_context : evar_map -> UState.t -> evar_map
val set_universe_context : evar_map -> UState.t -> evar_map
val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
-val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map
val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
diff --git a/engine/uState.ml b/engine/uState.ml
index 99ac5f2ce8..7c60d8317c 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -63,6 +63,8 @@ let make ~lbound u =
uctx_universes_lbound = lbound;
uctx_initial_universes = u}
+let from_env e = make ~lbound:(Environ.universes_lbound e) (Environ.universes e)
+
let is_empty ctx =
ContextSet.is_empty ctx.uctx_local &&
LMap.is_empty ctx.uctx_univ_variables
diff --git a/engine/uState.mli b/engine/uState.mli
index 533a501b59..45a0f9964e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -29,6 +29,8 @@ val make : lbound:UGraph.Bound.t -> UGraph.t -> t
val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
+val from_env : Environ.env -> t
+
val is_empty : t -> bool
val union : t -> t -> t
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache.test-suite
index 046cb067c5..046cb067c5 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache.test-suite
Binary files differ
diff --git a/test-suite/Makefile b/test-suite/Makefile
index f0f838680e..5dd4f42af3 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -117,7 +117,11 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
# All subsystems
SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
-PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v))
+.csdp.cache: .csdp.cache.test-suite
+ cp $< $@
+ chmod u+w $@
+
+PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v)) .csdp.cache
#######################################################################
# Phony targets
@@ -470,6 +474,7 @@ approve-output: output output-coqtop
output/MExtraction.out: ../plugins/micromega/micromega.ml
$(SHOW) GEN $@
$(HIDE) cp $< $@
+ $(HIDE) chmod u+w $@
$(HIDE) echo >> $@
$(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index 30be5e6456..ab89e12592 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -9,10 +9,18 @@ cd _test || exit 1
mkdir -p src
mkdir -p theories/sub
-cp ../../template/theories/sub/testsub.v theories/sub
-cp ../../template/theories/test.v theories
-cp ../../template/src/test.mlg src
-cp ../../template/src/test_aux.mli src
-cp ../../template/src/test.mli src
-cp ../../template/src/test_plugin.mlpack src
-cp ../../template/src/test_aux.ml src
+cp_file() {
+ local _TARGET=$1
+ cp ../../template/$_TARGET $_TARGET
+ chmod u+w $_TARGET
+}
+
+# We chmod +w as to fix the case where the sources are read-only, as
+# for example when using Dune's cache.
+cp_file theories/sub/testsub.v
+cp_file theories/test.v
+cp_file src/test.mlg
+cp_file src/test_aux.mli
+cp_file src/test.mli
+cp_file src/test_plugin.mlpack
+cp_file src/test_aux.ml
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5323c9f1c6..bb640a83f6 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -385,7 +385,7 @@ let build_beq_scheme mode kn =
Vars.substl subst cores.(i)
in
create_input fix),
- UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()))
+ UState.from_env (Global.env ()))
let beq_scheme_kind =
declare_mutual_scheme_object "_beq"
@@ -707,7 +707,7 @@ let make_bl_scheme mode mind =
let lnonparrec,lnamesparrec = (* TODO subst *)
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let bl_goal = compute_bl_goal ind lnamesparrec nparrec in
- let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+ let uctx = UState.from_env (Global.env ()) in
let side_eff = side_effect_of_mode mode in
let bl_goal = EConstr.of_constr bl_goal in
let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
@@ -840,7 +840,7 @@ let make_lb_scheme mode mind =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let lb_goal = compute_lb_goal ind lnamesparrec nparrec in
- let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+ let uctx = UState.from_env (Global.env ()) in
let side_eff = side_effect_of_mode mode in
let lb_goal = EConstr.of_constr lb_goal in
let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
@@ -1010,7 +1010,7 @@ let make_eq_decidability mode mind =
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
let u = Univ.Instance.empty in
- let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+ let uctx = UState.from_env (Global.env ()) in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let side_eff = side_effect_of_mode mode in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index eac8f92e2e..d56917271c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
let (body, types), evd, udecl, impargs =
interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
in
- let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
+ let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in
let _ : Declare.Obls.progress =
Obligations.add_definition
~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c291890dce..333b186b22 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1007,25 +1007,20 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
-let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
+let prepare_obligation ~name ~types ~body sigma =
+ let env = Global.env () in
+ let types = match types with
+ | Some t -> t
+ | None -> Retyping.get_type_of env sigma body
+ in
let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
- sigma (fun nf -> nf body, Option.map nf types)
+ sigma (fun nf -> nf body, nf types)
in
- let univs = Evd.check_univ_decl ~poly sigma udecl in
- let ce = definition_entry ?opaque ?inline ?types ~univs body in
- let env = Global.env () in
- let (c,ctx), sideff = Future.force ce.proof_entry_body in
- assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private);
- assert(Univ.ContextSet.is_empty ctx);
RetrieveObl.check_evars env sigma;
- let c = EConstr.of_constr c in
- let typ = match ce.proof_entry_type with
- | Some t -> EConstr.of_constr t
- | None -> Retyping.get_type_of env sigma c
- in
- let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
+ let body, types = EConstr.(of_constr body, of_constr types) in
+ let obls, _, body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in
let uctx = Evd.evar_universe_context sigma in
- c, cty, uctx, obls
+ body, cty, uctx, obls
let prepare_parameter ~poly ~udecl ~types sigma =
let env = Global.env () in
@@ -1641,7 +1636,7 @@ let obligation_terminator entries uctx {name; num; auto} =
universes and constraints if any *)
defined
then
- UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
+ UState.from_env (Global.env ())
else uctx
in
update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
@@ -1673,9 +1668,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
if not prg.prg_poly (* Not polymorphic *) then
(* The universe context was declared globally, we continue
from the new global environment. *)
- let ctx =
- UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
- in
+ let ctx = UState.from_env (Global.env ()) in
let ctx' = UState.merge_subst ctx (UState.subst ctx') in
(Univ.Instance.empty, ctx')
else
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 82b0cff8d9..62bc6a34bf 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -367,11 +367,7 @@ val declare_mutually_recursive
(** Prepare API, to be removed once we provide the corresponding 1-step API *)
val prepare_obligation
- : ?opaque:bool
- -> ?inline:bool
- -> name:Id.t
- -> poly:bool
- -> udecl:UState.universe_decl
+ : name:Id.t
-> types:EConstr.t option
-> body:EConstr.t
-> Evd.evar_map
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5fdee9f2d4..bbc20d5e30 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -191,10 +191,9 @@ and solve_obligation_by_tac prg obls i tac =
obls.(i) <- obl';
if def && not prg.prg_poly then (
(* Declare the term constraints with the first obligation only *)
- let evd = Evd.from_env (Global.env ()) in
- let evd = Evd.merge_universe_subst evd (UState.subst ctx) in
- let ctx' = Evd.evar_universe_context evd in
- Some (ProgramDecl.set_uctx ~uctx:ctx' prg))
+ let uctx = UState.from_env (Global.env ()) in
+ let uctx = UState.merge_subst uctx (UState.subst ctx) in
+ Some (ProgramDecl.set_uctx ~uctx prg))
else Some prg
else None
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 21:01:53 +0000