- 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

9 files changed, 39 insertions, 11 deletions

diff --git a/TODO b/TODO
index 1067e1cc6a..df0a2b0a74 100644
--- a/TODO
+++ b/TODO
@@ -1,8 +1,6 @@
 Distribution:
 
 - faire une passe sur les options de coqtop et coqc
-- option -byte à coqtop
-- coqc utilise coqtop.opt par défaut, sauf si -byte indiqué
 
 Environnement:
 
diff --git a/config/coq_config.mli b/config/coq_config.mli
index b7731b8ab2..d896d6175e 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -12,6 +12,7 @@ val camllib : string    (* for Dynlink *)
 
 val camlp4lib : string  (* where is the library of Camlp4 *)
 
+val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
 val osdeplibs : string  (* OS dependant link options for ocamlc *)
 
diff --git a/configure b/configure
index bc3f8c0707..d05521b7ff 100755
--- a/configure
+++ b/configure
@@ -451,6 +451,7 @@ let coqlib = "$LIBDIR"
 let coqtop = "$COQTOP"
 let camllib = "$CAMLLIB"
 let camlp4lib = "$CAMLP4LIB"
+let best = "$best_compiler"
 let arch = "$ARCH"
 let osdeplibs = "$OSDEPLIBS"
 let defined = [ "$OSTYPE" ]
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 85cea9606b..adc5212324 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -18,7 +18,7 @@
 let environment = Unix.environment ()
 
 let bindir = ref Coq_config.bindir
-let binary = ref "coqtop.byte"
+let binary = ref ("coqtop." ^ Coq_config.best)
 
 (* the $COQBIN environment variable has priority over the Coq_config value *)
 let _ = 
@@ -133,8 +133,12 @@ let parse_args () =
 	end
     | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
-      |"-silent"|"-v"|"--version" as o) :: rem ->
+      |"-silent" as o) :: rem ->
 	parse (cfiles,o::args) rem
+    | ("-v"|"--version") :: _ ->
+        Usage.version ()
+    | "-where" :: _ -> 
+	print_endline Coq_config.coqlib; exit 0
     | f :: rem -> 
 	if Sys.file_exists f then
 	  parse (f::cfiles,args) rem
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