aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--INSTALL.md10
-rw-r--r--dev/ci/user-overlays/README.md26
-rw-r--r--lib/envars.ml34
-rw-r--r--pretyping/recordops.ml19
-rw-r--r--pretyping/recordops.mli2
-rw-r--r--pretyping/reductionops.ml8
-rw-r--r--pretyping/reductionops.mli35
-rw-r--r--pretyping/unification.ml16
-rw-r--r--test-suite/dune6
-rwxr-xr-xtest-suite/misc/coq_environment.sh51
-rw-r--r--test-suite/ocaml_pwd.ml27
-rw-r--r--tools/coq_makefile.ml2
12 files changed, 168 insertions, 68 deletions
diff --git a/INSTALL.md b/INSTALL.md
index f672bb45d3..74f4091134 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -99,3 +99,13 @@ dependencies...) as Coq. Distribution of pre-compiled plugins and
Coq version compiled with the same OCaml toolchain. An OCaml setup
mismatch is the most probable cause for an `Error while loading ...:
implementation mismatch on ...`.
+
+coq_environment.txt
+-------------------
+Coq binaries which honor environment variables, such as `COQLIB`, can
+be seeded values for these variables by placing a text file named
+`coq_environment.txt` next to them. The file can contain assignments
+like `COQLIB="some path"`, that is a variable name followed by `=` and
+a string that follows OCaml's escaping conventions. This feature can be
+used by installers of binary package to make Coq aware of its installation
+path.
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 14ee5e4199..cf1d71c1cd 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -5,27 +5,29 @@ have prepared a branch with the fix, you can add an "overlay" to your pull
request to test it with the adapted version of the external project.
An overlay is a file which defines where to look for the patched
-version so that testing is possible. This is done by calling the
-`overlay` command for each project with the project name (as used in
-the variables in [`ci-basic-overlay.sh`](../ci-basic-overlay.sh)), the
-location of your fork and the branch containing the patch on your
-fork.
-
-Moreover, the file contains very simple logic to test the pull request number
-or branch name and apply it only in this case.
-
+version so that testing is possible.
The name of your overlay file should start with a five-digit pull request
number, followed by a dash, anything (for instance your GitHub nickname
and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
-Example: `13128-SkySkimmer-noinstance.sh` containing
+This file must contain one or more invocation of the `overlay` function:
+```
+overlay <project> <giturl> <ref> <prnumber> [<prbranch>]
+```
+Each call creates an overlay for `project` using a given `giturl` and
+`ref` which is active for `prnumber` or `prbranch` (`prbranch` defaults
+to `ref`).
+Example of an overlay for the project `elpi` that uses the branch `noinstance`
+from the fork of `SkySkimmer` and is active for pull request `13128`
```
overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128
```
-See [`ci-common.sh`](../ci-common.sh) for the detailed documentation of
-the `overlay` function.
+Such a file can be created automatically using the scripts
+[`create_overlays.sh`](../../dev/tools/create_overlays.sh).
+See also the list of projects for which one can write an overlay in
+the file [`ci-basic-overlay.sh`](../ci-basic-overlay.sh).
### Branching conventions
diff --git a/lib/envars.ml b/lib/envars.ml
index 585d5185b4..1702b5d7a2 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -12,7 +12,37 @@ open Util
(** {1 Helper functions} *)
-let getenv_else s dft = try Sys.getenv s with Not_found -> dft ()
+let parse_env_line l =
+ try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
+ with _ -> None
+
+let with_ic file f =
+ let ic = open_in file in
+ try
+ let rc = f ic in
+ close_in ic;
+ rc
+ with e -> close_in ic; raise e
+
+let getenv_from_file name =
+ let base = Filename.dirname Sys.executable_name in
+ try
+ with_ic (base ^ "/coq_environment.txt") (fun ic ->
+ let rec find () =
+ let l = input_line ic in
+ match parse_env_line l with
+ | Some(n,v) when n = name -> v
+ | _ -> find ()
+ in
+ find ())
+ with
+ | Sys_error s -> raise Not_found
+ | End_of_file -> raise Not_found
+
+let system_getenv name =
+ try Sys.getenv name with Not_found -> getenv_from_file name
+
+let getenv_else s dft = try system_getenv s with Not_found -> dft ()
let safe_getenv warning n =
getenv_else n (fun () ->
@@ -145,7 +175,7 @@ let coqpath =
(** {2 Caml paths} *)
-let ocamlfind () = Coq_config.ocamlfind
+let ocamlfind () = getenv_else "OCAMLFIND" (fun () -> Coq_config.ocamlfind)
(** {1 XDG utilities} *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b6e44265ae..aa862a912e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -323,23 +323,32 @@ let check_and_decompose_canonical_structure env sigma ref =
let lookup_canonical_conversion env (proj,pat) =
assoc_pat env pat (GlobRef.Map.find proj !object_table)
-let decompose_projection sigma c args =
+let rec get_nth n = function
+| [] -> raise Not_found
+| arg :: args ->
+ let len = Array.length arg in
+ if n < len then arg.(n)
+ else get_nth (n - len) args
+
+let rec decompose_projection sigma c args =
match EConstr.kind sigma c with
+ | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args
+ | Cast (c, _, _) -> decompose_projection sigma c args
+ | App (c, arg) -> decompose_projection sigma c (arg :: args)
| Const (c, u) ->
let n = find_projection_nparams (GlobRef.ConstRef c) in
(* Check if there is some canonical projection attached to this structure *)
let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
- let arg = Stack.nth args n in
- arg
+ get_nth n args
| Proj (p, c) ->
let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in
c
| _ -> raise Not_found
-let is_open_canonical_projection env sigma (c,args) =
+let is_open_canonical_projection env sigma c =
let open EConstr in
try
- let arg = decompose_projection sigma c args in
+ let arg = decompose_projection sigma c [] in
try
let arg = whd_all env sigma arg in
let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5b8dc8184a..83927085e9 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -94,7 +94,7 @@ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
cs -> unit
val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
val is_open_canonical_projection :
- Environ.env -> Evd.evar_map -> Reductionops.state -> bool
+ Environ.env -> Evd.evar_map -> EConstr.t -> bool
val canonical_projections : unit ->
((GlobRef.t * cs_pattern) * obj_typ) list
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3352bfce38..7a5d0897b5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -930,14 +930,6 @@ let stack_red_of_state_red f =
let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in
f
-(* Drops the Cst_stack *)
-let iterate_whd_gen flags env sigma s =
- let rec aux t =
- let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in
- let whd_sk = Stack.map aux sk in
- Stack.zip sigma (hd,whd_sk)
- in aux s
-
let red_of_state_red f env sigma x =
Stack.zip sigma (f env sigma (x,Stack.empty))
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d404a7e414..04dfc5ffe6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -106,8 +106,6 @@ end
(************************************************************************)
-type state = constr * constr Stack.t
-
type reduction_function = env -> evar_map -> constr -> constr
type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
@@ -115,11 +113,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
type stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
-type state_reduction_function =
- env -> evar_map -> state -> state
-
-val pr_state : env -> evar_map -> state -> Pp.t
-
(** {6 Reduction Function Operators } *)
val strong_with_flags :
@@ -127,12 +120,6 @@ val strong_with_flags :
(CClosure.RedFlags.reds -> reduction_function)
val strong : reduction_function -> reduction_function
-val whd_state_gen :
- CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state
-
-val iterate_whd_gen : CClosure.RedFlags.reds ->
- Environ.env -> Evd.evar_map -> constr -> constr
-
(** {6 Generic Optimized Reduction Function using Closures } *)
val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
@@ -166,24 +153,13 @@ val whd_all_stack : stack_reduction_function
val whd_allnolet_stack : stack_reduction_function
val whd_betalet_stack : stack_reduction_function
-val whd_nored_state : state_reduction_function
-val whd_beta_state : state_reduction_function
-val whd_betaiota_state : state_reduction_function
-val whd_betaiotazeta_state : state_reduction_function
-val whd_all_state : state_reduction_function
-val whd_allnolet_state : state_reduction_function
-val whd_betalet_state : state_reduction_function
-
(** {6 Head normal forms } *)
val whd_delta_stack : stack_reduction_function
-val whd_delta_state : state_reduction_function
val whd_delta : reduction_function
val whd_betadeltazeta_stack : stack_reduction_function
-val whd_betadeltazeta_state : state_reduction_function
val whd_betadeltazeta : reduction_function
val whd_zeta_stack : stack_reduction_function
-val whd_zeta_state : state_reduction_function
val whd_zeta : reduction_function
val shrink_eta : Environ.env -> constr -> constr
@@ -269,8 +245,17 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
(** {6 Heuristic for Conversion with Evar } *)
+type state = constr * constr Stack.t
+
+type state_reduction_function =
+ env -> evar_map -> state -> state
+
+val pr_state : env -> evar_map -> state -> Pp.t
+
+val whd_nored_state : state_reduction_function
+
val whd_betaiota_deltazeta_for_iota_state :
- TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
+ TransparentState.t -> state_reduction_function
(** {6 Meta-related reduction functions } *)
val meta_instance : env -> evar_map -> constr freelisted -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1c24578a1c..3d3010d1a4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1070,10 +1070,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
let f1 () =
if isApp_or_Proj sigma cM then
- let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in
- if is_open_canonical_projection curenv sigma f1l1 then
- let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in
- solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
+ if is_open_canonical_projection curenv sigma cM then
+ solve_canonical_projection curenvnb pb opt cM cN substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
@@ -1086,14 +1084,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
else
try f1 () with e when precatchable_exception e ->
if isApp_or_Proj sigma cN then
- let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in
- if is_open_canonical_projection curenv sigma f2l2 then
- let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in
- solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
+ if is_open_canonical_projection curenv sigma cN then
+ solve_canonical_projection curenvnb pb opt cN cM substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
- and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
+ and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) =
+ let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in
+ let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in
let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
diff --git a/test-suite/dune b/test-suite/dune
index 6ab2988331..1864153021 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -9,6 +9,10 @@
(action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))
(rule
+ (targets bin.inc)
+ (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
+
+(rule
(targets summary.log)
(deps
; File that should be promoted.
@@ -44,4 +48,4 @@
; %{bin:fake_ide}
(action
(progn
- (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
+ (bash "make -j %{env:NJOBS=2} BIN=%{read:bin.inc} COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh
new file mode 100755
index 0000000000..667d11f89e
--- /dev/null
+++ b/test-suite/misc/coq_environment.sh
@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+TMP=`mktemp -d`
+cd $TMP
+
+cat > coq_environment.txt <<EOT
+# we override COQLIB because we can
+COQLIB="$TMP/overridden" # bla bla
+OCAMLFIND="$TMP/overridden"
+FOOBAR="one more"
+EOT
+
+cp $BIN/coqc .
+cp $BIN/coq_makefile .
+mkdir -p overridden/tools/
+cp $COQLIB/tools/CoqMakefile.in overridden/tools/
+
+unset COQLIB
+N=`./coqc -config | grep COQLIB | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+ echo COQLIB not overridden by coq_environment
+ coqc -config
+ exit 1
+fi
+N=`./coqc -config | grep OCAMLFIND | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+ echo OCAMLFIND not overridden by coq_environment
+ coqc -config
+ exit 1
+fi
+./coq_makefile -o CoqMakefile -R . foo > /dev/null
+N=`grep COQMF_OCAMLFIND CoqMakefile.conf | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+ echo COQMF_OCAMLFIND not overridden by coq_environment
+ cat CoqMakefile.conf
+ exit 1
+fi
+
+export COQLIB="/overridden2"
+N=`./coqc -config | grep COQLIB | grep /overridden2 | wc -l`
+if [ $N -ne 1 ]; then
+ echo COQLIB not overridden by COQLIB when coq_environment present
+ coqc -config
+ exit 1
+fi
+
+rm -rf $TMP
+exit 0
diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml
index afa3deea3a..054a921b93 100644
--- a/test-suite/ocaml_pwd.ml
+++ b/test-suite/ocaml_pwd.ml
@@ -1,7 +1,26 @@
+open Arg
+
+let quoted = ref false
+let trailing_slash = ref false
+
+let arguments = [
+ "-quoted",Set quoted, "Quote path";
+ "-trailing-slash",Set trailing_slash, "End the path with a /";
+]
+let subject = ref None
+let set_subject x =
+ if !subject <> None then
+ failwith "only one path";
+ subject := Some x
+
let _ =
- let quoted = Sys.argv.(1) = "-quoted" in
- let ch_dir = Sys.argv.(if quoted then 2 else 1) in
- Sys.chdir ch_dir;
+ Arg.parse arguments set_subject "Usage:";
+ let subject =
+ match !subject with
+ | None -> failwith "no path given";
+ | Some x -> x in
+ Sys.chdir subject;
let dir = Sys.getcwd () in
- let dir = if quoted then Filename.quote dir else dir in
+ let dir = if !trailing_slash then dir ^ "/" else dir in
+ let dir = if !quoted then Filename.quote dir else dir in
Format.printf "%s%!" dir
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0cbfd46e80..07550b67e3 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -216,7 +216,7 @@ let generate_conf_coq_config oc =
section oc "Coq configuration.";
let src_dirs = Coq_config.all_src_dirs in
Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
- fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib)
+ fprintf oc "COQMF_WINDRIVE=%s\n" (windrive (Envars.coqlib()))
;;
let generate_conf_files oc
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 01:05:19 +0000