diff options
Diffstat (limited to 'scripts/coqmktop.ml')
| -rw-r--r-- | scripts/coqmktop.ml | 357 |
1 files changed, 357 insertions, 0 deletions
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 *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: coqmktop.ml,v 1.28.2.1 2004/07/16 19:30:50 herbelin Exp $ *) + +(* 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 + +(* Objects to link *) + +(* 1. Core objects *) +let ocamlobjs = ["unix.cma"] +let dynobjs = ["dynlink.cma"] +let camlp4objs = [(*"odyl.cma"; "camlp4.cma";*) "gramlib.cma"] +let configobjs = ["coq_config.cmo"] +let libobjs = ocamlobjs @ camlp4objs @ configobjs + +let spaces = Str.regexp "[ \t\n]+" +let split_cmo l = Str.split spaces l + +let lib = split_cmo Tolink.lib +let kernel = split_cmo Tolink.kernel +let library = split_cmo Tolink.library +let pretyping = split_cmo Tolink.pretyping +let interp = split_cmo Tolink.interp +let parsing = split_cmo Tolink.parsing +let proofs = split_cmo Tolink.proofs +let tactics = split_cmo Tolink.tactics +let toplevel = split_cmo Tolink.toplevel +let highparsing = split_cmo Tolink.highparsing +let highparsingnew = split_cmo Tolink.highparsingnew +let ide = split_cmo Tolink.ide + +let core_objs = + libobjs @ lib @ kernel @ library @ pretyping @ interp @ parsing @ + proofs @ tactics + +let core_libs = + libobjs @ [ "lib/lib.cma" ; "kernel/kernel.cma" ; "library/library.cma" ; + "pretyping/pretyping.cma" ; "interp/interp.cma" ; "parsing/parsing.cma" ; + "proofs/proofs.cma" ; "tactics/tactics.cma" ] + +(* 3. Files only in coqsearchisos (if option -searchisos is used) *) +let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"] + +(* 4. Toplevel objects *) +let camlp4objs = + ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; "q_util.cmo"; "q_coqast.cmo" ] +let topobjs = camlp4objs + +let gramobjs = [] +let notopobjs = gramobjs + +(* 5. High-level tactics objects *) +let hightactics = + (split_cmo Tolink.hightactics) @ (split_cmo Tolink.contrib) + +(* environment *) +let src_coqtop = ref Coq_config.coqtop +let opt = ref false +let full = ref false +let top = ref false +let searchisos = ref false +let coqide = ref false +let echo = ref false + +let src_dirs () = + [ []; [ "config" ]; [ "toplevel" ] ] @ + 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 [])) + +(* 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 <options> <ocaml options> 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 |