summaryrefslogtreecommitdiff
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml687
1 files changed, 465 insertions, 222 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d2eb7d9c..142f3386 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -1,36 +1,96 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
+open Errors
open Util
open System
open Flags
open Names
open Libnames
-open Nameops
open States
-open Toplevel
open Coqinit
+let () = at_exit flush_all
+
+let ( / ) = Filename.concat
+
+let fatal_error info anomaly =
+ let msg = info ++ fnl () in
+ pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
+ flush_all ();
+ exit (if anomaly then 129 else 1)
+
let get_version_date () =
try
- let coqlib = Envars.coqlib () in
- let ch = open_in (Filename.concat coqlib "revision") in
+ let ch = open_in (Envars.coqlib () / "revision") in
let ver = input_line ch in
let rev = input_line ch in
- (ver,rev)
+ let () = close_in ch in
+ (ver,rev)
with e when Errors.noncritical e ->
(Coq_config.version,Coq_config.date)
let print_header () =
- let (ver,rev) = (get_version_date ()) in
- Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
- flush stdout
+ let (ver,rev) = get_version_date () in
+ ppnl (str ("Welcome to Coq "^ver^" ("^rev^")"));
+ pp_flush ()
+
+let warning s = msg_warning (strbrk s)
+
+let toploop = ref None
+
+let color : [`ON | `AUTO | `OFF] ref = ref `AUTO
+let set_color = function
+| "on" -> color := `ON
+| "off" -> color := `OFF
+| "auto" -> color := `AUTO
+| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1
+
+let init_color () =
+ let has_color = match !color with
+ | `OFF -> false
+ | `ON -> true
+ | `AUTO ->
+ Terminal.has_style Unix.stdout &&
+ Terminal.has_style Unix.stderr
+ in
+ if has_color then begin
+ let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
+ match colors with
+ | None ->
+ (** Default colors *)
+ Ppstyle.init_color_output ()
+ | Some "" ->
+ (** No color output *)
+ ()
+ | Some s ->
+ (** Overwrite all colors *)
+ Ppstyle.clear_styles ();
+ Ppstyle.parse_config s;
+ Ppstyle.init_color_output ()
+ end
+
+let toploop_init = ref begin fun x ->
+ let () = init_color () in
+ let () = CoqworkmgrApi.(init !Flags.async_proofs_worker_priority) in
+ x
+ end
+
+let toploop_run = ref (fun () ->
+ if Dumpglob.dump () then begin
+ if_verbose warning "Dumpglob cannot be used in interactive mode.";
+ Dumpglob.noglob ()
+ end;
+ Coqloop.loop();
+ (* Initialise and launch the Ocaml toplevel *)
+ Coqinit.init_ocaml_path();
+ Mltop.ocaml_toploop())
let output_context = ref false
@@ -38,7 +98,8 @@ let memory_stat = ref false
let print_memory_stat () =
if !memory_stat then
- Format.printf "total heap size = %d kbytes\n" (heap_size_kb ())
+ ppnl
+ (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes")
let _ = at_exit print_memory_stat
@@ -47,40 +108,40 @@ let set_engagement c = engagement := Some c
let engage () =
match !engagement with Some c -> Global.set_engagement c | None -> ()
+let type_in_type = ref false
+let set_type_in_type () = type_in_type := true
+let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
+
let set_batch_mode () = batch_mode := true
-let toplevel_default_name = make_dirpath [id_of_string "Top"]
+let toplevel_default_name = DirPath.make [Id.of_string "Top"]
let toplevel_name = ref (Some toplevel_default_name)
let set_toplevel_name dir =
- if dir = empty_dirpath then error "Need a non empty toplevel module name";
+ if DirPath.is_empty dir then error "Need a non empty toplevel module name";
toplevel_name := Some dir
let unset_toplevel_name () = toplevel_name := None
let remove_top_ml () = Mltop.remove ()
-let inputstate = ref None
-let set_inputstate s = inputstate:= Some s
-let inputstate () =
- match !inputstate with
- | Some "" -> ()
- | Some s -> intern_state s
- | None -> intern_state "initial.coq"
+let inputstate = ref ""
+let set_inputstate s =
+ let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in
+ inputstate:=s
+let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate
let outputstate = ref ""
-let set_outputstate s = outputstate:=s
-let outputstate () = if !outputstate <> "" then extern_state !outputstate
+let set_outputstate s =
+ let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in
+ outputstate:=s
+let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
-let set_default_include d = push_include (d,Nameops.default_root_prefix)
-let set_include d p =
+let set_include d p recursive implicit =
let p = dirpath_of_string p in
- push_include (d,p)
-let set_rec_include d p =
- let p = dirpath_of_string p in
- push_rec_include(d,p)
+ push_include d p recursive implicit
let load_vernacular_list = ref ([] : (string * bool) list)
let add_load_vernacular verb s =
- load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list
+ load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
let load_vernacular () =
List.iter
(fun (s,b) ->
@@ -96,29 +157,57 @@ let load_vernac_obj () =
List.iter (fun f -> Library.require_library_from_file None f None)
(List.rev !load_vernacular_obj)
+let require_prelude () =
+ let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
+ let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in
+ let m =
+ if Sys.file_exists vo then vo else
+ if Sys.file_exists vio then vio else vo in
+ Library.require_library_from_dirpath [Coqlib.prelude_module,m] (Some true)
+
let require_list = ref ([] : string list)
let add_require s = require_list := s :: !require_list
let require () =
+ if !load_init then silently require_prelude ();
List.iter (fun s -> Library.require_library_from_file None s (Some false))
(List.rev !require_list)
let compile_list = ref ([] : (bool * string) list)
+
+let glob_opt = ref false
+
let add_compile verbose s =
set_batch_mode ();
Flags.make_silent true;
+ if not !glob_opt then Dumpglob.dump_to_dotglob ();
+ (** make the file name explicit; needed not to break up Coq loadpath stuff. *)
+ let s =
+ let open Filename in
+ if is_implicit s
+ then concat current_dir_name s
+ else s
+ in
compile_list := (verbose,s) :: !compile_list
+
+let compile_file (v,f) =
+ if Flags.do_beautify () then
+ with_option beautify_file (Vernac.compile v) f
+ else
+ Vernac.compile v f
+
let compile_files () =
- let init_state = States.freeze() in
- let coqdoc_init_state = Dumpglob.coqdoc_freeze () in
- List.iter
- (fun (v,f) ->
- States.unfreeze init_state;
- Dumpglob.coqdoc_unfreeze coqdoc_init_state;
- if Flags.do_beautify () then
- with_option beautify_file (Vernac.compile v) f
- else
- Vernac.compile v f)
- (List.rev !compile_list)
+ match !compile_list with
+ | [] -> ()
+ | [vf] -> compile_file vf (* One compilation : no need to save init state *)
+ | l ->
+ let init_state = States.freeze ~marshallable:`No in
+ let coqdoc_init_state = Lexer.location_table () in
+ List.iter
+ (fun vf ->
+ States.unfreeze init_state;
+ Lexer.restore_location_table coqdoc_init_state;
+ compile_file vf)
+ (List.rev l)
(*s options for the virtual machine *)
@@ -129,248 +218,402 @@ let set_vm_opt () =
Vm.set_transp_values (not !boxed_val);
Vconv.set_use_vm !use_vm
+(** Options for proof general *)
+
+let set_emacs () =
+ Flags.print_emacs := true;
+ Pp.make_pp_emacs ();
+ Vernacentries.qed_display_script := false;
+ color := `OFF
+
+(** GC tweaking *)
+
+(** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
+ minor heap is heavily sollicited. Unfortunately, the default size is far too
+ small, so we enlarge it a lot (128 times larger).
+
+ To better handle huge memory consumers, we also augment the default major
+ heap increment and the GC pressure coefficient.
+*)
+
+let init_gc () =
+ let param =
+ try ignore (Sys.getenv "OCAMLRUNPARAM"); true
+ with Not_found -> false
+ in
+ let control = Gc.get () in
+ let tweaked_control = { control with
+ Gc.minor_heap_size = 33554432; (** 4M *)
+(* Gc.major_heap_increment = 268435456; (** 32M *) *)
+ Gc.space_overhead = 120;
+ } in
+ if param then ()
+ else Gc.set tweaked_control
+
(*s Parsing of the command line.
We no longer use [Arg.parse], in order to use share [Usage.print_usage]
between coqtop and coqc. *)
let usage () =
- if !batch_mode then
- Usage.print_usage_coqc ()
- else
- Usage.print_usage_coqtop () ;
- flush stderr ;
- exit 1
+ Envars.set_coqlib Errors.error;
+ init_load_path ();
+ if !batch_mode then Usage.print_usage_coqc ()
+ else begin
+ Mltop.load_ml_objects_raw_rex
+ (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
+ Usage.print_usage_coqtop ()
+ end
+
+let print_style_tags () =
+ let () = init_color () in
+ let tags = Ppstyle.dump () in
+ let iter (t, st) =
+ let st = match st with Some st -> st | None -> Terminal.make () in
+ let opt =
+ Terminal.eval st ^
+ String.concat "." (Ppstyle.repr t) ^
+ Terminal.reset ^ "\n"
+ in
+ print_string opt
+ in
+ List.iter iter tags;
+ flush_all ()
-let warning s = msg_warning (str s)
+let error_missing_arg s =
+ prerr_endline ("Error: extra argument expected after option "^s);
+ prerr_endline "See -help for the syntax of supported options";
+ exit 1
-let ide_slave = ref false
let filter_opts = ref false
+let exitcode () = if !filter_opts then 2 else 0
let verb_compat_ntn = ref false
let no_compat_ntn = ref false
-let parse_args arglist =
- let glob_opt = ref false in
- let rec parse = function
- | [] -> []
- | "-with-geoproof" :: s :: rem ->
- if s = "yes" then Coq_config.with_geoproof := true
- else if s = "no" then Coq_config.with_geoproof := false
- else usage ();
- parse rem
- | "-impredicative-set" :: rem ->
- set_engagement Declarations.ImpredicativeSet; parse rem
-
- | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
- | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
- | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
- | ("-I"|"-include") :: [] -> usage ()
-
- | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
- | "-R" :: d :: "-as" :: [] -> usage ()
- | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
- | "-R" :: ([] | [_]) -> usage ()
-
- | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem
- | "-top" :: [] -> usage ()
-
- | "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem
- | "-exclude-dir" :: [] -> usage ()
-
- | "-notop" :: rem -> unset_toplevel_name (); parse rem
- | "-q" :: rem -> no_load_rc (); parse rem
-
- | "-opt" :: rem -> warning "option -opt deprecated, call with .opt suffix\n"; parse rem
- | "-byte" :: rem -> warning "option -byte deprecated, call with .byte suffix\n"; parse rem
- | "-full" :: rem -> warning "option -full deprecated\n"; parse rem
-
- | "-batch" :: rem -> set_batch_mode (); parse rem
- | "-boot" :: rem -> boot := true; no_load_rc (); parse rem
- | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem
- | "-outputstate" :: s :: rem ->
- Flags.load_proofs := Flags.Force; set_outputstate s; parse rem
- | "-outputstate" :: [] -> usage ()
-
- | "-nois" :: rem -> set_inputstate ""; parse rem
-
- | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
- | ("-inputstate"|"-is") :: [] -> usage ()
+let print_where = ref false
+let print_config = ref false
+let print_tags = ref false
- | "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f; parse rem
- | "-load-ml-object" :: [] -> usage ()
+let get_priority opt s =
+ try Flags.priority_of_string s
+ with Invalid_argument _ ->
+ prerr_endline ("Error: low/high expected after "^opt); exit 1
- | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem
- | "-load-ml-source" :: [] -> usage ()
+let get_async_proofs_mode opt = function
+ | "off" -> Flags.APoff
+ | "on" -> Flags.APon
+ | "lazy" -> Flags.APonLazy
+ | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1
- | ("-load-vernac-source"|"-l") :: f :: rem ->
- add_load_vernacular false f; parse rem
- | ("-load-vernac-source"|"-l") :: [] -> usage ()
+let get_cache opt = function
+ | "force" -> Some Flags.Force
+ | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
- | ("-load-vernac-source-verbose"|"-lv") :: f :: rem ->
- add_load_vernacular true f; parse rem
- | ("-load-vernac-source-verbose"|"-lv") :: [] -> usage ()
- | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
- | "-load-vernac-object" :: [] -> usage ()
+let set_worker_id opt s =
+ assert (s <> "master");
+ Flags.async_proofs_worker_id := s
- | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); glob_opt := true; parse rem
- (* À ne pas documenter : l'option 'stdout' n'étant
- éventuellement utile que pour le debugging... *)
- | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; glob_opt := true; parse rem
- | "-dump-glob" :: [] -> usage ()
- | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); glob_opt := true; parse rem
+let get_bool opt = function
+ | "yes" -> true
+ | "no" -> false
+ | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
- | "-require" :: f :: rem -> add_require f; parse rem
- | "-require" :: [] -> usage ()
+let get_int opt n =
+ try int_of_string n
+ with Failure _ ->
+ prerr_endline ("Error: integer expected after option "^opt); exit 1
- | "-compile" :: f :: rem -> add_compile false f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
- | "-compile" :: [] -> usage ()
+let get_host_port opt s =
+ match CString.split ':' s with
+ | [host; port] -> Some (Spawned.Socket(host, int_of_string port))
+ | ["stdfds"] -> Some Spawned.AnonPipe
+ | _ ->
+ prerr_endline ("Error: host:port or stdfds expected after option "^opt);
+ exit 1
- | "-compile-verbose" :: f :: rem -> add_compile true f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
- | "-compile-verbose" :: [] -> usage ()
+let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
- | "-force-load-proofs" :: rem -> Flags.load_proofs := Flags.Force; parse rem
- | "-lazy-load-proofs" :: rem -> Flags.load_proofs := Flags.Lazy; parse rem
- | "-dont-load-proofs" :: rem -> Flags.load_proofs := Flags.Dont; parse rem
+let vio_tasks = ref []
- | "-beautify" :: rem -> make_beautify true; parse rem
-
- | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
- | "-unsafe" :: [] -> usage ()
-
- | "-debug" :: rem -> set_debug (); parse rem
-
- | "-compat" :: v :: rem ->
- Flags.compat_version := get_compat_version v; parse rem
- | "-compat" :: [] -> usage ()
-
- | "-verbose-compat-notations" :: rem -> verb_compat_ntn := true; parse rem
- | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem
-
- | "-vm" :: rem -> use_vm := true; parse rem
- | "-emacs" :: rem ->
- Flags.print_emacs := true; Pp.make_pp_emacs();
- Vernacentries.qed_display_script := false;
- parse rem
- | "-emacs-U" :: rem ->
- warning "Obsolete option \"-emacs-U\", use -emacs instead.";
- parse ("-emacs" :: rem)
-
- | "-unicode" :: rem -> add_require "Utf8_core"; parse rem
-
- | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
- | "-coqlib" :: [] -> usage ()
-
- | "-where" :: _ -> print_endline (Envars.coqlib ()); exit (if !filter_opts then 2 else 0)
-
- | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0)
-
- | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
-
- | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
-
- | ("-v"|"--version") :: _ -> Usage.version (if !filter_opts then 2 else 0)
-
- | "-init-file" :: f :: rem -> set_rcfile f; parse rem
- | "-init-file" :: [] -> usage ()
-
- | "-notactics" :: rem ->
- warning "Obsolete option \"-notactics\".";
- remove_top_ml (); parse rem
-
- | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
-
- | ("-m" | "--memory") :: rem -> memory_stat := true; parse rem
-
- | "-xml" :: rem -> Flags.xml_export := true; parse rem
-
- | "-output-context" :: rem -> output_context := true; parse rem
-
- (* Scanned in Flags. *)
- | "-v7" :: rem -> error "This version of Coq does not support v7 syntax"
- | "-v8" :: rem -> parse rem
-
- | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
-
- | "-ideslave" :: rem -> ide_slave := true; parse rem
+let add_vio_task f =
+ set_batch_mode ();
+ Flags.make_silent true;
+ vio_tasks := f :: !vio_tasks
+
+let check_vio_tasks () =
+ let rc =
+ List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
+ true (List.rev !vio_tasks) in
+ if not rc then exit 1
+
+let vio_files = ref []
+let vio_files_j = ref 0
+let vio_checking = ref false
+let add_vio_file f =
+ set_batch_mode ();
+ Flags.make_silent true;
+ vio_files := f :: !vio_files
+
+let set_vio_checking_j opt j =
+ try vio_files_j := int_of_string j
+ with Failure _ ->
+ prerr_endline ("The first argument of " ^ opt ^ " must the number");
+ prerr_endline "of concurrent workers to be used (a positive integer).";
+ prerr_endline "Makefiles generated by coq_makefile should be called";
+ prerr_endline "setting the J variable like in 'make vio2vo J=3'";
+ exit 1
+
+let is_not_dash_option = function
+ | Some f when String.length f > 0 && f.[0] <> '-' -> true
+ | _ -> false
+
+let schedule_vio_checking () =
+ if !vio_files <> [] && !vio_checking then
+ Vio_checking.schedule_vio_checking !vio_files_j !vio_files
+let schedule_vio_compilation () =
+ if !vio_files <> [] && not !vio_checking then
+ Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
+
+let get_native_name s =
+ (* We ignore even critical errors because this mode has to be super silent *)
+ try
+ String.concat Filename.dir_sep [Filename.dirname s;
+ Nativelib.output_dir; Library.native_name_from_filename s]
+ with _ -> ""
- | "-filteropts" :: rem -> filter_opts := true; parse rem
+let parse_args arglist =
+ let args = ref arglist in
+ let extras = ref [] in
+ let rec parse () = match !args with
+ | [] -> List.rev !extras
+ | opt :: rem ->
+ args := rem;
+ let next () = match !args with
+ | x::rem -> args := rem; x
+ | [] -> error_missing_arg opt
+ in
+ let peek_next () = match !args with
+ | x::_ -> Some x
+ | [] -> None
+ in
+ begin match opt with
+
+ (* Complex options with many args *)
+ |"-I"|"-include" ->
+ begin match rem with
+ | d :: "-as" :: p :: rem -> set_include d p false true; args := rem
+ | d :: "-as" :: [] -> error_missing_arg "-as"
+ | d :: rem -> push_ml_include d; args := rem
+ | [] -> error_missing_arg opt
+ end
+ |"-Q" ->
+ begin match rem with
+ | d :: p :: rem -> set_include d p true false; args := rem
+ | _ -> error_missing_arg opt
+ end
+ |"-R" ->
+ begin match rem with
+ | d :: "-as" :: [] -> error_missing_arg "-as"
+ | d :: "-as" :: p :: rem
+ | d :: p :: rem -> set_include d p true true; args := rem
+ | _ -> error_missing_arg opt
+ end
- | s :: rem ->
- if !filter_opts then
- s :: (parse rem)
- else
- (prerr_endline ("Don't know what to do with " ^ s); usage ())
+ (* Options with two arg *)
+ |"-check-vio-tasks" ->
+ let tno = get_task_list (next ()) in
+ let tfile = next () in
+ add_vio_task (tno,tfile)
+ |"-schedule-vio-checking" ->
+ vio_checking := true;
+ set_vio_checking_j opt (next ());
+ add_vio_file (next ());
+ while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
+ |"-schedule-vio2vo" ->
+ set_vio_checking_j opt (next ());
+ add_vio_file (next ());
+ while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
+
+ (* Options with one arg *)
+ |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
+ |"-async-proofs" ->
+ Flags.async_proofs_mode := get_async_proofs_mode opt (next())
+ |"-async-proofs-j" ->
+ Flags.async_proofs_n_workers := (get_int opt (next ()))
+ |"-async-proofs-cache" ->
+ Flags.async_proofs_cache := get_cache opt (next ())
+ |"-async-proofs-tac-j" ->
+ Flags.async_proofs_n_tacworkers := (get_int opt (next ()))
+ |"-async-proofs-worker-priority" ->
+ Flags.async_proofs_worker_priority := get_priority opt (next ())
+ |"-async-proofs-private-flags" ->
+ Flags.async_proofs_private_flags := Some (next ());
+ |"-worker-id" -> set_worker_id opt (next ())
+ |"-compat" -> Flags.compat_version := get_compat_version (next ())
+ |"-compile" -> add_compile false (next ())
+ |"-compile-verbose" -> add_compile true (next ())
+ |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
+ |"-feedback-glob" -> Dumpglob.feedback_glob ()
+ |"-exclude-dir" -> exclude_search_in_dirname (next ())
+ |"-init-file" -> set_rcfile (next ())
+ |"-inputstate"|"-is" -> set_inputstate (next ())
+ |"-load-ml-object" -> Mltop.dir_ml_load (next ())
+ |"-load-ml-source" -> Mltop.dir_ml_use (next ())
+ |"-load-vernac-object" -> add_vernac_obj (next ())
+ |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ())
+ |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
+ |"-outputstate" -> set_outputstate (next ())
+ |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
+ |"-require" -> add_require (next ())
+ |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
+ |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
+ |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
+ |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
+ |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
+ |"-toploop" -> toploop := Some (next ())
+
+ (* Options with zero arg *)
+ |"-async-queries-always-delegate"
+ |"-async-proofs-always-delegate"
+ |"-async-proofs-full" ->
+ Flags.async_proofs_full := true;
+ |"-async-proofs-never-reopen-branch" ->
+ Flags.async_proofs_never_reopen_branch := true;
+ |"-batch" -> set_batch_mode ()
+ |"-beautify" -> make_beautify true
+ |"-boot" -> boot := true; no_load_rc ()
+ |"-bt" -> Backtrace.record_backtrace true
+ |"-color" -> set_color (next ())
+ |"-config"|"--config" -> print_config := true
+ |"-debug" -> set_debug ()
+ |"-emacs" -> set_emacs ()
+ |"-filteropts" -> filter_opts := true
+ |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
+ |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
+ |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+ |"-indices-matter" -> Indtypes.enforce_indices_matter ()
+ |"-just-parsing" -> Vernac.just_parsing := true
+ |"-m"|"--memory" -> memory_stat := true
+ |"-noinit"|"-nois" -> load_init := false
+ |"-no-compat-notations" -> no_compat_ntn := true
+ |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
+ |"-no-native-compiler" -> no_native_compiler := true
+ |"-notop" -> unset_toplevel_name ()
+ |"-output-context" -> output_context := true
+ |"-q" -> no_load_rc ()
+ |"-quiet"|"-silent" -> Flags.make_silent true
+ |"-quick" -> Flags.compilation_mode := BuildVio
+ |"-list-tags" -> print_tags := true
+ |"-time" -> Flags.time := true
+ |"-type-in-type" -> set_type_in_type ()
+ |"-unicode" -> add_require "Utf8_core"
+ |"-v"|"--version" -> Usage.version (exitcode ())
+ |"-verbose-compat-notations" -> verb_compat_ntn := true
+ |"-vm" -> use_vm := true
+ |"-where" -> print_where := true
+
+ (* Deprecated options *)
+ |"-byte" -> warning "option -byte deprecated, call with .byte suffix"
+ |"-opt" -> warning "option -opt deprecated, call with .opt suffix"
+ |"-full" -> warning "option -full deprecated"
+ |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml ()
+ |"-emacs-U" ->
+ warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs ()
+ |"-v7" -> error "This version of Coq does not support v7 syntax"
+ |"-v8" -> warning "Obsolete option \"-v8\"."
+ |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"."
+ |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"."
+ |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"."
+ |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ())
+ |"-quality" -> warning "Obsolete option \"-quality\"."
+ |"-xml" -> warning "Obsolete option \"-xml\"."
+
+ (* Unknown option *)
+ | s -> extras := s :: !extras
+ end;
+ parse ()
in
try
- parse arglist
+ parse ()
with
- | UserError(_,s) as e -> begin
- try
- Stream.empty s; exit 1
- with Stream.Failure ->
- msgnl (Errors.print e); exit 1
- end
- | any -> begin msgnl (Errors.print any); exit 1 end
+ | UserError(_, s) as e ->
+ if is_empty s then exit 1
+ else fatal_error (Errors.print e) false
+ | any -> fatal_error (Errors.print any) (Errors.is_anomaly any)
let init arglist =
+ init_gc ();
Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
Lib.init();
(* Default Proofb Mode starts with an alternative default. *)
Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic";
begin
try
- let foreign_args = parse_args arglist in
- if !filter_opts then
- (print_string (String.concat "\n" foreign_args); exit 0);
- if !ide_slave then begin
- Flags.make_silent true;
- Ide_slave.init_stdout ()
+ let extras = parse_args arglist in
+ (* If we have been spawned by the Spawn module, this has to be done
+ * early since the master waits us to connect back *)
+ Spawned.init_channels ();
+ Envars.set_coqlib Errors.error;
+ if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
+ if !print_config then (Usage.print_config (); exit (exitcode ()));
+ if !print_tags then (print_style_tags (); exit (exitcode ()));
+ if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
+ init_load_path ();
+ Option.iter Mltop.load_ml_object_raw !toploop;
+ let extras = !toploop_init extras in
+ if not (List.is_empty extras) then begin
+ prerr_endline ("Don't know what to do with "^String.concat " " extras);
+ prerr_endline "See -help for the list of supported options";
+ exit 1
end;
if_verbose print_header ();
- init_load_path ();
inputstate ();
Mltop.init_known_plugins ();
set_vm_opt ();
engage ();
+ set_hierarchy ();
(* Be careful to set these variables after the inputstate *)
Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
Syntax_def.set_compat_notations (not !no_compat_ntn);
- if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
- Option.iter Declaremods.start_library !toplevel_name;
+ if (not !batch_mode || List.is_empty !compile_list)
+ && Global.env_is_initial ()
+ then Option.iter Declaremods.start_library !toplevel_name;
init_library_roots ();
load_vernac_obj ();
require ();
+ Stm.init ();
load_rcfile();
load_vernacular ();
compile_files ();
+ schedule_vio_checking ();
+ schedule_vio_compilation ();
+ check_vio_tasks ();
outputstate ()
with any ->
+ let any = Errors.push any in
flush_all();
- if not !batch_mode then message "Error during initialization:";
- msgnl (Toplevel.print_toplevel_error any);
- exit 1
+ let msg =
+ if !batch_mode then mt ()
+ else str "Error during initialization:" ++ fnl ()
+ in
+ fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly (fst any))
end;
- if !batch_mode then
- (flush_all();
- if !output_context then
- Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
- Profile.print_profile ();
- exit 0);
- (* We initialize the command history stack with a first entry *)
- Backtrack.mark_command Vernacexpr.VernacNop
+ if !batch_mode then begin
+ flush_all();
+ if !output_context then
+ Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
+ Profile.print_profile ();
+ exit 0
+ end
let init_toplevel = init
let start () =
- init_toplevel (List.tl (Array.to_list Sys.argv));
- if !ide_slave then
- Ide_slave.loop ()
- else
- Toplevel.loop();
- (* Initialise and launch the Ocaml toplevel *)
- Coqinit.init_ocaml_path();
- Mltop.ocaml_toploop();
+ let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
+ (* In batch mode, Coqtop has already exited at this point. In interactive one,
+ dump glob is nothing but garbage ... *)
+ !toploop_run ();
exit 1
(* [Coqtop.start] will be called by the code produced by coqmktop *)