compilation bytecode / native :

 - script de configuration
 - Makefile
 - simplification de coqmktop
 - option -opt de coqc


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

2 files changed, 11 insertions, 13 deletions

diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4
index c4d6468dd7..d0ef0c5ebc 100644
--- a/scripts/coqc.ml4
+++ b/scripts/coqc.ml4
@@ -18,6 +18,7 @@
 let environment = Unix.environment ()
 
 let bindir = ref Coq_config.bindir
+let binary = ref "coqtop.byte"
 
 (* the $COQBIN environment variable has priority over the Coq_config value *)
 let _ = 
@@ -114,6 +115,8 @@ let parse_args () =
 	bindir := d ; parse (cfiles,args) rem
     | "-bindir" :: []       ->
 	usage ()
+    | "-opt" :: rem ->
+	binary := "coqtop.opt"; parse (cfiles,args) rem
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
     | ("-image"|"-libdir"|"-I"|"-R"|"-include"|"-outputstate"|"-inputstate"
       |"-is"|"-load-vernac-source"|"-load-vernac-object"|"-load-ml-source"
@@ -125,7 +128,7 @@ let parse_args () =
 	    | []        -> usage ()
 	end
     | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois"
-      |"-q"|"-opt"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem ->
+      |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem ->
 	parse (cfiles,o::args) rem
     | f :: rem -> 
 	if Sys.file_exists f then
@@ -150,7 +153,7 @@ let main () =
     prerr_endline "coqc: too few arguments" ;
     usage ()
   end;
-  let coqtopname = Filename.concat !bindir "coqtop.byte" in
+  let coqtopname = Filename.concat !bindir !binary in
   List.iter (compile coqtopname args) cfiles
     
 let _ = Printexc.print main (); exit 0
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index a148c7695c..e087271aef 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -49,15 +49,11 @@ let notopobjs = gramobjs
 
 (* 5. High-level tactics objects *)
 let hightactics = split_cmo Tolink.hightactics
-let cmotacsobjs = [
-  "prolog.cmo"; "equality.cmo"; "inv.cmo"; "leminv.cmo"; 
-  "point.cmo"; "progmach.cmo"; "program.cmo"; "propre.cmo";
-  "tauto.cmo"; "gelim.cmo"; "eqdecide.cmo"]
 
 (* environment *)
 let src_coqtop = ref Coq_config.coqtop
-let notactics  = ref false
 let opt        = ref false
+let full       = ref false
 let top        = ref false
 let searchisos = ref false
 let echo       = ref false
@@ -98,10 +94,9 @@ let module_of_file name =
 let files_to_link userfiles =
   let dyn_objs = if not !opt then dynobjs else [] in
   let command_objs = if !searchisos then coqsearch else [] in
-  let tactic_objs = if !notactics then [] else hightactics in
   let toplevel_objs = if !top then topobjs else if !opt then notopobjs else []
   in
-  let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ tactic_objs @
+  let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ hightactics @
     toplevel_objs in
   let tolink =
     if !opt then 
@@ -142,11 +137,11 @@ let usage () =
   prerr_endline "Usage: coqmktop <options> <ocaml options> files
 Options are:
   -srcdir dir   Specify where the Coq source files are
-  -notactics    Do not link high level tactics
   -o exec-file  Specify the name of the resulting toplevel
   -opt          Compile in native code
+  -full         Link high level tactics
   -top          Build Coq on a ocaml toplevel (incompatible with -opt)
-  -searchisos   Build a toplevel for SearchIsos (implies -notactics)
+  -searchisos   Build a toplevel for SearchIsos
   -R dir        Specify recursively directories for Ocaml\n";
   exit 1
 
@@ -156,11 +151,11 @@ let parse_args () =
     | [] -> List.rev op, List.rev fl
     | "-srcdir" :: d :: rem -> src_coqtop := d ; parse (op,fl) rem
     | "-srcdir" :: _        -> usage ()
-    | "-notactics" :: rem -> notactics := true ; parse (op,fl) rem
     | "-opt" :: rem -> opt := true ; parse (op,fl) rem
+    | "-full" :: rem -> full := true ; parse (op,fl) rem
     | "-top" :: rem -> top := true ; parse (op,fl) rem
     | "-searchisos" :: rem ->
-        searchisos := true; notactics := true; parse (op,fl) rem
+        searchisos := true; parse (op,fl) rem
     | "-echo" :: rem -> echo := true ; parse (op,fl) rem
     | ("-cclib"|"-ccopt"|"-I"|"-o" as o) :: rem' ->
 	begin