From da4d0b0e3d82621fe8338dd313b788472fc31bb2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 10:26:08 +0200 Subject: Remove some uses of Loadpath.get_paths. The single remaining use is in library/states.ml. This use should be reviewed, as it is most certainly broken. The other uses of Loadpath.get_paths did not disappear by miracle though. They were replaced by a new function Loadpath.locate_file which factors all the uses of the function. This function should not be used as it is as broken as Loadpath.get_paths, by definition. Vernac.load_vernac now takes a complete path rather than looking up for the file. That is the way it was used most of the time, so the lookup was unnecessary. For instance, Vernac.compile was calling Library.start_library which already expected a complete path. Another consequence is that System.find_file_in_path is almost no longer used (except for Loadpath.locate_file, obviously). The two remaining uses are System.intern_state (used by States.intern_state, cf above) and Mltop.dir_ml_load for dynamically loading compiled .ml files. --- library/library.ml | 4 +--- library/loadpath.ml | 6 ++++++ library/loadpath.mli | 4 ++++ stm/vio_checking.ml | 4 +--- toplevel/coqtop.ml | 1 + toplevel/vernac.ml | 13 ++++--------- toplevel/vernacentries.ml | 7 ++----- 7 files changed, 19 insertions(+), 20 deletions(-) diff --git a/library/library.ml b/library/library.ml index 6d7b0f603..f5c7f6335 100644 --- a/library/library.ml +++ b/library/library.ml @@ -652,9 +652,7 @@ let start_library f = ldir let load_library_todo f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let longf = Loadpath.locate_file (f^".v") in let f = longf^"io" in let ch = System.with_magic_number_check raw_intern_library f in let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in diff --git a/library/loadpath.ml b/library/loadpath.ml index 26af809e7..d35dca212 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -112,3 +112,9 @@ let expand_path dir = if DirPath.equal dir lg then (ph, lg) :: aux l else aux l in aux !load_paths + +let locate_file fname = + let paths = get_paths () in + let _,longfname = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + longfname diff --git a/library/loadpath.mli b/library/loadpath.mli index 3251b8c60..c2c689af7 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -52,3 +52,7 @@ val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list (** As {!expand_path} but uses a filter function instead, and ignores the implicit status of loadpaths. *) + +val locate_file : string -> string +(** Locate a file among the registered paths. Do not use this function, as + it does not respect the visibility of paths. *) diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 4df9603dc..06bf955c8 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -104,9 +104,7 @@ let schedule_vio_compilation j fs = let f = if Filename.check_suffix f ".vio" then Filename.chop_extension f else f in - let paths = Loadpath.get_paths () in - let _, long_f_dot_v = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let long_f_dot_v = Loadpath.locate_file (f^".v") in let aux = Aux_file.load_aux_file_for long_f_dot_v in let eta = try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time") diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b7f1e4a19..4031a161b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -162,6 +162,7 @@ let add_load_vernacular verb s = let load_vernacular () = List.iter (fun (s,b) -> + let s = Loadpath.locate_file s in if Flags.do_beautify () then with_option beautify_file (Vernac.load_vernac b) s else diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 14d2bcea4..a0cd618e9 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -97,10 +97,7 @@ let user_error loc s = Errors.user_err_loc (loc,"_",str s) Note: we could use only one thanks to seek_in, but seeking on and on in the file we parse seems a bit risky to me. B.B. *) -let open_file_twice_if verbosely fname = - let paths = Loadpath.get_paths () in - let _,longfname = - find_file_in_path ~warn:(Flags.is_verbose()) paths fname in +let open_file_twice_if verbosely longfname = let in_chan = open_utf8_file_in longfname in let verb_ch = if verbosely then Some (open_utf8_file_in longfname) else None in @@ -206,19 +203,17 @@ let rec vernac_com verbose checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in + let fname = CUnix.make_suffix fname ".v" in + let f = Loadpath.locate_file fname in let st = save_translator_coqdoc () in if !Flags.beautify_file then begin - let paths = Loadpath.get_paths () in - let _,f = find_file_in_path ~warn:(Flags.is_verbose()) - paths - (CUnix.make_suffix fname ".v") in chan_beautify := open_out (f^beautify_suffix); Pp.comments := [] end; begin try - read_vernac_file verbosely (CUnix.make_suffix fname ".v"); + read_vernac_file verbosely f; restore_translator_coqdoc st; with reraise -> let reraise = Errors.push reraise in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8efcccaaa..ec81a3f1a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -365,8 +365,7 @@ let dump_universes sorted s = (* "Locate" commands *) let locate_file f = - let paths = Loadpath.get_paths () in - let _, file = System.find_file_in_path ~warn:false paths f in + let file = Flags.silently Loadpath.locate_file f in str file let msg_found_library = function @@ -1845,9 +1844,7 @@ let vernac_load interp fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let input = - let paths = Loadpath.get_paths () in - let _,longfname = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in Pcoq.Gram.parsable (Stream.of_channel in_chan) in try while true do interp (snd (parse_sentence input)) done -- cgit v1.2.3