Merge PR #6276: Coqchk accepts filenames

3 files changed, 52 insertions, 17 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 180ca1ece1..21fdba1faf 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -22,6 +22,11 @@ let extend_dirpath p id = DirPath.make (id :: DirPath.repr p)
 type section_path = {
   dirpath : string list ;
   basename : string }
+
+type object_file =
+| PhysicalFile of CUnix.physical_path
+| LogicalFile of section_path
+
 let dir_of_path p =
   DirPath.make (List.map Id.of_string p.dirpath)
 let path_of_dirpath dir =
@@ -69,11 +74,6 @@ let libraries_table = ref LibraryMap.empty
 let find_library dir =
   LibraryMap.find dir !libraries_table
 
-let try_find_library dir =
-  try find_library dir
-  with Not_found ->
-    user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir)))
-
 let library_full_filename dir = (find_library dir).library_filename
 
   (* If a library is loaded several time, then the first occurrence must
@@ -263,7 +263,17 @@ let try_locate_absolute_library dir =
     | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir)
     | LibNotFound -> error_lib_not_found (path_of_dirpath dir)
 
-let try_locate_qualified_library qid =
+let try_locate_qualified_library lib = match lib with
+| PhysicalFile f ->
+  let () =
+    if not (System.file_exists_respecting_case "" f) then
+      error_lib_not_found { dirpath = []; basename = f; }
+  in
+  let dir = Filename.dirname f in
+  let base = Filename.chop_extension (Filename.basename f) in
+  let dir = extend_dirpath (find_logical_path dir) (Id.of_string base) in
+  (dir, f)
+| LogicalFile qid ->
   try
     locate_qualified_library qid
   with
@@ -412,9 +422,3 @@ let recheck_library ~norec ~admit ~check =
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
   List.iter (check_one_lib nochk) needed;
   Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked")
-
-open Printf
-
-let mem s =
-  let m = try_find_library s in
-  h 0 (str (sprintf "%dk" (CObj.size_kb m)))
diff --git a/checker/check.mli b/checker/check.mli
new file mode 100644
index 0000000000..28ae385b5b
--- /dev/null
+++ b/checker/check.mli
@@ -0,0 +1,30 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open CUnix
+open Names
+
+type section_path = {
+  dirpath : string list;
+  basename : string;
+}
+
+type object_file =
+| PhysicalFile of physical_path
+| LogicalFile of section_path
+
+type logical_path = DirPath.t
+
+val default_root_prefix : DirPath.t
+
+val add_load_path : physical_path * logical_path -> unit
+
+val recheck_library :
+  norec:object_file list ->
+  admit:object_file list ->
+  check:object_file list -> unit
diff --git a/checker/checker.ml b/checker/checker.ml
index e960a55fd2..b2433ee364 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -40,9 +40,10 @@ let dirpath_of_string s =
       [] -> Check.default_root_prefix
     | dir -> DirPath.make (List.map Id.of_string dir)
 let path_of_string s =
-  match parse_dir s with
+  if Filename.check_suffix s ".vo" then PhysicalFile s
+  else match parse_dir s with
       [] -> invalid_arg "path_of_string"
-    | l::dir -> {dirpath=dir; basename=l}
+    | l::dir -> LogicalFile {dirpath=dir; basename=l}
 
 let ( / ) = Filename.concat
 
@@ -144,15 +145,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
 let engage () = Safe_typing.set_engagement (!impredicative_set)
 
 
-let admit_list = ref ([] : section_path list)
+let admit_list = ref ([] : object_file list)
 let add_admit s =
   admit_list := path_of_string s :: !admit_list
 
-let norec_list = ref ([] : section_path list)
+let norec_list = ref ([] : object_file list)
 let add_norec s =
   norec_list := path_of_string s :: !norec_list
 
-let compile_list = ref ([] : section_path list)
+let compile_list = ref ([] : object_file list)
 let add_compile s =
   compile_list := path_of_string s :: !compile_list