diff options
Diffstat (limited to 'scripts/coqmktop.ml')
| -rw-r--r-- | scripts/coqmktop.ml | 166 |
1 files changed, 83 insertions, 83 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index c7596d83..b75984e3 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -1,25 +1,33 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqmktop.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* 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 = ["gramlib.cma"] +let camlp4objs = + if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"] let libobjs = ocamlobjs @ camlp4objs let spaces = Str.regexp "[ \t\n]+" @@ -28,14 +36,16 @@ 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 (* 3. Toplevel objects *) let camlp4topobjs = if Coq_config.camlp4 = "camlp5" then ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] else - ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] + [ "Camlp4Top.cmo"; + "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo"; + "Camlp4Parsers/Camlp4OCamlParser.cmo"; + "Camlp4Parsers/Camlp4GrammarParser.cmo" ] let topobjs = camlp4topobjs let gramobjs = [] @@ -47,23 +57,24 @@ let notopobjs = gramobjs 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 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 () = - [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] @ - if !coqide then [[ "ide" ]] else [] +let src_dirs = + [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]; ] 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"; "\"" ^ coqlib ^ "\""] @ - (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else [])) + 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 = @@ -89,18 +100,10 @@ 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"::"Lablgtk"::"GtkThread"::ide else [] - in - let ide_libs = - if !coqide then - ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide/ide.cma" ] - else [] - in - let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs 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 @ ide_libs 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 @@ -132,20 +135,19 @@ let all_subdirs dir = (* usage *) let usage () = - prerr_endline "Usage: coqmktop <options> <ocaml options> files -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 - -echo Print calls to external commands - -ide Build a toplevel for the Coq IDE - -full Link high level tactics - -opt Compile in native code - -searchisos Build a toplevel for SearchIsos - -top Build Coq on a OCaml toplevel (incompatible with -opt) - -R dir Specify recursively directories for Ocaml\n"; + 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 *) @@ -165,8 +167,6 @@ let parse_args () = | "-opt" :: rem -> opt := true ; parse (op,fl) rem | "-full" :: rem -> full := true ; parse (op,fl) rem | "-top" :: rem -> top := true ; parse (op,fl) rem - | "-ide" :: rem -> - coqide := true; parse (op,fl) rem | "-v8" :: rem -> Printf.eprintf "warning: option -v8 deprecated"; parse (op,fl) rem @@ -184,12 +184,14 @@ let parse_args () = | ("-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" then + 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); @@ -220,28 +222,28 @@ let declare_loading_string () = if not !top then "Mltop.remove ();;" else - "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= - (fun f -> if not (Topdirs.load_file ppf f) then Util.error (\"Could not load plugin \"^f));\ - Mltop.use_file=Topdirs.dir_use ppf; - Mltop.add_dir=Topdirs.dir_directory; - Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n" + "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 = Filename.temp_file "coqmain" ".ml" in - let oc = open_out main_name in + 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 [\""; @@ -249,17 +251,13 @@ let create_tmp_main_file 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"; + (* Start the toplevel loop *) + if not !no_start then + output_string oc "Coqtop.start();;\n"; close_out oc; main_name - with e -> - clean main_name; raise e + with reraise -> + clean main_name; raise reraise (* main part *) let main () = @@ -270,12 +268,14 @@ let main () = if !opt then begin (* native code *) if !top then failwith "no custom toplevel in native code !"; - let ocamloptexec = Filename.concat camlbin "ocamlopt" in + let ocamloptexec = Filename.quote (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 camlbin "ocamlc" in + 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) @@ -292,8 +292,8 @@ let main () = (* the list of the loaded modules *) let main_file = create_tmp_main_file modules in try - let args = - options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in + 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 *) @@ -306,14 +306,14 @@ let main () = (string_of_int (String.length command)) ^ " characters)"); flush Pervasives.stdout end; - let retcode = Sys.command command in + 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 e -> - clean main_file; raise e + with reraise -> + clean main_file; raise reraise let retcode = - try Printexc.print main () with _ -> 1 + try Printexc.print main () with any -> 1 let _ = exit retcode |