coqc: support -o option to specify output file name

The -o option lets one put .vo or .vio files in a directory of choice,
i.e. decouple the location of the sources and the compiled files.
This ease the integration of Coq in already existing IDEs that handle
the build process automatically (eg Eclipse) and also enables one to
compile/run at the same time 2 versions of Coq on the same sources.

Example: b.v depending on a.v

  coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo
  coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo

  coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo
  coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo

11 files changed, 68 insertions, 29 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index f7bd81f85..c814438dd 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 127827ab6..86e322b71 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 c1ec9738c..9a209a2b3 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 24780f0dc..f52a14a30 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 8e2402dda..34dbdfeba 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 8f5b775d8..b9044b60d 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 8f11875b6..ebafed8d3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2108,11 +2108,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 f957200ab..d4f1447b1 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 c4222b330..379a96b89 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -514,6 +514,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 f855c096e..aa27b952f 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 64225a644..c47fde788 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -291,12 +291,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
     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
+    msg_error (str "Source and target file names must coincide, directories can differ");
+    msg_error (str "Source: " ++ str src);
+    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
+    msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f));
+    exit 1
   end
 
 (* Compile a vernac file *)
@@ -308,9 +331,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 ();
@@ -319,7 +349,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 ();
@@ -327,13 +357,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