diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqc.ml | 54 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 108 |
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 = |