Imported Upstream version 8.5~beta1+dfsg

1 files changed, 68 insertions, 67 deletions

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     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
-open System
-open Toplevel
 
-let (/) s1 s2 = s1 ^ "/" ^ s2
+let ( / ) s1 s2 = s1 ^ "/" ^ s2
 
-let set_debug () = Flags.debug := true
+let set_debug () =
+  let () = Backtrace.record_backtrace true in
+  Flags.debug := true
 
 (* Loading of the ressource file.
    rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one
@@ -30,16 +31,19 @@ let load_rcfile() =
   if !load_rc then
     try
       if !rcfile_specified then
-        if file_readable_p !rcfile then
+        if CUnix.file_readable_p !rcfile then
           Vernac.load_vernac false !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
-      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
+      else
+	try
+	  let warn x = msg_warning (str x) in
+	  let inferedrc = List.find CUnix.file_readable_p [
+	    Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
+	    Envars.xdg_config_home warn / rcdefaultname;
+	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
+	    Envars.home ~warn / "."^rcdefaultname
+	  ] in
+          Vernac.load_vernac false inferedrc
 	with Not_found -> ()
 	(*
 	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^"\".")