From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- scripts/coqc.ml | 182 +++++++++++++++++++++++++++ scripts/coqmktop.ml | 357 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 539 insertions(+) create mode 100644 scripts/coqc.ml create mode 100644 scripts/coqmktop.ml (limited to 'scripts') diff --git a/scripts/coqc.ml b/scripts/coqc.ml new file mode 100644 index 00000000..7d1cc206 --- /dev/null +++ b/scripts/coqc.ml @@ -0,0 +1,182 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ". + + 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 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 +let keep = ref false +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 dirname = Filename.dirname file in + let basename = Filename.basename file in + let modulename = + if Filename.check_suffix basename ".v" then + Filename.chop_suffix basename ".v" + else + basename + in + check_module_name modulename; + let file = Filename.concat dirname modulename in + (if !verbose then "-compile-verbose" else "-compile") + :: file :: (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 + ignore (Unix.waitpid [] pid) + | _ -> + 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 + | "-i" :: rem -> + specification := true ; parse (cfiles,args) rem + | "-t" :: rem -> + keep := true ; parse (cfiles,args) rem + | ("-verbose" | "--verbose") :: rem -> + verbose := true ; parse (cfiles,args) rem + | "-boot" :: rem -> + bindir:= Filename.concat Coq_config.coqtop "bin"; + 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 -> + binary := "coqtop.opt"; parse (cfiles,args) rem + | "-image" :: f :: rem -> + image := f; parse (cfiles,args) rem + | "-image" :: [] -> + usage () + | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () + | ("-libdir"|"-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 -> + begin + match rem with + | s :: rem' -> parse (cfiles,s::o::args) rem' + | [] -> usage () + end + | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem + | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" + |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" + |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate"|"-strict-implicit" + |"-dont-load-proofs"|"-impredicative-set" as o) :: rem -> + parse (cfiles,o::args) rem + | ("-v"|"--version") :: _ -> + Usage.version () + | "-where" :: _ -> + print_endline Coq_config.coqlib; exit 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 !bindir (!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 new file mode 100644 index 00000000..78306877 --- /dev/null +++ b/scripts/coqmktop.ml @@ -0,0 +1,357 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "-I" :: List.fold_left Filename.concat !src_coqtop d :: l) + (src_dirs ()) + (["-I"; Coq_config.camlp4lib] @ + (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 + (Filename.chop_suffix f ".cmo") ^ ".cmx" + else if Filename.check_suffix f ".cma" then + (Filename.chop_suffix f ".cma") ^ ".cmxa" + else + failwith ("File "^f^" has not extension .cmo or .cma") + +(* 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 then dynobjs else [] in + let command_objs = if !searchisos then coqsearch 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 + else [] + in + let ide_libs = if !coqide then + ["str.cma" ; "threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; + "ide/ide.cma" ] + else [] + in + let objs = + core_objs @ dyn_objs @ toplevel @ highparsing @ highparsingnew @ + command_objs @ hightactics @ toplevel_objs @ ide_objs + and libs = + core_libs @ dyn_objs @ + [ "toplevel/toplevel.cma" ; "parsing/highparsing.cma" ; + "parsing/highparsingnew.cma" ] @ + command_objs @ [ "tactics/hightactics.cma" ; "contrib/contrib.cma" ] @ + 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 ) + in + let modules = List.map module_of_file objstolink 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 files +Options 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 + -v8 Link with V8 grammar\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 () + | "-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; parse (op,fl) rem + | "-ide" :: rem -> + coqide := true; parse (op,fl) rem + | "-v8" :: rem -> parse (op,fl) rem + | "-echo" :: rem -> echo := true ; parse (op,fl) rem + | ("-cclib"|"-ccopt"|"-I"|"-o" 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 () + | ("-compact"|"-g"|"-p"|"-thread" as o) :: rem -> parse (o::op,fl) rem + | ("-h"|"--help") :: _ -> usage () + | 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" 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 + +(* Gives all modules in [dir]. Uses [.cmi] suffixes. Uses [Unix]. *) +let all_modules_in_dir dir = + try + let lst = ref [] + and stg = 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" + else + "let ppf = Format.std_formatter;; + Mltop.set (Mltop.WithTop + {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" + +(* create a temporary main file to link *) +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 *) + 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 + output_string oc "Cmd_searchisos_line.start();;\n" + else if !coqide then + output_string oc "Coqide.start();;\n" + else + output_string oc "Coqtop.start();;\n"; + close_out oc; + main_name + with e -> + clean main_name; raise e + +(* main part *) +let main () = + let (options, userfiles) = parse_args () in + (* which ocaml command to invoke *) + let prog = + if !opt then begin + (* native code *) + if !top then failwith "no custom toplevel in native code !"; + "ocamlopt -linkall" + end else + (* bytecode (we shunt ocamlmktop script which fails on win32) *) + let ocamlmktoplib = " toplevellib.cma" in + let ocamlccustom = "ocamlc -custom -linkall" 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 ()) @ tolink @ dynlink @ [ 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^" -linkall")::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 + with e -> + clean main_file; raise e + +let retcode = + try Printexc.print main () with _ -> 1 + +let _ = exit retcode -- cgit v1.2.3