The -compile option now accepts ".v" files and outputs a warning otherwise.

3 files changed, 25 insertions, 13 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
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 266d8f9b4..14d2bcea4 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -294,7 +294,15 @@ let load_vernac verb file =
     if !Flags.beautify_file then close_out !chan_beautify;
     raise_with_file file (disable_drop e, info)
 
-(* Compile a vernac file (f is assumed without .v suffix) *)
+let ensure_v f =
+  if Filename.check_suffix f ".v" then f
+  else begin
+    msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
+    expanded to \"" ++ str f ++ str ".v\"");
+    f ^ ".v"
+  end
+
+(* Compile a vernac file *)
 let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
@@ -302,7 +310,8 @@ let compile verbosely f =
       (msg_error (str "There are pending proofs"); flush_all (); exit 1) in
   match !Flags.compilation_mode with
   | BuildVo ->
-      let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
+      let long_f_dot_v = ensure_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
       Stm.set_compilation_hints long_f_dot_v;
       Aux_file.start_aux_file_for long_f_dot_v;
       Dumpglob.start_dump_glob long_f_dot_v;
@@ -318,7 +327,8 @@ let compile verbosely f =
       Aux_file.stop_aux_file ();
       Dumpglob.end_dump_glob ()
   | BuildVio ->
-      let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
+      let long_f_dot_v = ensure_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
       Dumpglob.noglob ();
       Stm.set_compilation_hints long_f_dot_v;
       let _ = load_vernac verbosely long_f_dot_v in