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

4 files changed, 41 insertions, 2 deletions

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