diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | checker/checker.ml | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 6 | ||||
| -rw-r--r-- | lib/envars.ml | 6 | ||||
| -rw-r--r-- | lib/envars.mli | 3 | ||||
| -rw-r--r-- | tools/coqdep.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 3 |
7 files changed, 25 insertions, 3 deletions
@@ -18,6 +18,9 @@ Changes from V8.3 to V8.4 - Vm_compute can now be interrupted via Ctrl-C. +- Coq now searches directories specified in COQPATH and user-contribs before + the standard library. + Tactics - New tactics constr_eq, is_evar and has_evar. diff --git a/checker/checker.ml b/checker/checker.ml index c2c21fbe2..0c9d7e2dc 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -102,6 +102,7 @@ let set_rec_include d p = let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in + let coqpath = Envars.coqpath () in let plugins = coqlib/"plugins" in (* NOTE: These directories are searched from last to first *) (* first standard library *) @@ -111,6 +112,8 @@ let init_load_path () = (* then user-contrib *) if Sys.file_exists user_contrib then add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; + (* then directories in COQPATH *) + List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 22417d60e..5af57aefc 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -70,9 +70,11 @@ option \verb:-q:. \section[Environment variables]{Environment variables\label{EnvVariables} \index{Environment variables}} -There are three environment variables used by the \Coq\ system. +There are four environment variables used by the \Coq\ system. \verb:$COQBIN: for the directory where the binaries are, -\verb:$COQLIB: for the directory where the standard library is, and +\verb:$COQLIB: for the directory where the standard library is, +\verb:$COQPATH: for a list of directories seperated by \verb|:| +(\verb|;| on windows) to add to the load path, and \verb:$COQTOP: for the directory of the sources. The latter is useful only for developers that are writing their own tactics and are using \texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or diff --git a/lib/envars.ml b/lib/envars.ml index efb2d3fa4..a05029c95 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -35,6 +35,12 @@ let path_to_list p = let sep = if Sys.os_type = "Win32" then ';' else ':' in Util.split_string_at sep p +let coqpath () = + try + let path = Sys.getenv "COQPATH" in + List.rev (path_to_list path) + with _ -> [] + let rec which l f = match l with | [] -> raise Not_found diff --git a/lib/envars.mli b/lib/envars.mli index e48f3ea00..6d053be6d 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -11,6 +11,9 @@ val coqlib : unit -> string val coqbin : unit -> string +(* coqpath is stored in reverse order, since that is the order it + * gets added to the searc path *) +val coqpath : unit -> string list val camlbin : unit -> string val camlp4bin : unit -> string diff --git a/tools/coqdep.ml b/tools/coqdep.ml index ccce7cd31..a683aaae9 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -199,7 +199,9 @@ let coqdep () = add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in - if Sys.file_exists user then add_rec_dir add_coqlib_known user [] + if Sys.file_exists user then add_rec_dir add_coqlib_known user []; + let coqpath = Envars.coqpath () in + List.iter (fun s -> add_rec_dir add_coqlib_known s []) coqpath; end; List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index d7031297d..977b8f4c7 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -91,6 +91,7 @@ let theories_dirs_map = [ let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in + let coqpath = Envars.coqpath () in let dirs = ["states";"plugins"] in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) @@ -104,6 +105,8 @@ let init_load_path () = (* then user-contrib *) if Sys.file_exists user_contrib then Mltop.add_rec_path ~unix_path:user_contrib ~coq_root:Nameops.default_root_prefix; + (* then directories in COQPATH *) + List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) coqpath; (* then current directory *) Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix; (* additional loadpath, given with -I -include -R options *) |