- coqc: utilise le meilleur coq possible

- coqc -v réparé
- coqtop: options -byte et -opt


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

5 files changed, 31 insertions, 7 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 456384d906..b0595cf78f 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -51,6 +51,18 @@ let require () =
     (fun s -> Library.require_module None (Filename.basename s) (Some s) false)
     (List.rev !require_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
+   by coqmktop (see scripts/coqmktop.ml). *)
+
+let re_exec s =
+  let is_native = (Mltop.get()) = Mltop.Native in
+  if (is_native && s = "byte") || ((not is_native) && s = "opt") then 
+    let prog = Sys.argv.(0) in
+    let newprog = Filename.concat (Filename.dirname prog) ("coqtop." ^ s) in
+    Sys.argv.(0) <- newprog;
+    Unix.execv newprog Sys.argv
 
 (* Parsing of the command line.
  *
@@ -65,11 +77,7 @@ let usage () =
   flush stderr ;
   exit 1
 
-let version () =
-  Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
-    Coq_config.version Coq_config.date;
-  Printf.printf "compiled on %s\n" Coq_config.compile_date;
-  exit 0
+let warning s = wARNING [< 'sTR s >]
 
 let parse_args () =
   let rec parse = function
@@ -83,6 +91,10 @@ let parse_args () =
 
     | "-q" :: rem -> no_load_rc (); parse rem
 
+    | "-opt" :: rem -> re_exec "opt"; parse rem
+    | "-byte" :: rem -> re_exec "byte"; parse rem
+    | "-full" :: rem -> warning "option -full deprecated\n"; parse rem
+
     | "-batch" :: rem -> set_batch_mode (); parse rem
 	     
     | "-outputstate" :: s :: rem -> set_outputstate s; parse rem
@@ -121,7 +133,7 @@ let parse_args () =
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
-    | ("-v"|"--version") :: _ -> version ()
+    | ("-v"|"--version") :: _ -> Usage.version ()
 
     | "-init-file" :: f :: rem -> set_rcfile f; parse rem
     | "-init-file" :: []       -> usage ()
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 7d0761771e..f255739b30 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -57,6 +57,7 @@ let load = ref Native
 
 (* Sets and initializes the kind of loading *)
 let set kload = load := kload
+let get () = !load
 
 (* Resets load *)
 let remove ()= load := Native
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 817bc0531a..37a71d212c 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -17,6 +17,7 @@ type kind_load=
 
 (*Sets and initializes the kind of loading*)
 val set : kind_load -> unit
+val get : unit -> kind_load
 
 (*Resets the kind of loading*)
 val remove : unit -> unit
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index d5a5a7aec3..dcd845e332 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -1,6 +1,12 @@
 
 (* $Id$ *)
 
+let version () =
+  Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
+    Coq_config.version Coq_config.date;
+  Printf.printf "compiled on %s\n" Coq_config.compile_date;
+  exit 0
+
 (* print the usage of coqtop (or coqc) on channel co *)
 
 let print_usage_channel co command =
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 0cd71ad098..3a4ed2b9b4 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -1,7 +1,11 @@
 
 (* $Id$ *)
 
-(* Prints the usage on the error output. *)
+(*s Prints the version number on the standard output and exits (with 0). *)
+
+val version : unit -> 'a
+
+(*s Prints the usage on the error output. *)
 
 val print_usage_coqtop : unit -> unit
 val print_usage_coqc : unit -> unit