diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/library.ml | 12 | ||||
-rw-r--r-- | library/library.mli | 10 |
2 files changed, 12 insertions, 10 deletions
diff --git a/library/library.ml b/library/library.ml index f7ca4e976..1bcffcd14 100644 --- a/library/library.ml +++ b/library/library.ml @@ -678,22 +678,22 @@ let check_module_name s = | c -> err c let start_library f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let () = if not (Sys.file_exists f) then + errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f)) + in let ldir0 = try - let lp = Loadpath.find_load_path (Filename.dirname longf) in + let lp = Loadpath.find_load_path (Filename.dirname f) in Loadpath.logical lp with Not_found -> Nameops.default_root_prefix in - let file = Filename.basename f in + let file = Filename.chop_extension (Filename.basename f) in let id = Id.of_string file in check_module_name file; check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; - ldir,longf + ldir let load_library_todo f = let paths = Loadpath.get_paths () in diff --git a/library/library.mli b/library/library.mli index 967a54e4c..f2e60718d 100644 --- a/library/library.mli +++ b/library/library.mli @@ -25,7 +25,7 @@ val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> u val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit -(** {6 ... } *) +(** {6 Start the compilation of a library } *) (** Segments of a library *) type seg_sum @@ -39,10 +39,12 @@ type seg_proofs = Term.constr Future.computation array an export otherwise just a simple import *) val import_module : bool -> qualid located list -> unit -(** {6 Start the compilation of a library } *) -val start_library : string -> DirPath.t * string +(** Start the compilation of a file as a library. The argument must be an + existing file on the system, and the returned path is the associated + absolute logical path of the library. *) +val start_library : CUnix.physical_path -> DirPath.t -(** {6 End the compilation of a library and save it to a ".vo" file } *) +(** End the compilation of a library and save it to a ".vo" file *) val save_library_to : ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit |