1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: coqmktop.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
11
(* coqmktop is a script to link Coq, analogous to ocamlmktop.
12
The command line contains options specific to coqmktop, options for the
13
Ocaml linker and files to link (in addition to the default Coq files). *)
20
let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"]
21
let dynobjs = ["dynlink.cma"]
22
let camlp4objs = ["gramlib.cma"]
23
let libobjs = ocamlobjs @ camlp4objs
25
let spaces = Str.regexp "[ \t\n]+"
26
let split_list l = Str.split spaces l
28
let copts = split_list Tolink.copts
29
let core_objs = split_list Tolink.core_objs
30
let core_libs = split_list Tolink.core_libs
31
let ide = split_list Tolink.ide
33
(* 3. Toplevel objects *)
35
if Coq_config.camlp4 = "camlp5" then
36
["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
38
["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
39
let topobjs = camlp4topobjs
42
let notopobjs = gramobjs
44
(* 4. High-level tactics objects *)
50
let searchisos = ref false
51
let coqide = ref false
55
[ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] @
56
if !coqide then [[ "ide" ]] else []
59
let coqlib = Envars.coqlib () in
60
let camlp4lib = Envars.camlp4lib () in
62
(fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
64
(["-I"; "\"" ^ camlp4lib ^ "\""] @
65
["-I"; "\"" ^ coqlib ^ "\""] @
66
(if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
68
(* Transform bytecode object file names in native object file names *)
70
if Filename.check_suffix f ".cmo" then
71
(Filename.chop_suffix f ".cmo") ^ ".cmx"
72
else if Filename.check_suffix f ".cma" then
73
(Filename.chop_suffix f ".cma") ^ ".cmxa"
75
if Filename.check_suffix f ".a" then f
77
failwith ("File "^f^" has not extension .cmo, .cma or .a")
79
(* Transforms a file name in the corresponding Caml module name. *)
80
let rem_ext_regexpr = Str.regexp "\\(.*\\)\\.\\(cm..?\\|ml\\)"
82
let module_of_file name =
83
let s = Str.replace_first rem_ext_regexpr "\\1" (Filename.basename name) in
86
(* Build the list of files to link and the list of modules names *)
87
let files_to_link userfiles =
89
if not !opt || Coq_config.has_natdynlink then dynobjs else [] in
91
if !top then topobjs else if !opt then notopobjs else [] in
92
let ide_objs = if !coqide then
93
"threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide
96
let ide_libs = if !coqide then
97
["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
101
let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs
102
and libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in
103
let objstolink,libstolink =
105
((List.map native_suffix objs) @ userfiles,
106
(List.map native_suffix libs) @ userfiles)
108
(objs @ userfiles, libs @ userfiles )
110
let modules = List.map module_of_file objstolink in
111
(modules, libstolink)
113
(* Gives the list of all the directories under [dir].
114
Uses [Unix] (it is hard to do without it). *)
115
let all_subdirs dir =
117
let add f = l := f :: !l in
118
let rec traverse dir =
120
try opendir dir with Unix_error _ -> invalid_arg "all_subdirs"
124
let f = readdir dirh in
125
if f <> "." && f <> ".." then
126
let file = Filename.concat dir f in
127
if (stat file).st_kind = S_DIR then begin
135
traverse dir; List.rev !l
139
prerr_endline "Usage: coqmktop <options> <ocaml options> files
141
-coqlib dir Specify where the Coq object files are
142
-camlbin dir Specify where the OCaml binaries are
143
-camlp4bin dir Specify where the CAmp4/5 binaries are
144
-o exec-file Specify the name of the resulting toplevel
145
-boot Run in boot mode
146
-opt Compile in native code
147
-full Link high level tactics
148
-top Build Coq on a ocaml toplevel (incompatible with -opt)
149
-searchisos Build a toplevel for SearchIsos
150
-ide Build a toplevel for the Coq IDE
151
-R dir Specify recursively directories for Ocaml\n";
154
(* parsing of the command line *)
156
let rec parse (op,fl) = function
157
| [] -> List.rev op, List.rev fl
158
| "-coqlib" :: d :: rem ->
159
Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
160
| "-coqlib" :: _ -> usage ()
161
| "-camlbin" :: d :: rem ->
162
Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
163
| "-camlbin" :: _ -> usage ()
164
| "-camlp4bin" :: d :: rem ->
165
Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
166
| "-camlp4bin" :: _ -> usage ()
167
| "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
168
| "-opt" :: rem -> opt := true ; parse (op,fl) rem
169
| "-full" :: rem -> full := true ; parse (op,fl) rem
170
| "-top" :: rem -> top := true ; parse (op,fl) rem
172
coqide := true; parse (op,fl) rem
174
Printf.eprintf "warning: option -v8 deprecated";
176
| "-echo" :: rem -> echo := true ; parse (op,fl) rem
177
| ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
180
| a :: rem -> parse (a::o::op,fl) rem
183
| "-R" :: a :: rem ->
184
parse ((List.rev(List.flatten (List.map (fun d -> ["-I";d])
185
(all_subdirs a))))@op,fl) rem
186
| "-R" :: [] -> usage ()
187
| ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
189
| ("-h"|"--help") :: _ -> usage ()
191
if Filename.check_suffix f ".ml"
192
or Filename.check_suffix f ".cmx"
193
or Filename.check_suffix f ".cmo"
194
or Filename.check_suffix f ".cmxa"
195
or Filename.check_suffix f ".cma" then
198
prerr_endline ("Don't know what to do with " ^ f);
202
parse ([Coq_config.osdeplibs],[]) (List.tl (Array.to_list Sys.argv))
205
let rm f = if Sys.file_exists f then Sys.remove f in
206
let basename = Filename.chop_suffix file ".ml" in
207
if not !echo then begin
209
rm (basename ^ ".o");
210
rm (basename ^ ".cmi");
211
rm (basename ^ ".cmo");
212
rm (basename ^ ".cmx")
215
(* Creates another temporary file for Dynlink if needed *)
217
let tmp = Filename.temp_file "coqdynlink" ".ml" in
218
let _ = Sys.command ("echo \"Dynlink.init();;\" > "^tmp) in
221
(* Initializes the kind of loading in the main program *)
222
let declare_loading_string () =
226
"let ppf = Format.std_formatter;;
228
{Mltop.load_obj=Topdirs.dir_load ppf;
229
Mltop.use_file=Topdirs.dir_use ppf;
230
Mltop.add_dir=Topdirs.dir_directory;
231
Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
233
(* create a temporary main file to link *)
234
let create_tmp_main_file modules =
235
let main_name = Filename.temp_file "coqmain" ".ml" in
236
let oc = open_out main_name in
238
(* Add the pre-linked modules *)
239
output_string oc "List.iter Mltop.add_known_module [\"";
240
output_string oc (String.concat "\";\"" modules);
241
output_string oc "\"];;\n";
242
(* Initializes the kind of loading *)
243
output_string oc (declare_loading_string());
244
(* Start the right toplevel loop: Coq or Coq_searchisos *)
246
output_string oc "Cmd_searchisos_line.start();;\n"
248
output_string oc "Coqide.start();;\n"
250
output_string oc "Coqtop.start();;\n";
254
clean main_name; raise e
258
let (options, userfiles) = parse_args () in
259
(* which ocaml command to invoke *)
260
let camlbin = Envars.camlbin () in
264
if !top then failwith "no custom toplevel in native code !";
265
let ocamloptexec = Filename.concat camlbin "ocamlopt" in
266
ocamloptexec^" -linkall"
268
(* bytecode (we shunt ocamlmktop script which fails on win32) *)
269
let ocamlmktoplib = " toplevellib.cma" in
270
let ocamlcexec = Filename.concat camlbin "ocamlc" in
271
let ocamlccustom = Printf.sprintf "%s %s -linkall "
272
ocamlcexec Coq_config.coqrunbyteflags in
273
(if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
276
let (modules, tolink) = files_to_link userfiles in
277
(*file for dynlink *)
279
if not (!opt || !top) then
280
[(print_int 2; tmp_dynlink())]
284
(* the list of the loaded modules *)
285
let main_file = create_tmp_main_file modules in
288
options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in
289
(* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
290
let args = if !top then args @ [ "topstart.cmo" ] else args in
291
(* Now, with the .cma, we MUST use the -linkall option *)
292
let command = String.concat " " (prog::"-rectypes"::args) in
295
print_endline command;
297
("(command length is " ^
298
(string_of_int (String.length command)) ^ " characters)");
299
flush Pervasives.stdout
301
let retcode = Sys.command command in
303
(* command gives the exit code in HSB, and signal in LSB !!! *)
304
if retcode > 255 then retcode lsr 8 else retcode
306
clean main_file; raise e
309
try Printexc.print main () with _ -> 1
added
removed
scripts/coqmktop.ml
