Imported Upstream snapshot 8.3~beta0+13298

2 files changed, 85 insertions, 77 deletions

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 69357b2f..61f13d4d 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqc.ml 12911 2010-04-09 10:08:37Z herbelin $ *)
+(* $Id$ *)
 
 (* Afin de rendre Coq plus portable, ce programme Caml remplace le script
-   coqc. 
+   coqc.
 
    Ici, on trie la ligne de commande pour en extraire les fichiers à compiler,
    puis on les compile un par un en passant le reste de la ligne de commande
@@ -24,7 +24,8 @@
 
 let environment = Unix.environment ()
 
-let binary = ref ("coqtop." ^ Coq_config.best)
+let best = if Coq_config.arch = "win32" then "" else ("."^Coq_config.best)
+let binary = ref ("coqtop" ^ best)
 let image = ref ""
 
 (* coqc options *)
@@ -46,12 +47,12 @@ let check_module_name s =
     else
       (output_string stderr"'"; output_char stderr c; output_string stderr"'");
     output_string stderr " is not allowed in module names\n";
-    exit 1 
+    exit 1
   in
-  match String.get s 0 with 
-    | 'a' .. 'z' | 'A' .. 'Z' -> 
+  match String.get s 0 with
+    | 'a' .. 'z' | 'A' .. 'Z' ->
 	for i = 1 to (String.length s)-1 do
-	  match String.get s i with 
+	  match String.get s i with
 	    | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_'  -> ()
 	    | c -> err c
 	done
@@ -59,7 +60,7 @@ let check_module_name s =
 
 let rec make_compilation_args = function
   | [] -> []
-  | file :: fl -> 
+  | file :: fl ->
       let dirname = Filename.dirname file in
       let basename = Filename.basename file in
       let modulename =
@@ -78,14 +79,14 @@ let rec make_compilation_args = function
 let compile command args files =
   let args' = command :: args @ (make_compilation_args files) in
   match Sys.os_type with
-  | "Win32" -> 
-     let pid = 
+  | "Win32" ->
+     let pid =
         Unix.create_process_env command (Array.of_list args') environment
-        Unix.stdin Unix.stdout Unix.stderr 
+        Unix.stdin Unix.stdout Unix.stderr
      in
      ignore (Unix.waitpid [] pid)
   | _ ->
-     Unix.execvpe command (Array.of_list args') environment 
+     Unix.execvpe command (Array.of_list args') environment
 
 (* parsing of the command line
  *
@@ -99,13 +100,13 @@ let usage () =
 
 let parse_args () =
   let rec parse (cfiles,args) = function
-    | [] -> 
+    | [] ->
 	List.rev cfiles, List.rev args
-    | "-i" :: rem -> 
+    | "-i" :: rem ->
 	specification := true ; parse (cfiles,args) rem
-    | "-t" :: rem -> 
+    | "-t" :: rem ->
 	keep := true ; parse (cfiles,args) rem
-    | ("-verbose" | "--verbose") :: rem -> 
+    | ("-verbose" | "--verbose") :: rem ->
 	verbose := true ; parse (cfiles,args) rem
     | "-boot" :: rem ->
 	Flags.boot := true;
@@ -129,7 +130,7 @@ let parse_args () =
     | ("-outputstate"|"-inputstate"|"-is"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
-      |"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem ->
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
@@ -149,15 +150,14 @@ let parse_args () =
 
     | ("-notactics"|"-debug"|"-nolib"
       |"-debugVM"|"-alltransp"|"-VMno"
-      |"-batch"|"-nois"
+      |"-batch"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-impredicative-set"|"-vm"
-      |"-unboxed-values"|"-unboxed-definitions"|"-draw-vm-instr"
-      |"-no-glob"|"-noglob" as o) :: rem ->
+      |"-unboxed-values"|"-unboxed-definitions"|"-draw-vm-instr" as o) :: rem ->
 	parse (cfiles,o::args) rem
-	    
-    | ("-where") :: _ -> 
+
+    | ("-where") :: _ ->
 	(try print_endline (Envars.coqlib ())
 	 with Util.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps));
 	exit 0
@@ -166,10 +166,10 @@ let parse_args () =
 
     | ("-v"|"--version") :: _ ->
         Usage.version ()
-    | f :: rem -> 
+    | f :: rem ->
 	if Sys.file_exists f then
 	  parse (f::cfiles,args) rem
-	else 
+	else
 	  let fv = f ^ ".v" in
 	  if Sys.file_exists fv then
 	    parse (fv::cfiles,args) rem
@@ -189,11 +189,11 @@ let main () =
       prerr_endline "coqc: too few arguments" ;
       usage ()
     end;
-    let coqtopname = 
-      if !image <> "" then !image 
+    let coqtopname =
+      if !image <> "" then !image
       else Filename.concat (Envars.coqbin ()) (!binary ^ Coq_config.exec_extension)
     in
       (*  List.iter (compile coqtopname args) cfiles*)
       Unix.handle_unix_error (compile coqtopname args) cfiles
-    
+
 let _ = Printexc.print main (); exit 0
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index ee8ef1d9..bd21c1c5 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqmktop.ml 12874 2010-03-19 23:15:52Z herbelin $ *)
+(* $Id$ *)
 
 (* coqmktop is a script to link Coq, analogous to ocamlmktop.
    The command line contains options specific to coqmktop, options for the
@@ -28,7 +28,7 @@ let split_list l = Str.split spaces l
 let copts     = split_list Tolink.copts
 let core_objs = split_list Tolink.core_objs
 let core_libs = split_list Tolink.core_libs
-let ide       = split_list Tolink.ide 
+let ide       = split_list Tolink.ide
 
 (* 3. Toplevel objects *)
 let camlp4topobjs =
@@ -51,28 +51,28 @@ let searchisos = ref false
 let coqide     = ref false
 let echo       = ref false
 
-let src_dirs () = 
+let src_dirs () =
   [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] @
   if !coqide then [[ "ide" ]] else []
 
-let includes () = 
+let includes () =
   let coqlib = Envars.coqlib () in
   let camlp4lib = Envars.camlp4lib () in
     List.fold_right
       (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
       (src_dirs ())
-      (["-I"; "\"" ^ camlp4lib ^ "\""] @ 
+      (["-I"; "\"" ^ camlp4lib ^ "\""] @
 	 ["-I"; "\"" ^ coqlib ^ "\""] @
 	 (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
 
 (* Transform bytecode object file names in native object file names *)
 let native_suffix f =
-  if Filename.check_suffix f ".cmo" then 
+  if Filename.check_suffix f ".cmo" then
     (Filename.chop_suffix f ".cmo") ^ ".cmx"
-  else if Filename.check_suffix f ".cma" then 
+  else if Filename.check_suffix f ".cma" then
     (Filename.chop_suffix f ".cma") ^ ".cmxa"
-  else  
-    if Filename.check_suffix f ".a" then f 
+  else
+    if Filename.check_suffix f ".a" then f
     else
       failwith ("File "^f^" has not extension .cmo, .cma or .a")
 
@@ -89,25 +89,21 @@ let files_to_link userfiles =
     if not !opt || Coq_config.has_natdynlink then dynobjs else [] in
   let toplevel_objs =
     if !top then topobjs else if !opt then notopobjs else [] in
-  let ide_objs = if !coqide then 
-    "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
-  else [] 
+  let ide_objs =
+    if !coqide then "Threads"::"Lablgtk"::"GtkThread"::ide else []
+  in
+  let ide_libs =
+    if !coqide then
+      ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide/ide.cma" ]
+    else []
   in
-  let ide_libs = if !coqide then 
-    ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
-     "ide/ide.cma" ]
-  else [] 
+  let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs in
+  let modules = List.map module_of_file (objs @ userfiles)
   in
-  let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs
-  and libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in
-  let objstolink,libstolink =
-    if !opt then 
-      ((List.map native_suffix objs) @ userfiles,
-       (List.map native_suffix libs) @ userfiles)
-    else 
-      (objs @ userfiles, libs @ userfiles )
+  let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in
+  let libstolink =
+    (if !opt then List.map native_suffix libs else libs) @ userfiles
   in
-  let modules = List.map module_of_file objstolink in
   (modules, libstolink)
 
 (* Gives the list of all the directories under [dir].
@@ -116,8 +112,8 @@ let all_subdirs dir =
   let l = ref [dir] in
   let add f = l := f :: !l in
   let rec traverse dir =
-    let dirh = 
-      try opendir dir with Unix_error _ -> invalid_arg "all_subdirs" 
+    let dirh =
+      try opendir dir with Unix_error _ -> invalid_arg "all_subdirs"
     in
     try
       while true do
@@ -137,17 +133,18 @@ let all_subdirs dir =
 (* usage *)
 let usage () =
   prerr_endline "Usage: coqmktop <options> <ocaml options> files
-Flags.are:
+Flags are:
   -coqlib dir    Specify where the Coq object files are
   -camlbin dir   Specify where the OCaml binaries are
   -camlp4bin dir Specify where the CAmp4/5 binaries are
   -o exec-file   Specify the name of the resulting toplevel
   -boot          Run in boot mode
-  -opt           Compile in native code
+  -echo          Print calls to external commands
+  -ide           Build a toplevel for the Coq IDE
   -full          Link high level tactics
-  -top           Build Coq on a ocaml toplevel (incompatible with -opt)
+  -opt           Compile in native code
   -searchisos    Build a toplevel for SearchIsos
-  -ide           Build a toplevel for the Coq IDE
+  -top           Build Coq on a OCaml toplevel (incompatible with -opt)
   -R dir         Specify recursively directories for Ocaml\n";
   exit 1
 
@@ -155,13 +152,13 @@ Flags.are:
 let parse_args () =
   let rec parse (op,fl) = function
     | [] -> List.rev op, List.rev fl
-    | "-coqlib" :: d :: rem -> 
+    | "-coqlib" :: d :: rem ->
 	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
     | "-coqlib" :: _        -> usage ()
-    | "-camlbin" :: d :: rem -> 
+    | "-camlbin" :: d :: rem ->
 	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
     | "-camlbin" :: _        -> usage ()
-    | "-camlp4bin" :: d :: rem -> 
+    | "-camlp4bin" :: d :: rem ->
 	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
     | "-camlp4bin" :: _        -> usage ()
     | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
@@ -170,7 +167,7 @@ let parse_args () =
     | "-top" :: rem -> top := true ; parse (op,fl) rem
     | "-ide" :: rem ->
         coqide := true; parse (op,fl) rem
-    | "-v8" :: rem -> 
+    | "-v8" :: rem ->
 	Printf.eprintf "warning: option -v8 deprecated";
 	parse (op,fl) rem
     | "-echo" :: rem -> echo := true ; parse (op,fl) rem
@@ -188,8 +185,8 @@ let parse_args () =
         parse (o::op,fl) rem
     | ("-h"|"--help") :: _ -> usage ()
     | f :: rem ->
-	if Filename.check_suffix f ".ml" 
-	  or Filename.check_suffix f ".cmx" 
+	if Filename.check_suffix f ".ml"
+	  or Filename.check_suffix f ".cmx"
 	  or Filename.check_suffix f ".cmo"
 	  or Filename.check_suffix f ".cmxa"
 	  or Filename.check_suffix f ".cma" then
@@ -223,9 +220,20 @@ let declare_loading_string () =
   if not !top then
     "Mltop.remove ();;"
   else
-    "let ppf = Format.std_formatter;;
+    "begin try
+       (* Enable rectypes in the toplevel if it has the directive #rectypes *)
+       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with
+         | Toploop.Directive_none f -> f ()
+         | _ -> ()
+       end
+     with
+       | Not_found -> ()
+     end;;
+
+     let ppf = Format.std_formatter;;
      Mltop.set_top
-       {Mltop.load_obj=Topdirs.dir_load ppf;
+       {Mltop.load_obj=
+         (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
         Mltop.use_file=Topdirs.dir_use ppf;
         Mltop.add_dir=Topdirs.dir_directory;
         Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
@@ -235,14 +243,14 @@ let create_tmp_main_file modules =
   let main_name = Filename.temp_file "coqmain" ".ml" in
   let oc = open_out main_name in
   try
-    (* Add the pre-linked modules *)    
+    (* Add the pre-linked modules *)
     output_string oc "List.iter Mltop.add_known_module [\"";
     output_string oc (String.concat "\";\"" modules);
     output_string oc "\"];;\n";
     (* Initializes the kind of loading *)
     output_string oc (declare_loading_string());
     (* Start the right toplevel loop: Coq or Coq_searchisos *)
-    if !searchisos then 
+    if !searchisos then
       output_string oc "Cmd_searchisos_line.start();;\n"
     else if !coqide then
       output_string oc "Coqide.start();;\n"
@@ -250,7 +258,7 @@ let create_tmp_main_file modules =
       output_string oc "Coqtop.start();;\n";
     close_out oc;
     main_name
-  with e -> 
+  with e ->
     clean main_name; raise e
 
 (* main part *)
@@ -290,19 +298,19 @@ let main () =
     let args = if !top then args @ [ "topstart.cmo" ] else args in
       (* Now, with the .cma, we MUST use the -linkall option *)
     let command = String.concat " " (prog::"-rectypes"::args) in
-      if !echo then 
-	begin 
-	  print_endline command; 
-	  print_endline 
-	    ("(command length is " ^ 
+      if !echo then
+	begin
+	  print_endline command;
+	  print_endline
+	    ("(command length is " ^
 	       (string_of_int (String.length command)) ^ " characters)");
-	  flush Pervasives.stdout 
+	  flush Pervasives.stdout
 	end;
       let retcode = Sys.command command in
 	clean main_file;
 	(* command gives the exit code in HSB, and signal in LSB !!! *)
-	if retcode > 255 then retcode lsr 8 else retcode 
-  with e -> 
+	if retcode > 255 then retcode lsr 8 else retcode
+  with e ->
     clean main_file; raise e
 
 let retcode =