Ajout d'une option et d'une fonction compile pour fabriquer les .vo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1984 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 64 insertions, 49 deletions

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index f458e8dcff..a05f20728d 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -65,52 +65,27 @@ let check_module_name s =
 	done
     | c -> err c
 
- (* compilation of a file [file] with command [command] and args [args] *)
-
-let compile command args file =
-  let dirname = Filename.dirname file in
-  let basename = Filename.basename file in
-  let modulename =
-    if Filename.check_suffix basename ".v" then
-      Filename.chop_suffix basename ".v"
-    else
-      basename 
-  in
-  check_module_name modulename;
-  let tmpfile = Filename.temp_file "coqc" ".v" in
-  let args' = 
-    command :: "-batch" :: "-silent" :: args 
-    @ ["-load-vernac-source"; tmpfile] in
-  let devnull = 
-    if Sys.os_type = "Unix" then
-      Unix.openfile "/dev/null" [] 0o777 
-    else 
-      Unix.stdin
-  in 
-  let filevo = Filename.concat dirname (modulename ^ ".vo") in
-  let oc = open_out tmpfile in
-  Printf.fprintf oc "Module %s.\n" modulename;
-  Printf.fprintf oc "Load %s\"%s\".\n" 
-    (if !verbose then "Verbose " else "") (String.escaped file);
-  Printf.fprintf oc "Write Module %s \"%s\".\n" modulename
-    (String.escaped filevo);
-  flush oc;
-  close_out oc;
-  try
-    let pid =
-      Unix.create_process_env command
-        (Array.of_list args') environment devnull Unix.stdout Unix.stderr in
-    let status = Unix.waitpid [] pid in
-    if not !keep then Sys.remove tmpfile ;
-    match status with
-      | _, Unix.WEXITED 0 -> ()
-      | _, Unix.WEXITED 127 -> 
-	  Printf.printf "Cannot execute %s\n" command;
-	  exit 1
-      | _, Unix.WEXITED c -> exit c
-      | _                 -> exit 1
-  with _ -> 
-    if not !keep then Sys.remove tmpfile; exit 1
+let rec make_compilation_args = function
+  | [] -> []
+  | file :: fl -> 
+      let dirname = Filename.dirname file in
+      let basename = Filename.basename file in
+      let modulename =
+        if Filename.check_suffix basename ".v" then
+          Filename.chop_suffix basename ".v"
+        else
+          basename
+      in
+      check_module_name modulename;
+      let file = Filename.concat dirname modulename in
+      (if !verbose then "-compile-verbose" else "-compile")
+      :: file :: (make_compilation_args fl)
+
+(* compilation of files [files] with command [command] and args [args] *)
+
+let compile command args files =
+  let args' = command :: args @ (make_compilation_args files) in
+  Unix.execvpe command (Array.of_list args') environment 
 
 (* parsing of the command line
  *
@@ -192,6 +167,7 @@ let main () =
   let coqtopname = 
     if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension)
   in
-  List.iter (compile coqtopname args) cfiles
+(*  List.iter (compile coqtopname args) cfiles*)
+  compile coqtopname args cfiles
     
 let _ = Printexc.print main (); exit 0
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2c57b885e2..0b7d699d0d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -72,6 +72,14 @@ let require () =
       Library.require_module None qid  (Some s) false)
     (List.rev !require_list)
 
+let compile_list = ref ([] : (bool * string) list)
+let add_compile verbose s =
+  set_batch_mode ();
+  Options.make_silent true; 
+  compile_list := (verbose,s) :: !compile_list
+let compile_files () =
+  List.iter (fun (v,f) -> Vernac.compile v f) (List.rev !compile_list)
+
 (* Re-exec Coq in bytecode or native code if necessary. [s] is either
    ["byte"] or ["opt"]. Notice that this is possible since the nature of
    the toplevel has already been set in [Mltop] by the main file created
@@ -146,6 +154,12 @@ let parse_args () =
     | "-require" :: f :: rem -> add_require f; parse rem
     | "-require" :: []       -> usage ()
 
+    | "-compile" :: f :: rem -> add_compile false f; parse rem
+    | "-compile" :: []       -> usage ()
+
+    | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem
+    | "-compile-verbose" :: []       -> usage ()
+
     | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
     | "-unsafe" :: []       -> usage ()
 
@@ -207,7 +221,8 @@ let start () =
       require ();
       load_rcfile();
       load_vernacular ();
-      outputstate ()
+      compile_files ();
+      outputstate ();
     with e ->
       flush_all();
       if not !batch_mode then message "Error during initialization :";
@@ -215,7 +230,7 @@ let start () =
       exit 1
   end;
   if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
-  if not (!batch_mode) then Lib.init_toplevel_root ();
+  Lib.init_toplevel_root ();
   Toplevel.loop();
 (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index f9d5decd9d..087db150d0 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -35,6 +35,8 @@ let print_usage_channel co command =
   -load-vernac-source f  load Coq file f.v (Load f.)
   -load-vernac-object f  load Coq object file f.vo
   -require f             load Coq object file f.vo and import it (Require f.)
+  -compile f             compile Coq file f.v (implies -batch)
+  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)
 
   -opt                   run the native-code version of Coq or Coq_SearchIsos
   -bindir dir            specify an alternative directory for the binaries
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9c2c88eebc..b3bdeae82e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -174,3 +174,20 @@ let load_vernac verb file =
     raw_load_vernac_file verb file
   with e -> 
     raise_with_file file e
+
+(* Compile a vernac file (f is assumed without .v suffix) *)
+let compile verbosely f =
+  try
+    let s = Filename.basename f in
+    let m = Names.id_of_string s in
+    let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in
+    let ldir = (Library.find_logical_path (Filename.dirname longf)) @ [m] in
+    Lib.start_module ldir;
+    load_vernac verbosely longf;
+    let mid = Lib.end_module m in
+    assert (mid = ldir);
+    Library.save_module_to ldir (f^".vo")
+  with e ->
+    raise_with_file f e
+
+
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 1266cd9dd9..da1aa182df 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -33,3 +33,8 @@ val raw_do_vernac : Pcoq.Gram.parsable -> unit
    and location *)
 
 val load_vernac : bool -> string -> unit
+
+
+(* Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
+
+val compile : bool -> string -> unit