From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- toplevel/coqinit.ml | 135 ++++++++++++++++++++++++++-------------------------- 1 file changed, 68 insertions(+), 67 deletions(-) (limited to 'toplevel/coqinit.ml') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 0b83bbb8..03074ced 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -1,18 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* () (* Flags.if_verbose @@ -47,79 +51,74 @@ let load_rcfile() = " found. Skipping rcfile loading.")) *) with reraise -> - (msgnl (str"Load of rcfile failed."); - raise reraise) + let reraise = Errors.push reraise in + let () = msg_info (str"Load of rcfile failed.") in + iraise reraise else - Flags.if_verbose msgnl (str"Skipping rcfile loading.") + Flags.if_verbose msg_info (str"Skipping rcfile loading.") (* Puts dir in the path of ML and in the LoadPath *) 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]) + Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; + Mltop.add_ml_dir unix_path -(* By the option -include -I or -R of the command line *) -let includes = ref [] -let push_include (s, alias) = includes := (s,alias,false) :: !includes -let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes +(* Recursively puts dir in the LoadPath if -nois was not passed *) +let add_stdlib_path ~unix_path ~coq_root ~with_ml = + if !Flags.load_init then + Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true + else + Mltop.add_path ~unix_path ~coq_root ~implicit:false; + if with_ml then + Mltop.add_rec_ml_dir unix_path -(* The list of all theories in the standard library /!\ order does matter *) -let theories_dirs_map = [ - "theories/Unicode", "Unicode" ; - "theories/Classes", "Classes" ; - "theories/Program", "Program" ; - "theories/MSets", "MSets" ; - "theories/FSets", "FSets" ; - "theories/Reals", "Reals" ; - "theories/Strings", "Strings" ; - "theories/Sorting", "Sorting" ; - "theories/Setoids", "Setoids" ; - "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" ; - "theories/Bool", "Bool" ; - "theories/Logic", "Logic" ; - "theories/Init", "Init" - ] +let add_userlib_path ~unix_path = + Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; + Mltop.add_rec_ml_dir unix_path + +(* Options -I, -I-as, and -R of the command line *) +let includes = ref [] +let push_include s alias recursive implicit = + includes := (s,alias,recursive,implicit) :: !includes +let ml_includes = ref [] +let push_ml_include s = ml_includes := s :: !ml_includes (* Initializes the LoadPath *) let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in - let xdg_dirs = Envars.xdg_dirs in + let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in let coqpath = Envars.coqpath in - let dirs = ["states";"plugins"] in + let coq_root = Names.DirPath.make [Nameops.coq_root] in (* 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"; + (* main loops *) + if Coq_config.local || !Flags.boot then begin + let () = Mltop.add_ml_dir (coqlib/"stm") in + Mltop.add_ml_dir (coqlib/"ide") + end; + Mltop.add_ml_dir (coqlib/"toploop"); (* then standard library *) - List.iter - (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; + add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; + (* then plugins *) + add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; (* then user-contrib *) if Sys.file_exists user_contrib then - Mltop.add_rec_path ~unix_path:user_contrib ~coq_root:Nameops.default_root_prefix; + add_userlib_path ~unix_path:user_contrib; (* 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; + List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs; (* then directories in COQPATH *) - List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) coqpath; + List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; (* then current directory *) - Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix; - (* additional loadpath, given with -I -include -R options *) + Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false; + (* additional loadpath, given with options -I-as, -Q, and -R *) List.iter - (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) + (fun (unix_path, coq_root, reci, implicit) -> + (if reci then Mltop.add_rec_path else Mltop.add_path) + ~unix_path ~coq_root ~implicit) + (List.rev !includes); + (* additional ml directories, given with option -I *) + List.iter Mltop.add_ml_dir (List.rev !ml_includes) let init_library_roots () = includes := [] @@ -134,12 +133,14 @@ let init_ocaml_path () = List.iter add_subdir [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; - [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ] + [ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ]; + [ "grammar" ]; [ "ide" ] ] let get_compat_version = function + | "8.4" -> Flags.V8_4 | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - msg_warn ("Compatibility with version "^s^" not supported."); + msg_warning (strbrk ("Compatibility with version "^s^" not supported.")); Flags.V8_2 - | s -> Util.error ("Unknown compatibility version \""^s^"\".") + | s -> Errors.error ("Unknown compatibility version \""^s^"\".") -- cgit v1.2.3