Imported Upstream version 8.5~beta1+dfsg

2 files changed, 0 insertions, 508 deletions

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
deleted file mode 100644
index 8cdac0c5..00000000
--- a/scripts/coqc.ml
+++ /dev/null
@@ -1,189 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Afin de rendre Coq plus portable, ce programme Caml remplace le script
-   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
-   à un process "coqtop -batch -load-vernac-source <fichier>".
-
-   On essaye au maximum d'utiliser les modules Sys et Filename pour que la
-   portabilité soit maximale, mais il reste encore des appels à des fonctions
-   du module Unix. Ceux-ci sont préfixés par "Unix."
-*)
-
-(* environment *)
-
-let environment = Unix.environment ()
-
-let best = if Coq_config.arch = "win32" then "" else ("."^Coq_config.best)
-let binary = ref ("coqtop" ^ best)
-let image = ref ""
-
-(* coqc options *)
-
-let verbose = ref false
-
-(* Verifies that a string starts by a letter and do not contain
-   others caracters than letters, digits, or `_` *)
-
-let check_module_name s =
-  let err c =
-    output_string stderr "Invalid module name: ";
-    output_string stderr s;
-    output_string stderr " character ";
-    if c = '\'' then
-      output_string stderr "\"'\""
-    else
-      (output_string stderr"'"; output_char stderr c; output_string stderr"'");
-    output_string stderr " is not allowed in module names\n";
-    exit 1
-  in
-  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
-	    | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_'  -> ()
-	    | c -> err c
-	done
-    | c -> err c
-
-let rec make_compilation_args = function
-  | [] -> []
-  | file :: fl ->
-      let name_no_suffix =
-        if Filename.check_suffix file ".v" then
-          Filename.chop_suffix file ".v"
-        else
-          file
-      in
-      let modulename = Filename.basename name_no_suffix  in
-      check_module_name modulename;
-      (if !verbose then "-compile-verbose" else "-compile")
-      :: name_no_suffix :: (make_compilation_args fl)
-
-(* compilation of files [files] with command [command] and args [args] *)
-
-let compile command args files =
-  let args' = command :: args @ (make_compilation_args files) in
-  match Sys.os_type with
-  | "Win32" ->
-     let pid =
-        Unix.create_process_env command (Array.of_list args') environment
-        Unix.stdin Unix.stdout Unix.stderr
-     in
-     let status = snd (Unix.waitpid [] pid) in
-     let errcode =
-       match status with Unix.WEXITED c|Unix.WSTOPPED c|Unix.WSIGNALED c -> c
-     in
-     exit errcode
-  | _ ->
-     Unix.execvpe command (Array.of_list args') environment
-
-(* parsing of the command line
- *
- * special treatment for -bindir and -i.
- * other options are passed to coqtop *)
-
-let usage () =
-  Usage.print_usage_coqc () ;
-  flush stderr ;
-  exit 1
-
-let parse_args () =
-  let rec parse (cfiles,args) = function
-    | [] ->
-	List.rev cfiles, List.rev args
-    | ("-verbose" | "--verbose") :: rem ->
-	verbose := true ; parse (cfiles,args) rem
-    | "-image" :: f :: rem ->
-	image := f; parse (cfiles,args) rem
-    | "-image" :: [] ->
-	usage ()
-    | "-byte" :: rem ->
-       binary := "coqtop.byte"; parse (cfiles,args) rem
-    | "-opt" :: rem ->
-       binary := "coqtop.opt"; parse (cfiles,args) rem
-    | "-libdir" :: _ :: rem ->
-        print_string "Warning: option -libdir deprecated and ignored\n"; flush stdout;
-        parse (cfiles,args) rem
-    | ("-db"|"-debugger") :: rem ->
-        print_string "Warning: option -db/-debugger deprecated and ignored\n";flush stdout;
-        parse (cfiles,args) rem
-
-    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
-    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
-      |"-load-vernac-source"|"-l"|"-load-vernac-object"
-      |"-load-ml-source"|"-require"|"-load-ml-object"
-      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem ->
-	begin
-	  match rem with
-	    | s :: rem' -> parse (cfiles,s::o::args) rem'
-	    | []        -> usage ()
-	end
-    | ("-I"|"-include" as o) :: rem ->
-	begin
-	  match rem with
-	  | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem'
-	  | s :: "-as" :: [] -> usage ()
-	  | s :: rem' -> parse (cfiles,s::o::args) rem'
-	  | []        -> usage ()
-	end
-    | "-R" :: s :: "-as" :: t :: rem ->	parse (cfiles,t::"-as"::s::"-R"::args) rem
-    | "-R" :: s :: "-as" :: [] -> usage ()
-    | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
-
-    | ("-notactics"|"-debug"|"-nolib"|"-boot"
-      |"-batch"|"-nois"|"-noglob"|"-no-glob"
-      |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
-      |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
-      |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
-      |"-impredicative-set"|"-vm" as o) :: rem ->
-	parse (cfiles,o::args) rem
-
-    | ("-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 0
-    | f :: rem ->
-	if Sys.file_exists f then
-	  parse (f::cfiles,args) rem
-	else
-	  let fv = f ^ ".v" in
-	  if Sys.file_exists fv then
-	    parse (fv::cfiles,args) rem
-	  else begin
-	    prerr_endline ("coqc: "^f^": no such file or directory") ;
-	    exit 1
-	  end
-  in
-  parse ([],[]) (List.tl (Array.to_list Sys.argv))
-
-(* main: we parse the command line, define the command to compile files
- * and then call the compilation on each file *)
-
-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 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 ()
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
deleted file mode 100644
index eaecda5d..00000000
--- a/scripts/coqmktop.ml
+++ /dev/null
@@ -1,319 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* coqmktop is a script to link Coq, analogous to ocamlmktop.
-   The command line contains options specific to coqmktop, options for the
-   Ocaml linker and files to link (in addition to the default Coq files). *)
-
-open Unix
-
-(* In Win32 outside cygwin, Sys.command calls cmd.exe. When it executes
-   a command that may contains many double-quote, we should double-quote
-   the whole ! *)
-
-let safe_sys_command =
-  if Sys.os_type = "Win32" then
-    fun cmd -> Sys.command ("\""^cmd^"\"")
-  else Sys.command
-
-(* Objects to link *)
-
-(* 1. Core objects *)
-let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"]
-let dynobjs = ["dynlink.cma"]
-let camlp4objs =
-  if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"]
-let libobjs = ocamlobjs @ camlp4objs
-
-let spaces = Str.regexp "[ \t\n]+"
-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
-
-(* 3. Toplevel objects *)
-let camlp4topobjs =
-  if Coq_config.camlp4 = "camlp5" then
-    ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
-  else
-    [ "Camlp4Top.cmo";
-      "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
-      "Camlp4Parsers/Camlp4OCamlParser.cmo";
-      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
-let topobjs = camlp4topobjs
-
-let gramobjs = []
-let notopobjs = gramobjs
-
-(* 4. High-level tactics objects *)
-
-(* environment *)
-let opt        = ref false
-let full       = ref false
-let top        = ref false
-let echo       = ref false
-let no_start   = ref false
-
-let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
-
-(* Since the .cma are given with their relative paths (e.g. "lib/clib.cma"),
-   we only need to include directories mentionned in the temp main ml file
-   below (for accessing the corresponding .cmi). *)
-
-let src_dirs =
-  [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]; ]
-
-let includes () =
-  let coqlib = if !Flags.boot then "." else Envars.coqlib () in
-  let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
-  (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
-  @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
-  @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
-
-(* Transform bytecode object file names in native object file names *)
-let native_suffix f =
-  if Filename.check_suffix f ".cmo" then
-    (Filename.chop_suffix f ".cmo") ^ ".cmx"
-  else if Filename.check_suffix f ".cma" then
-    (Filename.chop_suffix f ".cma") ^ ".cmxa"
-  else
-    if Filename.check_suffix f ".a" then f
-    else
-      failwith ("File "^f^" has not extension .cmo, .cma or .a")
-
-(* Transforms a file name in the corresponding Caml module name. *)
-let rem_ext_regexpr = Str.regexp "\\(.*\\)\\.\\(cm..?\\|ml\\)"
-
-let module_of_file name =
-  let s = Str.replace_first rem_ext_regexpr "\\1" (Filename.basename name) in
-  String.capitalize s
-
-(* Build the list of files to link and the list of modules names *)
-let files_to_link userfiles =
-  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 objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs in
-  let modules = List.map module_of_file (objs @ userfiles)
-  in
-  let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs in
-  let libstolink =
-    (if !opt then List.map native_suffix libs else libs) @ userfiles
-  in
-  (modules, libstolink)
-
-(* Gives the list of all the directories under [dir].
-   Uses [Unix] (it is hard to do without it). *)
-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"
-    in
-    try
-      while true do
-	let f = readdir dirh in
-	if f <> "." && f <> ".." then
-	  let file = Filename.concat dir f in
-	  if (stat file).st_kind = S_DIR then begin
-	    add file;
-	    traverse file
-	  end
-      done
-    with End_of_file ->
-      closedir dirh
-  in
-  traverse dir; List.rev !l
-
-(* usage *)
-let usage () =
-  prerr_endline "Usage: coqmktop <options> <ocaml options> files\
-\nFlags are:\
-\n  -coqlib dir    Specify where the Coq object files are\
-\n  -camlbin dir   Specify where the OCaml binaries are\
-\n  -camlp4bin dir Specify where the Camlp4/5 binaries are\
-\n  -o exec-file   Specify the name of the resulting toplevel\
-\n  -boot          Run in boot mode\
-\n  -echo          Print calls to external commands\
-\n  -full          Link high level tactics\
-\n  -opt           Compile in native code\
-\n  -top           Build Coq on a OCaml toplevel (incompatible with -opt)\
-\n  -R dir         Add recursively dir to OCaml search path\
-\n";
-  exit 1
-
-(* parsing of the command line *)
-let parse_args () =
-  let rec parse (op,fl) = function
-    | [] -> List.rev op, List.rev fl
-    | "-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
-    | "-v8" :: rem ->
-	Printf.eprintf "warning: option -v8 deprecated";
-	parse (op,fl) rem
-    | "-echo" :: rem -> echo := true ; parse (op,fl) rem
-    | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
-	begin
-	  match rem' with
-	    | a :: rem -> parse (a::o::op,fl) rem
-	    | []       -> usage ()
-	end
-    | "-R" :: a :: rem ->
-        parse ((List.rev(List.flatten (List.map (fun d -> ["-I";d])
-					 (all_subdirs a))))@op,fl) rem
-    | "-R" :: [] -> usage ()
-    | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
-        parse (o::op,fl) rem
-    | ("-h"|"--help") :: _ -> usage ()
-    | ("-no-start") :: rem -> no_start:=true; parse (op, fl) rem
-    | f :: rem ->
-	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"
-	  or Filename.check_suffix f ".c" then
-	    parse (op,f::fl) rem
-	else begin
-	  prerr_endline ("Don't know what to do with " ^ f);
-	  exit 1
-	end
-  in
-  parse ([Coq_config.osdeplibs],[]) (List.tl (Array.to_list Sys.argv))
-
-let clean file =
-  let rm f = if Sys.file_exists f then Sys.remove f in
-  let basename = Filename.chop_suffix file ".ml" in
-  if not !echo then begin
-    rm file;
-    rm (basename ^ ".o");
-    rm (basename ^ ".cmi");
-    rm (basename ^ ".cmo");
-    rm (basename ^ ".cmx")
-  end
-
-(* 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
-  tmp
-
-(* Initializes the kind of loading in the main program *)
-let declare_loading_string () =
-  if not !top then
-    "Mltop.remove ();;"
-  else
-    "begin try\
-\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
-\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
-\n         | Toploop.Directive_none f -> f ()\
-\n         | _ -> ()\
-\n       end\
-\n     with\
-\n       | Not_found -> ()\
-\n     end;;\
-\n\
-\n     let ppf = Format.std_formatter;;\
-\n     Mltop.set_top\
-\n       {Mltop.load_obj=\
-\n         (fun f -> if not (Topdirs.load_file ppf f) then Util.error (\"Could not load plugin \"^f));\
-\n        Mltop.use_file=Topdirs.dir_use ppf;\
-\n        Mltop.add_dir=Topdirs.dir_directory;\
-\n        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
-\n"
-
-(* create a temporary main file to link *)
-let create_tmp_main_file modules =
-  let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
-  try
-    (* 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 toplevel loop *)
-    if not !no_start then
-    output_string oc "Coqtop.start();;\n";
-    close_out oc;
-    main_name
-  with reraise ->
-    clean main_name; raise reraise
-
-(* main part *)
-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.quote (Filename.concat camlbin "ocamlopt") in
-        ocamloptexec^" -linkall"
-    end else
-      (* bytecode (we shunt ocamlmktop script which fails on win32) *)
-      let ocamlmktoplib = if is_ocaml4
-	then " ocamlcommon.cma ocamlbytecomp.cma ocamltoplevel.cma"
-	else " toplevellib.cma" in
-      let ocamlcexec = Filename.quote (Filename.concat camlbin "ocamlc") in
-      let ocamlccustom = Printf.sprintf "%s %s -linkall "
-        ocamlcexec Coq_config.coqrunbyteflags in
-      (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
-  in
-  (* files to link *)
-  let (modules, tolink) = files_to_link userfiles in
-  (*file for dynlink *)
-  let dynlink=
-    if not (!opt || !top) then
-      [tmp_dynlink()]
-    else
-      []
-  in
-  (* the list of the loaded modules *)
-  let main_file = create_tmp_main_file modules in
-  try
-    let args = options @ includes () @ copts @ tolink @ dynlink in
-    let args = args @ [ Filename.quote main_file ] in
-      (* 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 *)
-    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 = safe_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 reraise ->
-    clean main_file; raise reraise
-
-let retcode =
-  try Printexc.print main () with any -> 1
-
-let _ = exit retcode