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: coqtop.ml 11830 2009-01-22 06:45:13Z notin $ *)
22
let get_version_date () =
24
let coqlib = Envars.coqlib () in
25
let ch = open_in (Filename.concat coqlib "revision") in
26
let ver = input_line ch in
27
let rev = input_line ch in
29
with _ -> (Coq_config.version,Coq_config.date)
32
let (ver,rev) = (get_version_date ()) in
33
Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
36
let output_context = ref false
38
let memory_stat = ref false
40
let print_memory_stat () =
42
Format.printf "total heap size = %d kbytes\n" (heap_size_kb ())
44
let _ = at_exit print_memory_stat
46
let engagement = ref None
47
let set_engagement c = engagement := Some c
49
match !engagement with Some c -> Global.set_engagement c | None -> ()
51
let set_batch_mode () = batch_mode := true
53
let toplevel_default_name = make_dirpath [id_of_string "Top"]
54
let toplevel_name = ref (Some toplevel_default_name)
55
let set_toplevel_name dir =
56
if dir = empty_dirpath then error "Need a non empty toplevel module name";
57
toplevel_name := Some dir
58
let unset_toplevel_name () = toplevel_name := None
60
let remove_top_ml () = Mltop.remove ()
62
let inputstate = ref None
63
let set_inputstate s = inputstate:= Some s
65
match !inputstate with
67
| Some s -> intern_state s
68
| None -> intern_state "initial.coq"
70
let outputstate = ref ""
71
let set_outputstate s = outputstate:=s
72
let outputstate () = if !outputstate <> "" then extern_state !outputstate
74
let set_default_include d = push_include (d,Nameops.default_root_prefix)
75
let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix)
77
let p = dirpath_of_string p in
78
Library.check_coq_overwriting p;
80
let set_rec_include d p =
81
let p = dirpath_of_string p in
82
Library.check_coq_overwriting p;
85
let load_vernacular_list = ref ([] : (string * bool) list)
86
let add_load_vernacular verb s =
87
load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list
88
let load_vernacular () =
91
if Flags.do_beautify () then
92
with_option beautify_file (Vernac.load_vernac b) s
94
Vernac.load_vernac b s)
95
(List.rev !load_vernacular_list)
97
let load_vernacular_obj = ref ([] : string list)
98
let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
99
let load_vernac_obj () =
100
List.iter (fun f -> Library.require_library_from_file None f None)
101
(List.rev !load_vernacular_obj)
103
let require_list = ref ([] : string list)
104
let add_require s = require_list := s :: !require_list
106
List.iter (fun s -> Library.require_library_from_file None s (Some false))
107
(List.rev !require_list)
109
let compile_list = ref ([] : (bool * string) list)
110
let add_compile verbose s =
112
Flags.make_silent true;
113
compile_list := (verbose,s) :: !compile_list
114
let compile_files () =
115
let init_state = States.freeze() in
116
let coqdoc_init_state = Dumpglob.coqdoc_freeze () in
119
States.unfreeze init_state;
120
Dumpglob.coqdoc_unfreeze coqdoc_init_state;
121
if Flags.do_beautify () then
122
with_option beautify_file (Vernac.compile v) f
125
(List.rev !compile_list)
127
let re_exec_version = ref ""
128
let set_byte () = re_exec_version := "byte"
129
let set_opt () = re_exec_version := "opt"
131
(* Re-exec Coq in bytecode or native code if necessary. [s] is either
132
["byte"] or ["opt"]. Notice that this is possible since the nature of
133
the toplevel has already been set in [Mltop] by the main file created
134
by coqmktop (see scripts/coqmktop.ml). *)
137
let s = !re_exec_version in
138
let is_native = Mltop.is_native in
139
(* Unix.readlink is not implemented on Windows architectures :-(
141
try Unix.readlink "/proc/self/exe"
142
with Unix.Unix_error _ -> Sys.argv.(0) in
144
let prog = Sys.argv.(0) in
145
if (is_native && s = "byte") || ((not is_native) && s = "opt")
147
let s = if s = "" then if is_native then "opt" else "byte" else s in
149
let dir = Filename.dirname prog in
150
let coqtop = if is_ide then "coqide." else "coqtop." in
151
let com = coqtop ^ s ^ Coq_config.exec_extension in
152
if dir <> "." then Filename.concat dir com else com
154
Sys.argv.(0) <- newprog;
155
Unix.handle_unix_error (Unix.execvp newprog) Sys.argv
158
(*s options for the virtual machine *)
160
let boxed_val = ref false
161
let boxed_def = ref false
162
let use_vm = ref false
165
Vm.set_transp_values (not !boxed_val);
166
Flags.set_boxed_definitions !boxed_def;
167
Vconv.set_use_vm !use_vm
169
(*s Parsing of the command line.
170
We no longer use [Arg.parse], in order to use share [Usage.print_usage]
171
between coqtop and coqc. *)
175
Usage.print_usage_coqc ()
177
Usage.print_usage_coqtop () ;
181
let warning s = msg_warning (str s)
184
let ide_args = ref []
185
let parse_args is_ide =
186
let glob_opt = ref false in
187
let rec parse = function
189
| "-with-geoproof" :: s :: rem ->
190
if s = "yes" then Coq_config.with_geoproof := true
191
else if s = "no" then Coq_config.with_geoproof := false
194
| "-impredicative-set" :: rem ->
195
set_engagement Declarations.ImpredicativeSet; parse rem
197
| ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
198
| ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
199
| ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
200
| ("-I"|"-include") :: [] -> usage ()
202
| "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
203
| "-R" :: d :: "-as" :: [] -> usage ()
204
| "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
205
| "-R" :: ([] | [_]) -> usage ()
207
| "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem
208
| "-top" :: [] -> usage ()
210
| "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem
211
| "-exclude-dir" :: [] -> usage ()
213
| "-notop" :: rem -> unset_toplevel_name (); parse rem
214
| "-q" :: rem -> no_load_rc (); parse rem
216
| "-opt" :: rem -> set_opt(); parse rem
217
| "-byte" :: rem -> set_byte(); parse rem
218
| "-full" :: rem -> warning "option -full deprecated\n"; parse rem
220
| "-batch" :: rem -> set_batch_mode (); parse rem
221
| "-boot" :: rem -> boot := true; no_load_rc (); parse rem
222
| "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem
223
| "-outputstate" :: s :: rem -> set_outputstate s; parse rem
224
| "-outputstate" :: [] -> usage ()
226
| "-nois" :: rem -> set_inputstate ""; parse rem
228
| ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
229
| ("-inputstate"|"-is") :: [] -> usage ()
231
| "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f; parse rem
232
| "-load-ml-object" :: [] -> usage ()
234
| "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem
235
| "-load-ml-source" :: [] -> usage ()
237
| ("-load-vernac-source"|"-l") :: f :: rem ->
238
add_load_vernacular false f; parse rem
239
| ("-load-vernac-source"|"-l") :: [] -> usage ()
241
| ("-load-vernac-source-verbose"|"-lv") :: f :: rem ->
242
add_load_vernacular true f; parse rem
243
| ("-load-vernac-source-verbose"|"-lv") :: [] -> usage ()
245
| "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
246
| "-load-vernac-object" :: [] -> usage ()
248
| "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); glob_opt := true; parse rem
249
(* À ne pas documenter : l'option 'stdout' n'étant
250
éventuellement utile que pour le debugging... *)
251
| "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; glob_opt := true; parse rem
252
| "-dump-glob" :: [] -> usage ()
253
| ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); glob_opt := true; parse rem
255
| "-require" :: f :: rem -> add_require f; parse rem
256
| "-require" :: [] -> usage ()
258
| "-compile" :: f :: rem -> add_compile false f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
259
| "-compile" :: [] -> usage ()
261
| "-compile-verbose" :: f :: rem -> add_compile true f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
262
| "-compile-verbose" :: [] -> usage ()
264
| "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem
266
| "-beautify" :: rem -> make_beautify true; parse rem
268
| "-unsafe" :: f :: rem -> add_unsafe f; parse rem
269
| "-unsafe" :: [] -> usage ()
271
| "-debug" :: rem -> set_debug (); parse rem
273
| "-vm" :: rem -> use_vm := true; parse rem
274
| "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
275
| "-emacs-U" :: rem -> Flags.print_emacs := true;
276
Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
278
| "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
280
| "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
281
| "-coqlib" :: [] -> usage ()
283
| "-where" :: _ -> print_endline (Envars.coqlib ()); exit 0
285
| ("-config"|"--config") :: _ -> Usage.print_config (); exit 0
287
| ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
289
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
291
| ("-v"|"--version") :: _ -> Usage.version ()
293
| "-init-file" :: f :: rem -> set_rcfile f; parse rem
294
| "-init-file" :: [] -> usage ()
296
| "-user" :: u :: rem -> set_rcuser u; parse rem
297
| "-user" :: [] -> usage ()
299
| "-notactics" :: rem -> remove_top_ml (); parse rem
301
| "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
303
| ("-m" | "--memory") :: rem -> memory_stat := true; parse rem
305
| "-xml" :: rem -> Flags.xml_export := true; parse rem
307
| "-output-context" :: rem -> output_context := true; parse rem
309
(* Scanned in Flags. *)
310
| "-v7" :: rem -> error "This version of Coq does not support v7 syntax"
311
| "-v8" :: rem -> parse rem
313
| "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
317
ide_args := s :: !ide_args;
320
prerr_endline ("Don't know what to do with " ^ s); usage ()
324
parse (List.tl (Array.to_list Sys.argv))
326
| UserError(_,s) as e -> begin
328
Stream.empty s; exit 1
329
with Stream.Failure ->
330
msgnl (Cerrors.explain_exn e); exit 1
332
| e -> begin msgnl (Cerrors.explain_exn e); exit 1 end
335
Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
341
if_verbose print_header ();
346
if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
347
Option.iter Declaremods.start_library !toplevel_name;
348
init_library_roots ();
357
if not !batch_mode then message "Error during initialization:";
358
msgnl (Toplevel.print_toplevel_error e);
363
if !output_context then
364
Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
365
Profile.print_profile ();
367
Lib.declare_initial_state ()
369
let init_ide () = init true; List.rev !ide_args
374
(* Initialise and launch the Ocaml toplevel *)
375
Coqinit.init_ocaml_path();
376
Mltop.ocaml_toploop();
379
(* [Coqtop.start] will be called by the code produced by coqmktop *)
added
removed
toplevel/coqtop.ml
