diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | config/coq_config.mli | 2 | ||||
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 7 | ||||
| -rw-r--r-- | lib/system.ml | 95 | ||||
| -rw-r--r-- | lib/system.mli | 24 | ||||
| -rw-r--r-- | library/library.ml | 33 | ||||
| -rw-r--r-- | library/library.mli | 5 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 3 | ||||
| -rwxr-xr-x | tools/coqdep.ml | 5 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 36 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 13 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 5 |
16 files changed, 137 insertions, 108 deletions
@@ -355,13 +355,15 @@ COQDEPCMO=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo $(COQDEP): $(COQDEPCMO) $(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) -beforedepend:: $(COQDEP) +beforedepend:: tools/coqdep_lexer.ml $(COQDEP) GALLINACMO=tools/gallina_lexer.cmo tools/gallina.cmo $(GALLINA): $(GALLINACMO) $(OCAMLC) $(BYTEFLAGS) -custom -o $@ $(GALLINACMO) +beforedepend:: tools/gallina_lexer.ml + $(COQMAKEFILE): tools/coq_makefile.ml $(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coq_makefile.ml @@ -415,6 +417,8 @@ install-library: $(MKDIR) $(COQLIB)/`dirname $$f`; \ cp $$f $(COQLIB)/`dirname $$f`; \ done + $(MKDIR) $(COQLIB)/states + cp states/*.coq $(COQLIB)/states $(MKDIR) $(EMACSLIB) cp tools/coq.el tools/coq.elc $(EMACSLIB) diff --git a/config/coq_config.mli b/config/coq_config.mli index be3fd4cbc..b7731b8ab 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -23,5 +23,5 @@ val date : string (* release date *) val compile_date : string (* compile date *) val theories_dirs : string list -val tactics_dirs : string list +val contrib_dirs : string list @@ -473,7 +473,7 @@ echo_e "\nlet theories_dirs = [" >> $mlconfig_file subdirs theories echo_e "]\n" >> $mlconfig_file -echo_e "\nlet tactics_dirs = [" >> $mlconfig_file +echo_e "\nlet contrib_dirs = [" >> $mlconfig_file subdirs contrib echo_e "]\n" >> $mlconfig_file diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 47a800b68..a321ce1ab 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -110,7 +110,8 @@ let uri_of_path sp = match sl with [] -> assert false (*V7 WHAT NOW? *) | module_name::_ -> - trim_wrong_uri_prefix (Library.module_filename module_name) + let _,file = Library.module_filename module_name in + trim_wrong_uri_prefix file in "cic:" ^ module_path ^ "/" ^ (String.concat "/" sl) ^ "/" ^ (N.string_of_id id) ^ "." ^ (ext_of_sp sp) @@ -786,10 +787,10 @@ let printModule id dn = let sp = Lib.make_path id N.OBJ in let ls = L.module_segment (Some str) in print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ " " ^ - L.module_filename str ^ "\n") ; + (snd (L.module_filename str)) ^ "\n") ; print_closed_section str ls dn ; print_if_verbose ("MODULE_END " ^ str ^ " " ^ N.string_of_path sp ^ " " ^ - L.module_filename str ^ "\n") + (snd (L.module_filename str)) ^ "\n") ;; (* printSection identifier directory_name *) diff --git a/lib/system.ml b/lib/system.ml index 8c8dca7ba..fd7e93bd0 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -8,15 +8,23 @@ open Unix (* Files and load path. *) (* All subdirectories, recursively *) +type load_path_entry = { + directory : string; + root_dir : string; + relative_subdir : string } + +type load_path = load_path_entry list + let exists_dir dir = try let _ = opendir dir in true with Unix_error _ -> false -let all_subdirs dir = +let all_subdirs root = let l = ref [] in - let add f = l := f :: !l in - let rec traverse dir = - Printf.printf "%s\n" dir; + let add f rel = + l := { directory = f; root_dir = root; relative_subdir = rel } :: !l + in + let rec traverse dir rel = let dirh = try opendir dir with Unix_error _ -> invalid_arg "all_subdirs" in @@ -26,14 +34,15 @@ let all_subdirs dir = if f <> "." && f <> ".." then let file = Filename.concat dir f in if (stat file).st_kind = S_DIR then begin - add file; - traverse file + let newrel = Filename.concat rel f in + add file newrel; + traverse file newrel end done with End_of_file -> closedir dirh in - traverse dir; List.rev !l + traverse root ""; List.rev !l let safe_getenv_def var def = try @@ -49,9 +58,9 @@ let glob s = s let search_in_path path filename = let rec search = function - | dir :: rem -> - let f = glob (Filename.concat dir filename) in - if Sys.file_exists f then f else search rem + | lpe :: rem -> + let f = glob (Filename.concat lpe.directory filename) in + if Sys.file_exists f then (lpe,f) else search rem | [] -> raise Not_found in @@ -62,7 +71,8 @@ let where_in_path = search_in_path let find_file_in_path paths name = let globname = glob name in if not (Filename.is_relative globname) then - globname + let root = Filename.dirname globname in + { directory = root; root_dir = root; relative_subdir = "" }, globname else try search_in_path paths name @@ -97,47 +107,40 @@ let marshal_in ch = Marshal.from_channel ch exception Bad_magic_number of string -let (raw_extern_intern : - int -> string -> - (string -> string * out_channel) - * (string list -> string -> string * in_channel)) - = fun magic suffix -> - let extern_state name = - let (_,channel) as filec = - open_trapping_failure (fun n -> n,open_out_bin n) name suffix in - output_binary_int channel magic; - filec - and intern_state paths name = - let fname = find_file_in_path paths (make_suffix name suffix) in - let channel = open_in_bin fname in - if input_binary_int channel <> magic then - raise (Bad_magic_number fname); - (fname,channel) - in - (extern_state,intern_state) - -let (extern_intern : - int -> string -> (string -> 'a -> unit) * (string list -> string -> 'a)) - = fun magic suffix -> - let (raw_extern,raw_intern) = raw_extern_intern magic suffix in - let extern_state name val_0 = - try - let (fname,channel) = raw_extern name in - try - marshal_out channel val_0; - close_out channel - with e -> - begin try_remove fname; raise e end - with Sys_error s -> error ("System error: " ^ s) +let raw_extern_intern magic suffix = + let extern_state name = + let (_,channel) as filec = + open_trapping_failure (fun n -> n,open_out_bin n) name suffix in + output_binary_int channel magic; + filec + and intern_state paths name = + let lpe,fname = find_file_in_path paths (make_suffix name suffix) in + let channel = open_in_bin fname in + if input_binary_int channel <> magic then + raise (Bad_magic_number fname); + (lpe,fname,channel) + in + (extern_state,intern_state) +let extern_intern magic suffix = + let (raw_extern,raw_intern) = raw_extern_intern magic suffix in + let extern_state name val_0 = + try + let (fname,channel) = raw_extern name in + try + marshal_out channel val_0; + close_out channel + with e -> + begin try_remove fname; raise e end + with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try - let (fname,channel) = raw_intern paths name in + let (_,fname,channel) = raw_intern paths name in let v = marshal_in channel in close_in channel; v - with Sys_error s -> error("System error: " ^ s) - + with Sys_error s -> + error("System error: " ^ s) in (extern_state,intern_state) diff --git a/lib/system.mli b/lib/system.mli index da5effca8..18dae1915 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,11 +1,20 @@ (* $Id$ *) -(*s Files. *) +(*s Files and load paths. Load path entries remember the original root + given by the user. For efficiency, we keep the full path (field + [directory]), the root path and the path relative to the root. *) -val all_subdirs : string -> string list -val is_in_path : string list -> string -> bool -val where_in_path : string list -> string -> string +type load_path_entry = { + directory : string; + root_dir : string; + relative_subdir : string } + +type load_path = load_path_entry list + +val all_subdirs : string -> load_path +val is_in_path : load_path -> string -> bool +val where_in_path : load_path -> string -> load_path_entry * string val make_suffix : string -> string -> string val file_readable_p : string -> bool @@ -16,7 +25,7 @@ val home : string val exists_dir : string -> bool -val find_file_in_path : string list -> string -> string +val find_file_in_path : load_path -> string -> load_path_entry * string (*s Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] @@ -29,11 +38,10 @@ exception Bad_magic_number of string val raw_extern_intern : int -> string -> (string -> string * out_channel) * - (path:string list -> string -> string * in_channel) + (load_path -> string -> load_path_entry * string * in_channel) val extern_intern : - int -> string -> (string -> 'a -> unit) * - (path:string list -> string -> 'a) + int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a) (*s Time stamps. *) diff --git a/library/library.ml b/library/library.ml index 4a76bff1c..ca4309634 100644 --- a/library/library.ml +++ b/library/library.ml @@ -3,33 +3,28 @@ open Pp open Util +open System open Names open Environ open Libobject open Lib -(*s Load path. Used for commands Add Path, Remove Path, Print Path *) +(*s Load path. *) -let loadpath_name = "LoadPath" +let load_path = ref ([] : load_path) -module LoadPath = struct - let check s = if not (System.exists_dir s) then warning (s^" was not found") - let key = Goptions.PrimaryTable loadpath_name - let title = "Load Paths for Coq files" - let member_message s b = - if b then s^" is declared in the load path for Coq files" - else s^" is not declared in the load path for Coq files" - let synchronous = false -end +let get_load_path () = !load_path -module LoadPathTable = Goptions.MakeStringTable(LoadPath) +let add_load_path_entry lpe = load_path := lpe :: !load_path -let get_load_path = LoadPathTable.elements let add_path dir = - (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#add dir + add_load_path_entry { directory = dir; root_dir = dir; relative_subdir = "" } + let remove_path dir = - (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#remove dir -let rec_add_path dir = List.iter add_path (System.all_subdirs dir) + load_path := List.filter (fun lpe -> lpe.directory <> dir) !load_path + +let rec_add_path dir = + load_path := (all_subdirs dir) @ !load_path (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) @@ -45,7 +40,7 @@ type module_disk = { type module_t = { module_name : string; - module_filename : string; + module_filename : load_path_entry * string; module_compiled_env : compiled_env; module_declarations : library_segment; mutable module_opened : bool; @@ -129,12 +124,12 @@ let load_objects decls = segment_iter load_object decls let rec load_module_from s f = - let (fname,ch) = raw_intern_module (get_load_path ()) f in + let (lpe,fname,ch) = raw_intern_module (get_load_path ()) f in let md = System.marshal_in ch in let digest = System.marshal_in ch in close_in ch; let m = { module_name = md.md_name; - module_filename = fname; + module_filename = (lpe,fname); module_compiled_env = md.md_compiled_env; module_declarations = md.md_declarations; module_opened = false; diff --git a/library/library.mli b/library/library.mli index 474669452..cac8767d5 100644 --- a/library/library.mli +++ b/library/library.mli @@ -38,10 +38,11 @@ val save_module_to : string -> string -> unit [module_filename] returns the full filename of a loaded module. *) val module_segment : string option -> Lib.library_segment -val module_filename : string -> string +val module_filename : string -> System.load_path_entry * string (*s Global load path *) -val get_load_path : unit -> string list +val get_load_path : unit -> System.load_path +val add_load_path_entry : System.load_path_entry -> unit val add_path : string -> unit val rec_add_path : string -> unit val remove_path : string -> unit diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index e8b40ccea..ff6b3e24d 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -88,8 +88,7 @@ GEXTEND Gram | IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >> | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >> | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >> - | IDENT "AddRecPath"; dir = stringarg; "." -> - <:ast< (RECADDPATH $dir) >> + | IDENT "AddRecPath"; dir = stringarg; "." -> <:ast< (RECADDPATH $dir) >> | IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >> | IDENT "Print"; "Proof"; id = identarg; "." -> diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 16b0e4809..0c9407cb2 100755 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -397,9 +397,10 @@ let coqdep () = Coq_config.theories_dirs; let tactics = Filename.concat !coqlib "tactics" in add_coqlib_directory tactics; + let contrib = Filename.concat !coqlib "contrib" in List.iter - (fun s -> add_coqlib_directory (Filename.concat tactics s)) - Coq_config.tactics_dirs; + (fun s -> add_coqlib_directory (Filename.concat contrib s)) + Coq_config.contrib_dirs; mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu); mlKnown := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu); vKnown := !vKnown @ !vAccu; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 96b594106..432f6c5e0 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -45,10 +45,15 @@ let add_include s = Mltop.dir_ml_dir s; Library.add_path s +let add_rec_include s = + let subdirs = all_subdirs s in + List.iter (fun lpe -> Mltop.dir_ml_dir lpe.directory) subdirs; + List.iter Library.add_load_path_entry subdirs + (* By the option -include -I or -R of the command line *) let includes = ref [] -let push_include s = includes := s :: !includes -let rec_include s = includes := (all_subdirs s) @ !includes +let push_include s = includes := (s,false) :: !includes +let push_rec_include s = includes := (s,true) :: !includes (* Because find puts "./" and the loadpath is not nicely pretty-printed *) let hm2 s = @@ -59,22 +64,31 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft (* Initializes the LoadPath according to COQLIB and Coq_config *) let init_load_path () = - if Coq_config.local then + if Coq_config.local then begin (* local use (no installation) *) List.iter (fun s -> add_include (Filename.concat Coq_config.coqtop s)) - ("states" :: "dev" :: - (List.map - (fun s -> Filename.concat "theories" (hm2 s)) - Coq_config.theories_dirs)) - else begin - (* default load path; only if COQLIB is defined *) + ["states"; "dev"]; + let theories = Filename.concat Coq_config.coqtop "theories" in + List.iter + (fun s -> add_include (Filename.concat theories (hm2 s))) + Coq_config.theories_dirs; + add_include (Filename.concat Coq_config.coqtop "tactics"); + let contrib = Filename.concat Coq_config.coqtop "contrib" in + List.iter + (fun s -> add_include (Filename.concat contrib (hm2 s))) + Coq_config.contrib_dirs + end else begin + (* default load path; variable COQLIB overrides the default library *) let coqlib = getenv_else "COQLIB" Coq_config.coqlib in - add_include coqlib + add_rec_include coqlib end; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in add_include camlp4; add_include "."; (* additional loadpath, given with -I -include -R options *) - List.iter add_include (List.rev !includes); + List.iter + (fun (s,reci) -> if reci then add_rec_include s else add_include s) + (List.rev !includes); includes := [] + diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index ca74f9ec7..7baa825be 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -11,10 +11,7 @@ val set_rcuser : string -> unit val no_load_rc : unit -> unit val load_rcfile : unit -> unit -val add_include : string -> unit val push_include : string -> unit -val rec_include : string -> unit - -val hm2 : string -> string +val push_rec_include : string -> unit val init_load_path : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 564acaee6..456384d90 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -78,7 +78,7 @@ let parse_args () = | ("-I"|"-include") :: d :: rem -> push_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: rem -> rec_include d; parse rem + | "-R" :: d :: rem -> push_rec_include d; parse rem | "-R" :: [] -> usage () | "-q" :: rem -> no_load_rc (); parse rem diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index c5d628769..66577bea6 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -3,6 +3,7 @@ open Util open Pp +open System open Libobject open Library open System @@ -33,7 +34,10 @@ open Vernacinterp (* This path is where we look for .cmo *) let coq_mlpath_copy = ref [] -let keep_copy_mlpath s = coq_mlpath_copy := (glob s)::!coq_mlpath_copy +let keep_copy_mlpath s = + let dir = glob s in + let lpe = { directory = dir; root_dir = dir; relative_subdir = "" } in + coq_mlpath_copy := lpe :: !coq_mlpath_copy (* If there is a toplevel under Coq *) type toplevel = { @@ -86,7 +90,7 @@ let dir_ml_load s = | WithoutTop -> ifdef Byte then (if is_in_path !coq_mlpath_copy s then - let gname = where_in_path !coq_mlpath_copy s in + let _,gname = where_in_path !coq_mlpath_copy s in try Dynlink.loadfile gname; Dynlink.add_interfaces @@ -119,7 +123,8 @@ let dir_ml_dir s = | _ -> () (* For Rec Add ML Path *) -let rdir_ml_dir dir = List.iter dir_ml_dir (all_subdirs dir) +let rdir_ml_dir dir = + List.iter (fun lpe -> dir_ml_dir lpe.directory) (all_subdirs dir) (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -231,7 +236,7 @@ let declare_ml_modules l = let print_ml_path () = let l = !coq_mlpath_copy in pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR" "; - hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >] + hV 0 (prlist_with_sep pr_fnl (fun e -> [< 'sTR e.directory >]) l) >] let _ = vinterp_add "DeclareMLModule" (fun l -> diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c755419df..7997b2451 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -51,7 +51,7 @@ let real_error = function the file we parse seems a bit risky to me. B.B. *) let open_file_twice_if verbosely fname = - let longfname = find_file_in_path (Library.get_load_path ()) fname in + let _,longfname = find_file_in_path (Library.get_load_path ()) fname in let in_chan = open_in longfname in let verb_ch = if verbosely then Some (open_in longfname) else None in let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5ae050039..7f584a4b9 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -106,7 +106,8 @@ let show_top_evars () = let locate_file f = try - mSG [< 'sTR (System.where_in_path (get_load_path()) f); 'fNL >] + let _,file = System.where_in_path (get_load_path()) f in + mSG [< 'sTR file; 'fNL >] with Not_found -> mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC; 'sTR"on loadpath"; 'fNL >]) @@ -120,7 +121,7 @@ let locate_id id = let print_loadpath () = let l = get_load_path () in mSGNL [< 'sTR"Load Path:"; 'fNL; 'sTR" "; - hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >] + hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s.directory >]) l) >] let get_current_context_of_args = function | [VARG_NUMBER n] -> get_goal_context n |