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

2 files changed, 10 insertions, 12 deletions

diff --git a/library/library.ml b/library/library.ml
index 8e2402ddae..34dbdfebac 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 *)