Merge remote-tracking branch 'origin/pr/166' into trunk

Add -o option to coqc

12 files changed, 72 insertions, 29 deletions

diff --git a/CHANGES b/CHANGES
index 82076168ac..ae9b979292 100644
--- a/CHANGES
+++ b/CHANGES
@@ -31,6 +31,10 @@ Notations
 
 - "Bind Scope" can once again bind "Funclass" and "Sortclass".
 
+Tools
+
+- coqc accepts a -o option to specify the output file name
+
 Changes from V8.5pl1 to V8.5pl2
 ===============================
 
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index d06d4b3768..096305b987 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -25,9 +25,9 @@ let mk_absolute vfile =
   if Filename.is_relative vfile then CUnix.correct_path vfile (Sys.getcwd ())
   else vfile
 
-let start_aux_file_for vfile =
-  let vfile = mk_absolute vfile in
-  oc := Some (open_out (aux_file_name_for vfile));
+let start_aux_file ~aux_file:output_file ~v_file =
+  let vfile = mk_absolute v_file in
+  oc := Some (open_out output_file);
   Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n"
     version (Digest.to_hex (Digest.file vfile)) vfile
 
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index 127827ab6a..86e322b71d 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -17,7 +17,8 @@ module H : Map.S with type key = int * int
 module M : Map.S with type key = string
 val contents : aux_file -> string M.t H.t
 
-val start_aux_file_for : string -> unit
+val aux_file_name_for : string -> string
+val start_aux_file : aux_file:string -> v_file:string -> unit
 val stop_aux_file : unit -> unit 
 val recording : unit -> bool
 
diff --git a/lib/flags.ml b/lib/flags.ml
index f07877e20d..ba19c7a63b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,6 +47,7 @@ let batch_mode = ref false
 
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 let compilation_mode = ref BuildVo
+let compilation_output_name = ref None
 
 let test_mode = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 729c21fcf9..8fe64d24fa 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -14,6 +14,7 @@ val load_init : bool ref
 val batch_mode : bool ref
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 val compilation_mode : compilation_mode ref
+val compilation_output_name : string option ref
 
 val test_mode : bool ref
 
diff --git a/library/library.ml b/library/library.ml
index 4d0082850e..bc7723f481 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -628,17 +628,14 @@ let check_module_name s =
         done
     | c -> err c
 
-let start_library f =
-  let () = if not (Sys.file_exists f) then
-    errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f))
-  in
+let start_library fo =
   let ldir0 =
     try
-      let lp = Loadpath.find_load_path (Filename.dirname f) in
+      let lp = Loadpath.find_load_path (Filename.dirname fo) in
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let file = Filename.chop_extension (Filename.basename f) in
+  let file = Filename.chop_extension (Filename.basename fo) in
   let id = Id.of_string file in
   check_module_name file;
   check_coq_overwriting ldir0 id;
@@ -693,12 +690,13 @@ let error_recursively_dependent_library dir =
    writing the content and computing the checksum... *)
 
 let save_library_to ?todo dir f otab =
-  let f, except = match todo with
+  let except = match todo with
     | None ->
         assert(!Flags.compilation_mode = Flags.BuildVo);
-        f ^ "o", Future.UUIDSet.empty
+        assert(Filename.check_suffix f ".vo");
+        Future.UUIDSet.empty
     | Some (l,_) ->
-        f ^ "io",
+        assert(Filename.check_suffix f ".vio");
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~except dir in
diff --git a/library/library.mli b/library/library.mli
index 8f5b775d8d..b9044b60dd 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -37,9 +37,9 @@ type seg_proofs = Term.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located list -> unit
 
-(** 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. *)
+(** Start the compilation of a file as a library. The first argument must be
+    output file, and the 
+    returned path is the associated absolute logical path of the library. *)
 val start_library : CUnix.physical_path -> DirPath.t
 
 (** End the compilation of a library and save it to a ".vo" file *)
diff --git a/stm/stm.ml b/stm/stm.ml
index f312e8539e..c0813827de 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2379,11 +2379,11 @@ let handle_failure (e, info) vcs tty =
       VCS.print ();
       iraise (e, info)
 
-let snapshot_vio ldir long_f_dot_v =
+let snapshot_vio ldir long_f_dot_vo =
   finish ();
   if List.length (VCS.branches ()) > 1 then
     Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
-  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
+  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
     (Global.opaque_tables ())
 
 let reset_task_queue = Slaves.reset_task_queue
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 18b2a24fa0..ecbbfefac6 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -107,6 +107,7 @@ let parse_args () =
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
+      |"-o"
       as o) :: rem ->
 	begin
 	  match rem with
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a488bb3e64..a820008d2e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -532,6 +532,7 @@ let parse_args arglist =
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
     |"-toploop" -> set_toploop (next ())
     |"-w" -> set_warning (next ())
+    |"-o" -> Flags.compilation_output_name := Some (next())
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 5359a288ac..ffbbe7ed4a 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -45,6 +45,7 @@ let print_usage_channel co command =
 \n  -require path          load Coq library path and import it (Require Import path.)\
 \n  -compile f.v           compile Coq file f.v (implies -batch)\
 \n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
+\n  -o f.vo                use f.vo as the output file name\
 \n  -quick                 quickly compile .v files to .vio files (skip proofs)\
 \n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
 \n                         into fi.vo\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1c3f0d9976..0a32c88d64 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -290,12 +290,35 @@ let load_vernac verb file =
     if !Flags.beautify_file then close_out !chan_beautify;
     raise_with_file file (disable_drop e, info)
 
-let ensure_v f =
-  if Filename.check_suffix f ".v" then f
+let ensure_ext ext f =
+  if Filename.check_suffix f ext then f
   else begin
     Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
-    expanded to \"" ++ str f ++ str ".v\"");
-    f ^ ".v"
+    expanded to \"" ++ str f ++ str ext ++ str "\"");
+    f ^ ext
+  end
+
+let ensure_bname src tgt =
+  let src, tgt = Filename.basename src, Filename.basename tgt in
+  let src, tgt = Filename.chop_extension src, Filename.chop_extension tgt in
+  if src <> tgt then begin
+    Feedback.msg_error (str "Source and target file names must coincide, directories can differ");
+    Feedback.msg_error (str "Source: " ++ str src);
+    Feedback.msg_error (str "Target: " ++ str tgt);
+    flush_all ();
+    exit 1
+  end
+
+let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
+
+let ensure_v v = ensure ".v" v v
+let ensure_vo v vo = ensure ".vo" v vo
+let ensure_vio v vio = ensure ".vio" v vio
+
+let ensure_exists f =
+  if not (Sys.file_exists f) then begin
+    Feedback.msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f));
+    exit 1
   end
 
 (* Compile a vernac file *)
@@ -307,9 +330,16 @@ let compile verbosely f =
   match !Flags.compilation_mode with
   | BuildVo ->
       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;
+      ensure_exists long_f_dot_v;
+      let long_f_dot_vo =
+        match !Flags.compilation_output_name with
+        | None -> long_f_dot_v ^ "o"
+        | Some f -> ensure_vo long_f_dot_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_vo in
+      Stm.set_compilation_hints long_f_dot_vo;
+      Aux_file.(start_aux_file
+        ~aux_file:(aux_file_name_for long_f_dot_vo)
+        ~v_file:long_f_dot_v);
       Dumpglob.start_dump_glob long_f_dot_v;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       if !Flags.xml_export then Hook.get f_xml_start_library ();
@@ -318,7 +348,7 @@ let compile verbosely f =
       Stm.join ();
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
-      Library.save_library_to ldir long_f_dot_v (Global.opaque_tables ());
+      Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
       Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
@@ -326,13 +356,18 @@ let compile verbosely f =
       Dumpglob.end_dump_glob ()
   | BuildVio ->
       let long_f_dot_v = ensure_v f in
-      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
+      ensure_exists long_f_dot_v;
+      let long_f_dot_vio =
+        match !Flags.compilation_output_name with
+        | None -> long_f_dot_v ^ "io"
+        | Some f -> ensure_vio long_f_dot_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_vio in
       Dumpglob.noglob ();
-      Stm.set_compilation_hints long_f_dot_v;
+      Stm.set_compilation_hints long_f_dot_vio;
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
-      Stm.snapshot_vio ldir long_f_dot_v;
+      Stm.snapshot_vio ldir long_f_dot_vio;
       Stm.reset_task_queue ()
   | Vio2Vo ->
       let open Filename in