aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqmktop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqmktop.ml')
-rw-r--r--tools/coqmktop.ml335
1 files changed, 173 insertions, 162 deletions
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index b9b67f3e4..95baa8085 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -6,121 +6,145 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* coqmktop is a script to link Coq, analogous to ocamlmktop.
+(** {1 Coqmktop} *)
+
+(** 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). *)
-let (/) = Filename.concat
+(** {6 Utilities} *)
-let safe_sys_command =
- if Sys.os_type = "Win32" then
- fun cmd -> Sys.command ("\""^cmd^"\"")
- else Sys.command
+(** Split a string at each blank
+*)
+let split_list =
+ let spaces = Str.regexp "[ \t\n]+" in
+ fun str -> Str.split spaces str
-(* Objects to link *)
+let (/) = Filename.concat
-(* NB: dynlink is now always linked, it is used for loading plugins
- and compiled vm code (see native-compiler). We now reject platforms
- with ocamlopt but no dynlink.cmxa during ./configure, and give
- instructions there about how to build a dummy dynlink.cmxa,
- cf. dev/dynlink.ml. *)
+(** Which user files do we support (and propagate to ocamlopt) ?
+*)
+let supported_suffix f = match CUnix.get_extension f with
+ | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true
+ | _ -> false
-(* 1. Core objects *)
-let ocamlobjs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
-let camlp4objs =
- if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"]
-let libobjs = ocamlobjs @ camlp4objs
+(** From bytecode extension to native
+*)
+let native_suffix f = match CUnix.get_extension f with
+ | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx"
+ | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa"
+ | ".a" -> f
+ | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a")
-let spaces = Str.regexp "[ \t\n]+"
-let split_list l = Str.split spaces l
+(** Transforms a file name in the corresponding Caml module name.
+*)
+let module_of_file name =
+ String.capitalize
+ (try Filename.chop_extension name with Invalid_argument _ -> name)
-let copts = split_list Tolink.copts
-let core_objs = split_list Tolink.core_objs
-let core_libs = split_list Tolink.core_libs
+(** Run a command [prog] with arguments [args].
+ We do not use [Sys.command] anymore, see comment in [CUnix.sys_command].
+*)
+let run_command prog args =
+ match CUnix.sys_command prog args with
+ | Unix.WEXITED 127 -> failwith ("no such command "^prog)
+ | Unix.WEXITED n -> n
+ | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n)
+ | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n)
-(* 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 *)
+(** {6 Coqmktop options} *)
-(* 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'
+let is_camlp5 = Coq_config.camlp4 = "camlp5"
-(* 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 (/) 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\\)"
+(** {6 Includes options} *)
-let module_of_file name =
- let s = Str.replace_first rem_ext_regexpr "\\1" (Filename.basename name) in
- String.capitalize s
+(** Since the Coq core .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). *)
-(* Build the list of files to link and the list of modules names *)
-let files_to_link userfiles =
- let toplevel_objs =
- if !top then topobjs else if !opt then notopobjs else [] in
- let objs = libobjs @ core_objs @ toplevel_objs in
- let modules = List.map module_of_file (objs @ userfiles)
- in
- let libs = libobjs @ core_libs @ toplevel_objs in
- let libstolink =
- (if !opt then List.map native_suffix libs else libs) @ userfiles
- in
- (modules, libstolink)
+let std_includes basedir =
+ let rebase d = match basedir with None -> d | Some base -> base / d in
+ ["-I"; rebase ".";
+ "-I"; rebase "lib";
+ "-I"; rebase "toplevel";
+ "-I"; rebase "kernel/byterun";
+ "-I"; Envars.camlp4lib () ] @
+ (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
-(* Gives the list of all the directories under [dir]. *)
-let all_subdirs dir =
- let l = ref [] in
- let add f = l := f :: !l in
+(** For the -R option, visit all directories under [dir] and add
+ corresponding -I to the [opts] option list (in reversed order) *)
+let incl_all_subdirs dir opts =
+ let l = ref opts in
+ let add f = l := f :: "-I" :: !l in
let rec traverse dir =
if Sys.file_exists dir && Sys.is_directory dir then
let () = add dir in
- let subdirs = try Sys.readdir dir with _ -> [||] in
+ let subdirs = try Sys.readdir dir with any -> [||] in
Array.iter (fun f -> traverse (dir/f)) subdirs
in
- traverse dir; List.rev !l
+ traverse dir; !l
+
+
+(** {6 Objects to link} *)
+
+(** NB: dynlink is now always linked, it is used for loading plugins
+ and compiled vm code (see native-compiler). We now reject platforms
+ with ocamlopt but no dynlink.cmxa during ./configure, and give
+ instructions there about how to build a dummy dynlink.cmxa,
+ cf. dev/dynlink.ml. *)
+
+(** OCaml + CamlpX libraries *)
+
+let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
+let camlp4_libs = if is_camlp5 then ["gramlib.cma"] else ["camlp4lib.cma"]
+let libobjs = ocaml_libs @ camlp4_libs
+
+(** Toplevel objects *)
+
+let ocaml_topobjs =
+ if is_ocaml4 then
+ ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"]
+ else
+ ["toplevellib.cma"]
+
+let camlp4_topobjs =
+ if is_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 = ocaml_topobjs @ camlp4_topobjs
+
+(** Coq Core objects *)
+
+let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts)
+let core_objs = split_list Tolink.core_objs
+let core_libs = split_list Tolink.core_libs
+
+(** Build the list of files to link and the list of modules names
+*)
+let files_to_link userfiles =
+ let top = if !top then topobjs else [] in
+ let modules = List.map module_of_file (top @ core_objs @ userfiles) in
+ let objs = libobjs @ top @ core_libs in
+ let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles
+ in (modules, objs')
+
+
+(** {6 Parsing of the command-line} *)
-(* usage *)
let usage () =
prerr_endline "Usage: coqmktop <options> <ocaml options> files\
\nFlags are:\
@@ -130,63 +154,56 @@ let usage () =
\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
+
+ (* Directories *)
| "-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 ()
+ | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem
+ | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage ()
+
+ (* Boolean options of coqmktop *)
| "-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
+ | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem
| "-echo" :: rem -> echo := true ; parse (op,fl) rem
+ | ("-v8"|"-full" as o) :: rem ->
+ Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem
+
+ (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *)
+ | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
+ parse (o::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"
- || Filename.check_suffix f ".cmx"
- || Filename.check_suffix f ".cmo"
- || Filename.check_suffix f ".cmxa"
- || Filename.check_suffix f ".cma"
- || 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
+
+ | ("-h"|"-help"|"--help") :: _ -> usage ()
+ | f :: rem when supported_suffix f -> parse (op,f::fl) rem
+ | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1
in
- parse ([Coq_config.osdeplibs],[]) (List.tl (Array.to_list Sys.argv))
+ parse ([],[]) (List.tl (Array.to_list Sys.argv))
+
+(** {6 Temporary main file} *)
+
+(** remove the temporary main file
+*)
let clean file =
let rm f = if Sys.file_exists f then Sys.remove f in
let basename = Filename.chop_suffix file ".ml" in
@@ -198,7 +215,8 @@ let clean file =
rm (basename ^ ".cmx")
end
-(* Initializes the kind of loading in the main program *)
+(** Initializes the kind of loading in the main program
+*)
let declare_loading_string () =
if not !top then
"Mltop.remove ();;"
@@ -216,13 +234,15 @@ let declare_loading_string () =
\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 Errors.error (\"Could not load plugin \"^f));\
+\n (fun f -> if not (Topdirs.load_file ppf f)\
+\n then Errors.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 *)
+(** 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
@@ -233,63 +253,54 @@ let create_tmp_main_file modules =
(* 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";
+ 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 *)
+
+(** {6 Main } *)
+
let main () =
let (options, userfiles) = parse_args () in
+ (* Directories: *)
let () = Envars.set_coqlib ~fail:Errors.error 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 (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 (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 basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
+ (* Which ocaml compiler to invoke *)
+ let prog = camlbin/(if !opt then "ocamlopt" else "ocamlc") in
+ (* Which arguments ? *)
+ if !opt && !top then failwith "no custom toplevel in native code !";
+ let flags = if !opt then [] else Coq_config.vmbyteflags in
+ let topstart = if !top then [ "topstart.cmo" ] else [] in
let (modules, tolink) = files_to_link userfiles in
- (* the list of the loaded modules *)
let main_file = create_tmp_main_file modules in
try
+ (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
+ - With the coq .cma, we MUST use the -linkall option. *)
let args =
- options @ (includes ()) @ copts @ tolink @ [ Filename.quote main_file ]
+ "-linkall" :: "-rectypes" :: flags @ copts @ options @
+ (std_includes basedir) @ tolink @ [ main_file ] @ topstart
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
+ if !echo then begin
+ let command = String.concat " " (prog::args) in
+ print_endline command;
+ print_endline
+ ("(command length is " ^
+ (string_of_int (String.length command)) ^ " characters)");
+ flush Pervasives.stdout
+ end;
+ let exitcode = run_command prog args in
+ clean main_file;
+ exitcode
+ with reraise -> clean main_file; raise reraise
-let retcode =
- try Printexc.print main () with any -> 1
+let pr_exn = function
+ | Failure msg -> msg
+ | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err
+ | any -> Printexc.to_string any
-let _ = exit retcode
+let _ =
+ try exit (main ())
+ with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 21:36:33 +0000