Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

2 files changed, 82 insertions, 111 deletions

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 41fb0803..784e2d51 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqc.ml 10235 2007-10-18 12:25:03Z notin $ *)
+(* $Id: coqc.ml 11749 2009-01-05 14:01:04Z notin $ *)
 
 (* Afin de rendre Coq plus portable, ce programme Caml remplace le script
    coqc. 
@@ -24,17 +24,9 @@
 
 let environment = Unix.environment ()
 
-let bindir = ref Coq_config.bindir
 let binary = ref ("coqtop." ^ Coq_config.best)
 let image = ref ""
 
-(* the $COQBIN environment variable has priority over the Coq_config value *)
-let _ = 
-  try 
-    let c = Sys.getenv "COQBIN" in
-    if c <> "" then bindir := c
-  with Not_found -> ()
-
 (* coqc options *)
 
 let specification = ref false
@@ -116,12 +108,8 @@ let parse_args () =
     | ("-verbose" | "--verbose") :: rem -> 
 	verbose := true ; parse (cfiles,args) rem
     | "-boot" :: rem ->
-	bindir:= Filename.concat Coq_config.coqtop "bin";
+	Flags.boot := true;
 	parse (cfiles, "-boot"::args) rem
-    | "-bindir" :: d :: rem ->
-	bindir := d ; parse (cfiles,args) rem
-    | "-bindir" :: []       ->
-	usage ()
     | "-byte" :: rem ->
 	binary := "coqtop.byte"; parse (cfiles,args) rem
     | "-opt" :: rem ->
@@ -141,7 +129,7 @@ let parse_args () =
     | ("-I"|"-include"|"-outputstate"
       |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
-      |"-init-file"|"-dump-glob" as o) :: rem ->
+      |"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
@@ -150,19 +138,22 @@ let parse_args () =
     | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
 
     | ("-notactics"|"-debug"|"-nolib"
-      | "-debugVM"|"-alltransp"|"-VMno"
+      |"-debugVM"|"-alltransp"|"-VMno"
       |"-batch"|"-nois"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
-      |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" |"-strict-implicit"
-      |"-dont-load-proofs"|"-impredicative-set"|"-vm" 
-      | "-unboxed-values" | "-unboxed-definitions" | "-draw-vm-instr" 
-	  as o) :: rem ->
+      |"-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 ->
 	parse (cfiles,o::args) rem
-    | "-where" :: _ -> 
-	let coqlib = 
-	  try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib 
-	in
-	  print_endline coqlib; exit 0
+	    
+    | ("-where") :: _ -> 
+	(try print_endline (Envars.coqlib ())
+	 with Util.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps));
+	exit 0
+
+    | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
+
     | ("-v"|"--version") :: _ ->
         Usage.version ()
     | f :: rem -> 
@@ -184,14 +175,15 @@ let parse_args () =
 
 let main () =
   let cfiles, args = parse_args () in
-  if cfiles = [] then begin
-    prerr_endline "coqc: too few arguments" ;
-    usage ()
-  end;
-  let coqtopname = 
-    if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension)
-  in
-(*  List.iter (compile coqtopname args) cfiles*)
-  Unix.handle_unix_error (compile coqtopname args) cfiles
+    if cfiles = [] then begin
+      prerr_endline "coqc: too few arguments" ;
+      usage ()
+    end;
+    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 2569b292..9a7d30b1 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqmktop.ml 11380 2008-09-07 12:27:27Z glondu $ *)
+(* $Id: coqmktop.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
 
 (* coqmktop is a script to link Coq, analogous to ocamlmktop.
    The command line contains options specific to coqmktop, options for the
@@ -17,7 +17,7 @@ open Unix
 (* Objects to link *)
 
 (* 1. Core objects *)
-let ocamlobjs = ["unix.cma";"nums.cma"]
+let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"]
 let dynobjs = ["dynlink.cma"]
 let camlp4objs = ["gramlib.cma"]
 let libobjs = ocamlobjs @ camlp4objs
@@ -44,7 +44,6 @@ let notopobjs = gramobjs
 (* 4. High-level tactics objects *)
 
 (* environment *)
-let src_coqtop = ref Coq_config.coqtop
 let opt        = ref false
 let full       = ref false
 let top        = ref false
@@ -57,11 +56,14 @@ let src_dirs () =
   if !coqide then [[ "ide" ]] else []
 
 let includes () = 
-  List.fold_right
-    (fun d l -> "-I" :: List.fold_left Filename.concat !src_coqtop d :: l)
-    (src_dirs ())
-    (["-I"; "\"" ^ Coq_config.camlp4lib ^ "\""] @ 
-     (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
+  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"; "\"" ^ coqlib ^ "\""] @
+	 (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
 
 (* Transform bytecode object file names in native object file names *)
 let native_suffix f =
@@ -83,15 +85,16 @@ let module_of_file name =
 
 (* Build the list of files to link and the list of modules names *)
 let files_to_link userfiles =
-  let dyn_objs = if not !opt then dynobjs else [] in
+  let dyn_objs =
+    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 
-    "str.cma"::"threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
+    "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
   else [] 
   in
   let ide_libs = if !coqide then 
-    ["str.cma" ; "threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
+    ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
      "ide/ide.cma" ]
   else [] 
   in
@@ -135,22 +138,33 @@ let all_subdirs dir =
 let usage () =
   prerr_endline "Usage: coqmktop <options> <ocaml options> files
 Flags.are:
-  -srcdir dir   Specify where the Coq source files are
-  -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
-  -ide          Build a toplevel for the Coq IDE
-  -R dir        Specify recursively directories for Ocaml\n";
+  -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
+  -full          Link high level tactics
+  -top           Build Coq on a ocaml toplevel (incompatible with -opt)
+  -searchisos    Build a toplevel for SearchIsos
+  -ide           Build a toplevel for the Coq IDE
+  -R dir         Specify recursively directories for Ocaml\n";
   exit 1
 
 (* parsing of the command line *)
 let parse_args () =
   let rec parse (op,fl) = function
     | [] -> List.rev op, List.rev fl
-    | "-srcdir" :: d :: rem -> src_coqtop := d ; parse (op,fl) rem
-    | "-srcdir" :: _        -> usage ()
+    | "-coqlib" :: d :: rem -> 
+	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
+    | "-coqlib" :: _        -> usage ()
+    | "-camlbin" :: d :: rem -> 
+	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
+    | "-camlbin" :: _        -> usage ()
+    | "-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
     | "-opt" :: rem -> opt := true ; parse (op,fl) rem
     | "-full" :: rem -> full := true ; parse (op,fl) rem
     | "-top" :: rem -> top := true ; parse (op,fl) rem
@@ -198,59 +212,23 @@ let clean file =
     rm (basename ^ ".cmx")
   end
 
-(* Gives all modules in [dir]. Uses [.cmi] suffixes. Uses [Unix]. *)
-let all_modules_in_dir dir =
-  try
-    let lst = ref []
-    and dh = Unix.opendir dir in
-    try
-      while true do
-	let stg = Unix.readdir dh in
-        if (Filename.check_suffix stg ".cmi") then
-          lst := !lst @ [String.capitalize (Filename.chop_suffix stg ".cmi")]
-      done;
-      []
-    with End_of_file -> 
-      Unix.closedir dh; !lst
-  with Unix.Unix_error (_,"opendir",_) ->
-    failwith ("all_modules_in_dir: directory "^dir^" not found")
-
-(* Gives a part of command line (corresponding to dir) for [extract_crc] *)
-let crc_cmd dir =
-  " -I "^dir^(List.fold_right (fun x y -> " "^x^y) (all_modules_in_dir dir)
-  "")
-
-(* Same as [crc_cmd] but recursively *)
-let rec_crc_cmd dir =
-  List.fold_right (fun x y -> x^y) (List.map crc_cmd (all_subdirs dir)) ""
-
 (* Creates another temporary file for Dynlink if needed *)
 let tmp_dynlink()=
   let tmp = Filename.temp_file "coqdynlink" ".ml" in
   let _ = Sys.command ("echo \"Dynlink.init();;\" > "^tmp) in
-  let _ = Sys.command (Coq_config.camllib^"/extract_crc"^(crc_cmd
-      Coq_config.camllib)^(crc_cmd Coq_config.camlp4lib)^(rec_crc_cmd
-      Coq_config.coqtop)^" >> "^tmp) in
-  let _ = Sys.command ("echo \";;\" >> "^tmp) in
-  let _ = 
-    Sys.command ("echo \"Dynlink.add_available_units crc_unit_list;;\" >> "^
-		 tmp)
-  in
   tmp
 
 (* Initializes the kind of loading in the main program *)
 let declare_loading_string () =
-  if !opt then
-    "Mltop.set Mltop.Native;;\n"
-  else if not !top then
-    "Mltop.set Mltop.WithoutTop;;\n"
+  if not !top then
+    "Mltop.remove ();;"
   else
     "let ppf = Format.std_formatter;;
-     Mltop.set (Mltop.WithTop
+     Mltop.set_top
        {Mltop.load_obj=Topdirs.dir_load ppf;
         Mltop.use_file=Topdirs.dir_use ppf;
         Mltop.add_dir=Topdirs.dir_directory;
-        Mltop.ml_loop=(fun () -> Toploop.loop ppf) });;\n"
+        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
 
 (* create a temporary main file to link *)
 let create_tmp_main_file modules =
@@ -279,16 +257,17 @@ let create_tmp_main_file modules =
 let main () =
   let (options, userfiles) = parse_args () in
   (* which ocaml command to invoke *)
+  let camlbin = Envars.camlbin () in
   let prog =
     if !opt then begin
       (* native code *)
       if !top then failwith "no custom toplevel in native code !";
-      let ocamloptexec = Filename.concat Coq_config.camldir "ocamlopt" in
+      let ocamloptexec = Filename.concat camlbin "ocamlopt" in
         ocamloptexec^" -linkall"
     end else
       (* bytecode (we shunt ocamlmktop script which fails on win32) *)
       let ocamlmktoplib = " toplevellib.cma" in
-      let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in
+      let ocamlcexec = Filename.concat camlbin "ocamlc" in
       let ocamlccustom = Printf.sprintf "%s %s -linkall "
         ocamlcexec Coq_config.coqrunbyteflags in
       (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
@@ -307,22 +286,22 @@ let main () =
   try
     let args =
       options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in
-    (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
+      (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
     let args = if !top then args @ [ "topstart.cmo" ] else args in
-    (* Now, with the .cma, we MUST use the -linkall option *)
+      (* 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 " ^ 
-	   (string_of_int (String.length command)) ^ " characters)");
-	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 
+      if !echo then 
+	begin 
+	  print_endline command; 
+	  print_endline 
+	    ("(command length is " ^ 
+	       (string_of_int (String.length command)) ^ " characters)");
+	  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 -> 
     clean main_file; raise e