diff options
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 63 |
1 files changed, 36 insertions, 27 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 210507e1..e4cfcb3f 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqinit.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open System open Toplevel @@ -17,13 +15,13 @@ let (/) = Filename.concat let set_debug () = Flags.debug := true (* Loading of the ressource file. - rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one + rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one does not exist. *) -let rcfile = ref (home/".coqrc") +let rcdefaultname = "coqrc" +let rcfile = ref "" let rcfile_specified = ref false let set_rcfile s = rcfile := s; rcfile_specified := true -let set_rcuser s = rcfile := ("~"^s)/".coqrc" let load_rc = ref true let no_load_rc () = load_rc := false @@ -35,14 +33,17 @@ let load_rcfile() = if file_readable_p !rcfile then Vernac.load_vernac false !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) - else if file_readable_p (!rcfile^"."^Coq_config.version) then - Vernac.load_vernac false (!rcfile^"."^Coq_config.version) - else if file_readable_p !rcfile then - Vernac.load_vernac false !rcfile - else () + else try let inferedrc = List.find file_readable_p [ + Envars.xdg_config_home/rcdefaultname^"."^Coq_config.version; + Envars.xdg_config_home/rcdefaultname; + System.home/"."^rcdefaultname^"."^Coq_config.version; + System.home/"."^rcdefaultname; + ] in + Vernac.load_vernac false inferedrc + with Not_found -> () (* Flags.if_verbose - mSGNL (str ("No .coqrc or .coqrc."^Coq_config.version^ + mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ " found. Skipping rcfile loading.")) *) with e -> @@ -52,9 +53,9 @@ let load_rcfile() = Flags.if_verbose msgnl (str"Skipping rcfile loading.") (* Puts dir in the path of ML and in the LoadPath *) -let coq_add_path d s = - Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s]) -let coq_add_rec_path s = Mltop.add_rec_path s (Names.make_dirpath [Nameops.coq_root]) +let coq_add_path unix_path s = + Mltop.add_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root;Names.id_of_string s]) +let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root]) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -75,10 +76,12 @@ let theories_dirs_map = [ "theories/Sets", "Sets" ; "theories/Structures", "Structures" ; "theories/Lists", "Lists" ; + "theories/Vectors", "Vectors" ; "theories/Wellfounded", "Wellfounded" ; "theories/Relations", "Relations" ; "theories/Numbers", "Numbers" ; "theories/QArith", "QArith" ; + "theories/PArith", "PArith" ; "theories/NArith", "NArith" ; "theories/ZArith", "ZArith" ; "theories/Arith", "Arith" ; @@ -91,24 +94,31 @@ let theories_dirs_map = [ let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in + let xdg_dirs = Envars.xdg_dirs in + let coqpath = Envars.coqpath in let dirs = ["states";"plugins"] in - (* first user-contrib *) - if Sys.file_exists user_contrib then - Mltop.add_rec_path user_contrib Nameops.default_root_prefix; - (* then states, theories and dev *) - List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; - (* developer specific directory to open *) + (* NOTE: These directories are searched from last to first *) + (* first, developer specific directory to open *) if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; (* then standard library *) List.iter - (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) + (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) theories_dirs_map; + (* then states and plugins *) + List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; + (* 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 XDG_DATA_DIRS and XDG_DATA_HOME *) + List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) xdg_dirs; + (* 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 "." Nameops.default_root_prefix; + Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (s,alias,reci) -> - if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias) + (fun (unix_path, coq_root, reci) -> + if reci then Mltop.add_rec_path ~unix_path ~coq_root else Mltop.add_path ~unix_path ~coq_root) (List.rev !includes) let init_library_roots () = @@ -117,9 +127,8 @@ let init_library_roots () = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = - let coqsrc = Coq_config.coqsrc in let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) + Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl) in Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir |