diff options
33 files changed, 1076 insertions, 771 deletions
@@ -68,6 +68,11 @@ Universes module and library boundaries. Global universe names introduced in an inductive / constant / Let declaration get qualified with the name of the declaration. +- Universe cumulativity for inductive types is now specified as a + variance for each polymorphic universe. See the reference manual for + more information. +- Fix #5726: Notations that start with `Type` now support universe instances + with `@{u}`. Checker @@ -84,6 +89,18 @@ Documentation moved to the GitHub wiki section of this repository; the main entry page is https://github.com/coq/coq/wiki/The-Coq-FAQ. +Changes from 8.7.1 to 8.7.2 +=========================== + +Fixed a critical bug in the VM handling of universes (#6677). This bug +affected all releases since 8.5. + +Improved support for building with OCaml 4.06.0 and external num package. + +Many other bug fixes, documentation improvements, and user +message improvements (for details, see the 8.7.2 milestone at +https://github.com/coq/coq/milestone/11?closed=1). + Changes from 8.7.0 to 8.7.1 =========================== diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index d7acf01f1..e4359f703 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -50,6 +50,15 @@ else fi +if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then + echo + read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]]; then + exit 1 + fi +fi + if [[ "${OPTION}" == "--stop-before-merging" ]]; then exit 0 fi diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5f40a2242..6d1064d25 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -454,9 +454,11 @@ let slave_feeder fmt xml_oc msg = let msg_format = ref (fun () -> let margin = Option.default 72 (Topfmt.get_margin ()) in Xmlprotocol.Richpp margin -) + ) -let loop doc = +(* The loop ignores the command line arguments as the current model delegates + its handing to the toplevel container. *) +let loop _args doc = set_doc doc; init_signal_handler (); catch_break := false; @@ -504,8 +506,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let () = Coqtop.toploop_init := (fun args -> - let args = parse args in +let () = Coqtop.toploop_init := (fun coq_args extra_args -> + let args = parse extra_args in Flags.quiet := true; CoqworkmgrApi.(init High); args) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 5dab2932d..4a34dbcff 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -628,27 +628,17 @@ let rec compile_constr reloc c sz cont = of the structured constant, while the later (if any) will be applied as arguments. *) let open Univ in begin - let levels = Universe.levels u in - let global_levels = - LSet.filter (fun x -> Level.var_index x = None) levels - in - let local_levels = - List.map_filter (fun x -> Level.var_index x) - (LSet.elements levels) - in + let u,s = Universe.compact u in (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) - let uglob = - LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m - in - if local_levels = [] then - compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont + if List.is_empty s then + compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont else let compile_get_univ reloc idx sz cont = set_max_stack_size sz; compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc - (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont + (Bstrconst (Const_type u)) (Array.of_list s) sz cont end | LetIn(_,xb,_,body) -> compile_constr reloc xb sz diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 2bbb867cd..bbd284bc1 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -70,7 +70,7 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn _, _ -> false | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false -| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type u1, Const_type u2 -> Univ.Universe.equal u1 u2 | Const_type _ , _ -> false let rec hash_structured_constant c = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 159d2ea66..da7042713 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -882,6 +882,18 @@ let hnf_prod_app env t n = let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl +let hnf_prod_applist_assum env n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Too many arguments.") + else match kind (whd_allnolet env t), l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") + | _ -> anomaly (Pp.str "Not enough prod/let's.") in + app n [] c l + (* Dealing with arities *) let dest_prod env = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0e6a2b819..6f7e3f8f8 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -105,6 +105,12 @@ val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to + the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it + returns [t] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val hnf_prod_applist_assum : env -> int -> types -> constr list -> types + (** Compatibility alias for Term.lambda_appvect_assum *) val betazeta_appvect : int -> constr -> constr array -> constr diff --git a/kernel/term.ml b/kernel/term.ml index fae990d45..a4c92bd33 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -352,10 +352,11 @@ let lambda_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l @@ -377,10 +378,11 @@ let prod_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l diff --git a/kernel/term.mli b/kernel/term.mli index c9a8cf6e1..b4597676a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr val lambda_appvect : constr -> constr array -> constr (** In [lambda_applist_assum n c args], [c] is supposed to have the - form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) val lambda_applist_assum : int -> constr -> constr list -> constr @@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr (** pseudo-reduction rule *) (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) -val prod_appvect : constr -> constr array -> constr -val prod_applist : constr -> constr list -> constr +val prod_appvect : types -> constr array -> types +val prod_applist : types -> constr list -> types (** In [prod_appvect_assum n c args], [c] is supposed to have the - form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) -val prod_appvect_assum : int -> constr -> constr array -> constr -val prod_applist_assum : int -> constr -> constr list -> constr +val prod_appvect_assum : int -> types -> constr array -> types +val prod_applist_assum : int -> types -> constr list -> types (** {5 Other term destructors. } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5f501bff1..9b864440d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -223,9 +223,8 @@ let rec unzip ctx j = unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let feedback_completion_typecheck = - let open Feedback in Option.iter (fun state_id -> - feedback ~id:state_id Feedback.Complete) + Feedback.feedback ~id:state_id Feedback.Complete) let abstract_constant_universes = function | Monomorphic_const_entry uctx -> diff --git a/kernel/univ.ml b/kernel/univ.ml index 080bb7ad4..fbb047364 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -266,7 +266,7 @@ struct module Expr = struct type t = Level.t * int - + (* Hashing of expressions *) module ExprHash = struct @@ -487,7 +487,40 @@ struct | [] -> cons a l in List.fold_right (fun a acc -> aux a acc) u [] - + + (** [max_var_pred p u] returns the maximum variable level in [u] satisfying + [p], -1 if not found *) + let rec max_var_pred p u = + let open Level in + match u with + | [] -> -1 + | (v, _) :: u -> + match var_index v with + | Some i when p i -> max i (max_var_pred p u) + | _ -> max_var_pred p u + + let rec remap_var u i j = + let open Level in + match u with + | [] -> [] + | (v, incr) :: u when var_index v = Some i -> + (Level.var j, incr) :: remap_var u i j + | _ :: u -> remap_var u i j + + let rec compact u max_var i = + if i >= max_var then (u,[]) else + let j = max_var_pred (fun j -> j < i) u in + if Int.equal i (j+1) then + let (u,s) = compact u max_var (i+1) in + (u, i :: s) + else + let (u,s) = compact (remap_var u i j) max_var (i+1) in + (u, j+1 :: s) + + let compact u = + let max_var = max_var_pred (fun _ -> true) u in + compact u max_var 0 + (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y diff --git a/kernel/univ.mli b/kernel/univ.mli index 77ebf5a11..c45ebe21c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -125,6 +125,13 @@ sig val for_all : (Level.t * int -> bool) -> t -> bool val map : (Level.t * int -> 'a) -> t -> 'a list + + (** [compact u] remaps local variables in [u] such that their indices become + consecutive. It returns the new universe and the mapping. + Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] = + [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] + *) + val compact : t -> t * int list end type universe = Universe.t diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 1102cdec1..2d8a1d976 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -8,6 +8,7 @@ open Names open Sorts open Cbytecodes +open Univ (*******************************************) (* Initalization of the abstract machine ***) @@ -189,11 +190,11 @@ let rec whd_accu a stk = | i when Int.equal i type_atom_tag -> begin match stk with | [Zapp args] -> - let u = ref (Obj.obj (Obj.field at 0)) in - for i = 0 to nargs args - 1 do - u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) - done; - Vsort (Type !u) + let args = Array.init (nargs args) (arg args) in + let u = Obj.obj (Obj.field at 0) in + let inst = Instance.of_array (Array.map uni_lvl_val args) in + let u = Univ.subst_instance_universe inst u in + Vsort (Type u) | _ -> assert false end | i when i <= max_atom_tag -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b21fbf0eb..c93b41786 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -240,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in + hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 35487e09c..2cdb9be3f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -93,10 +93,11 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in + let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in - let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in + let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then @@ -173,10 +174,11 @@ let print_record env mind mib udecl = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in + let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in - let cstrtype = hnf_prod_applist env cstrtypes.(0) args in + let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 10b42f7e9..def60d1b9 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index a1fe50c63..928a6bfb0 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 17f90b7b1..f202fc7c5 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 704119186..d606f19bf 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -15,8 +15,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let loop init args = - let args = parse args in +let loop init _coq_args extra_args = + let args = parse extra_args in Flags.quiet := true; init (); CoqworkmgrApi.init !async_proofs_worker_priority; diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index da2e6fe0c..c42b48a28 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -9,4 +9,4 @@ (* Default priority *) val async_proofs_worker_priority : CoqworkmgrApi.priority ref -val loop : (unit -> unit) -> string list -> string list +val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list diff --git a/test-suite/bugs/closed/6677.v b/test-suite/bugs/closed/6677.v new file mode 100644 index 000000000..99e47bb87 --- /dev/null +++ b/test-suite/bugs/closed/6677.v @@ -0,0 +1,5 @@ +Set Universe Polymorphism. + +Definition T@{i} := Type@{i}. +Fail Definition U@{i} := (T@{i} <: Type@{i}). +Fail Definition eqU@{i j} : @eq T@{j} U@{i} T@{i} := eq_refl. diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index e912003f0..af202ea01 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,3 +1,7 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x + +For foo: Argument scopes are [type_scope _] +For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 8db8956e3..8ff91268a 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -1,3 +1,7 @@ Fail Inductive list' (A:Set) : Set := | nil' : list' A | cons' : A -> list' A -> list' (A*A). + +(* Check printing of let-ins *) +Inductive foo (A : Type) (x : A) (y := x) := Foo. +Print foo. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index ca02c983d..173eaae89 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -169,7 +169,8 @@ endif COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) COQCHKFLAGS?=-silent -o $(COQLIBS) -COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) +COQDOCFLAGS?=-interpolate -utf8 +COQDOCLIBS?=$(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml new file mode 100644 index 000000000..5b73471c5 --- /dev/null +++ b/toplevel/coqargs.ml @@ -0,0 +1,575 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s)) + +let fatal_error ?extra exn = + Topfmt.print_err_exn ?extra exn; + let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in + exit exit_code + +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 + +(******************************************************************************) +(* Imperative effects! This must be fixed at some point. *) +(******************************************************************************) +let set_worker_id opt s = + assert (s <> "master"); + Flags.async_proofs_worker_id := s + +let set_type_in_type () = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_universes = false } + +(******************************************************************************) + +type compilation_mode = BuildVo | BuildVio | Vio2Vo +type color = [`ON | `AUTO | `OFF] + +type coq_cmdopts = { + + load_init : bool; + load_rcfile : bool; + rcfile : string option; + + ml_includes : string list; + vo_includes : (string * Names.DirPath.t * bool) list; + vo_requires : (string * string option * bool option) list; + (* None = No Import; Some false = Import; Some true = Export *) + + (* XXX: Fusion? *) + batch_mode : bool; + compilation_mode : compilation_mode; + + toplevel_name : Names.DirPath.t; + toploop : string option; + + compile_list: (string * bool) list; (* bool is verbosity *) + compilation_output_name : string option; + + load_vernacular_list : (string * bool) list; + + vio_checking: bool; + vio_tasks : (int list * string) list; + vio_files : string list; + vio_files_j : int; + + color : color; + + impredicative_set : Declarations.set_predicativity; + stm_flags : Stm.AsyncOpts.stm_opt; + debug : bool; + time : bool; + + filter_opts : bool; + + glob_opt : bool; + + memory_stat : bool; + print_tags : bool; + print_where : bool; + print_config: bool; + output_context : bool; + + inputstate : string option; + outputstate : string option; + +} + +let init_args = { + + load_init = true; + load_rcfile = true; + rcfile = None; + + ml_includes = []; + vo_includes = []; + vo_requires = []; + + batch_mode = false; + compilation_mode = BuildVo; + + toplevel_name = Names.(DirPath.make [Id.of_string "Top"]); + toploop = None; + + compile_list = []; + compilation_output_name = None; + + load_vernacular_list = []; + + vio_checking = false; + vio_tasks = []; + vio_files = []; + vio_files_j = 0; + + color = `AUTO; + + impredicative_set = Declarations.PredicativeSet; + stm_flags = Stm.AsyncOpts.default_opts; + debug = false; + time = false; + + filter_opts = false; + + glob_opt = false; + + memory_stat = false; + print_tags = false; + print_where = false; + print_config = false; + output_context = false; + + inputstate = None; + outputstate = None; +} + +(******************************************************************************) +(* Functional arguments *) +(******************************************************************************) +let add_ml_include opts s = + { opts with ml_includes = s :: opts.ml_includes } + +let add_vo_include opts d p implicit = + let p = Libnames.dirpath_of_string p in + { opts with vo_includes = (d, p, implicit) :: opts.vo_includes } + +let add_vo_require opts d p export = + { opts with vo_requires = (d, p, export) :: opts.vo_requires } + +let add_compat_require opts v = + match v with + | Flags.V8_5 -> add_vo_require opts "Coq.Compat.Coq85" None (Some false) + | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false) + | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false) + | Flags.VOld | Flags.Current -> opts + +let set_batch_mode opts = + Flags.quiet := true; + System.trust_file_cache := false; + { opts with batch_mode = true } + +let add_compile opts verbose s = + let opts = set_batch_mode opts in + if not opts.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 + { opts with compile_list = (s,verbose) :: opts.compile_list } + +let add_load_vernacular opts verb s = + { opts with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.load_vernacular_list } + +let add_vio_task opts f = + let opts = set_batch_mode opts in + { opts with vio_tasks = f :: opts.vio_tasks } + +let add_vio_file opts f = + let opts = set_batch_mode opts in + { opts with vio_files = f :: opts.vio_files } + +let set_vio_checking_j opts opt j = + try { opts with 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 + +(** Options for proof general *) +let set_emacs opts = + if not (Option.is_empty opts.toploop) then + CErrors.user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); + Coqloop.print_emacs := true; + Printer.enable_goal_tags_printing := true; + { opts with color = `OFF } + +let set_color opts = function +| "yes" | "on" -> { opts with color = `ON } +| "no" | "off" -> { opts with color = `OFF } +| "auto" -> { opts with color = `AUTO } +| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 + +let warn_deprecated_inputstate = + CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" + (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") + +let set_inputstate opts s = + warn_deprecated_inputstate (); + { opts with inputstate = Some s } + +let warn_deprecated_outputstate = + CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" + (fun () -> + Pp.strbrk "The outputstate option is deprecated and discouraged.") + +let set_outputstate opts s = + warn_deprecated_outputstate (); + { opts with outputstate = Some s } + +let exitcode opts = if opts.filter_opts then 2 else 0 + +(******************************************************************************) +(* Parsing helpers *) +(******************************************************************************) +let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) + +let get_bool opt = function + | "yes" | "on" -> true + | "no" | "off" -> false + | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 + +let get_int opt n = + try int_of_string n + with Failure _ -> + prerr_endline ("Error: integer expected after option "^opt); exit 1 + +let get_float opt n = + try float_of_string n + with Failure _ -> + prerr_endline ("Error: float expected after option "^opt); exit 1 + +let get_host_port opt s = + match CString.split ':' s with + | [host; portr; portw] -> + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) + | ["stdfds"] -> Some Spawned.AnonPipe + | _ -> + prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); + exit 1 + +let get_error_resilience opt = function + | "on" | "all" | "yes" -> `All + | "off" | "no" -> `None + | s -> `Only (CString.split ',' s) + +let get_priority opt s = + try CoqworkmgrApi.priority_of_string s + with Invalid_argument _ -> + prerr_endline ("Error: low/high expected after "^opt); exit 1 + +let get_async_proofs_mode opt = let open Stm.AsyncOpts in function + | "no" | "off" -> APoff + | "yes" | "on" -> APon + | "lazy" -> APonLazy + | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 + +let get_cache opt = function + | "force" -> Some Stm.AsyncOpts.Force + | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 + +let is_not_dash_option = function + | Some f when String.length f > 0 && f.[0] <> '-' -> true + | _ -> false + +let rec add_vio_args peek next oval = + if is_not_dash_option (peek ()) then + let oval = add_vio_file oval (next ()) in + add_vio_args peek next oval + else oval + +let get_native_name s = + (* We ignore even critical errors because this mode has to be super silent *) + try + String.concat "/" [Filename.dirname s; + Nativelib.output_dir; Library.native_name_from_filename s] + with _ -> "" + +(*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_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" + (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") + +exception NoCoqLib + +let usage batch = + begin + try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) + with NoCoqLib -> usage_no_coqlib () + end; + let lp = Coqinit.toplevel_init_load_path () in + (* Necessary for finding the toplevels below *) + List.iter Mltop.add_coq_path lp; + if batch 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 + +(* Main parsing routine *) +let parse_args arglist : coq_cmdopts * string list = + let args = ref arglist in + let extras = ref [] in + let rec parse oval = match !args with + | [] -> + (oval, 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 + let noval = begin match opt with + + (* Complex options with many args *) + |"-I"|"-include" -> + begin match rem with + | d :: rem -> + args := rem; + add_ml_include oval d + | [] -> error_missing_arg opt + end + |"-Q" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p false + | _ -> error_missing_arg opt + end + |"-R" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p true + | _ -> error_missing_arg opt + end + + (* Options with two arg *) + |"-check-vio-tasks" -> + let tno = get_task_list (next ()) in + let tfile = next () in + add_vio_task oval (tno,tfile) + + |"-schedule-vio-checking" -> + let oval = { oval with vio_checking = true } in + let oval = set_vio_checking_j oval opt (next ()) in + let oval = add_vio_file oval (next ()) in + add_vio_args peek_next next oval + + |"-schedule-vio2vo" -> + let oval = set_vio_checking_j oval opt (next ()) in + let oval = add_vio_file oval (next ()) in + add_vio_args peek_next next oval + + (* Options with one arg *) + |"-coqlib" -> + Flags.coqlib_spec := true; + Flags.coqlib := (next ()); + oval + + |"-async-proofs" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) + }} + |"-async-proofs-j" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) + }} + |"-async-proofs-cache" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) + }} + + |"-async-proofs-tac-j" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ())) + }} + + |"-async-proofs-worker-priority" -> + WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()); + oval + + |"-async-proofs-private-flags" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); + }} + + |"-async-proofs-tactic-error-resilience" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()) + }} + + |"-async-proofs-command-error-resilience" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ()) + }} + + |"-async-proofs-delegation-threshold" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) + }} + + |"-worker-id" -> set_worker_id opt (next ()); oval + + |"-compat" -> + let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in + Flags.compat_version := v; + add_compat_require oval v + + |"-compile" -> + add_compile oval false (next ()) + + |"-compile-verbose" -> + add_compile oval true (next ()) + + |"-dump-glob" -> + Dumpglob.dump_into_file (next ()); + { oval with glob_opt = true } + + |"-feedback-glob" -> + Dumpglob.feedback_glob (); oval + + |"-exclude-dir" -> + System.exclude_directory (next ()); oval + + |"-init-file" -> + { oval with rcfile = Some (next ()); } + + |"-inputstate"|"-is" -> + set_inputstate oval (next ()) + + |"-outputstate" -> + set_outputstate oval (next ()) + + |"-load-ml-object" -> + Mltop.dir_ml_load (next ()); oval + + |"-load-ml-source" -> + Mltop.dir_ml_use (next ()); oval + + |"-load-vernac-object" -> + add_vo_require oval (next ()) None None + + |"-load-vernac-source"|"-l" -> + add_load_vernacular oval false (next ()) + + |"-load-vernac-source-verbose"|"-lv" -> + add_load_vernacular oval true (next ()) + + |"-print-mod-uid" -> + let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 + + |"-profile-ltac-cutoff" -> + Flags.profile_ltac := true; + Flags.profile_ltac_cutoff := get_float opt (next ()); + oval + + |"-require" -> add_vo_require oval (next ()) None (Some false) + + |"-top" -> + let topname = Libnames.dirpath_of_string (next ()) in + if Names.DirPath.is_empty topname then + CErrors.user_err Pp.(str "Need a non empty toplevel module name"); + { oval with toplevel_name = topname } + + |"-main-channel" -> + Spawned.main_channel := get_host_port opt (next()); oval + + |"-control-channel" -> + Spawned.control_channel := get_host_port opt (next()); oval + + |"-vio2vo" -> + let oval = add_compile oval false (next ()) in + { oval with compilation_mode = Vio2Vo } + + |"-toploop" -> + if !Coqloop.print_emacs then + CErrors.user_err Pp.(str "Flags -toploop and -emacs are incompatible"); + { oval with toploop = Some (next ()) } + + |"-w" | "-W" -> + let w = next () in + if w = "none" then + (CWarnings.set_flags w; oval) + else + let w = CWarnings.get_flags () ^ "," ^ w in + CWarnings.set_flags (CWarnings.normalize_flags_string w); + oval + + |"-o" -> { oval with compilation_output_name = Some (next()) } + + (* Options with zero arg *) + |"-async-queries-always-delegate" + |"-async-proofs-always-delegate" + |"-async-proofs-full" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_full = true; + }} + |"-async-proofs-never-reopen-branch" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_never_reopen_branch = true + }} + |"-batch" -> set_batch_mode oval + |"-test-mode" -> Flags.test_mode := true; oval + |"-beautify" -> Flags.beautify := true; oval + |"-boot" -> Flags.boot := true; { oval with load_rcfile = false; } + |"-bt" -> Backtrace.record_backtrace true; oval + |"-color" -> set_color oval (next ()) + |"-config"|"--config" -> { oval with print_config = true } + |"-debug" -> Coqinit.set_debug (); oval + |"-stm-debug" -> Stm.stm_debug := true; oval + |"-emacs" -> set_emacs oval + |"-filteropts" -> { oval with filter_opts = true } + |"-ideslave" -> + if !Coqloop.print_emacs then + CErrors.user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); + Flags.ide_slave := true; + { oval with toploop = Some "coqidetop" } + + |"-impredicative-set" -> + { oval with impredicative_set = Declarations.ImpredicativeSet } + |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval + |"-m"|"--memory" -> { oval with memory_stat = true } + |"-noinit"|"-nois" -> { oval with load_init = false } + |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true } + |"-native-compiler" -> + if not Coq_config.native_compiler then + warning "Native compilation was disabled at configure time." + else Flags.output_native_objects := true; oval + |"-output-context" -> { oval with output_context = true } + |"-profile-ltac" -> Flags.profile_ltac := true; oval + |"-q" -> { oval with load_rcfile = false; } + |"-quiet"|"-silent" -> + Flags.quiet := true; + Flags.make_warn false; + oval + |"-quick" -> { oval with compilation_mode = BuildVio } + |"-list-tags" -> { oval with print_tags = true } + |"-time" -> { oval with time = true } + |"-type-in-type" -> set_type_in_type (); oval + |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) + |"-where" -> { oval with print_where = true } + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage oval.batch_mode; oval + |"-v"|"--version" -> Usage.version (exitcode oval) + |"-print-version"|"--print-version" -> + Usage.machine_readable_version (exitcode oval) + + (* Unknown option *) + | s -> + extras := s :: !extras; + oval + end in + parse noval + in + try + parse init_args + with any -> fatal_error any diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli new file mode 100644 index 000000000..8ee1a8f55 --- /dev/null +++ b/toplevel/coqargs.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type compilation_mode = BuildVo | BuildVio | Vio2Vo +type color = [`ON | `AUTO | `OFF] + +type coq_cmdopts = { + + load_init : bool; + load_rcfile : bool; + rcfile : string option; + + ml_includes : string list; + vo_includes : (string * Names.DirPath.t * bool) list; + vo_requires : (string * string option * bool option) list; + + (* Fuse these two? Currently, [batch_mode] is only used to + distinguish coqc / coqtop in help display. *) + batch_mode : bool; + compilation_mode : compilation_mode; + + toplevel_name : Names.DirPath.t; + toploop : string option; + + compile_list: (string * bool) list; (* bool is verbosity *) + compilation_output_name : string option; + + load_vernacular_list : (string * bool) list; + + vio_checking: bool; + vio_tasks : (int list * string) list; + vio_files : string list; + vio_files_j : int; + + color : color; + + impredicative_set : Declarations.set_predicativity; + stm_flags : Stm.AsyncOpts.stm_opt; + debug : bool; + time : bool; + + filter_opts : bool; + + glob_opt : bool; + + memory_stat : bool; + print_tags : bool; + print_where : bool; + print_config: bool; + output_context : bool; + + inputstate : string option; + outputstate : string option; + +} + +val parse_args : string list -> coq_cmdopts * string list +val exitcode : coq_cmdopts -> int diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 10205964a..8574092b8 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -20,21 +20,15 @@ let set_debug () = does not exist. *) let rcdefaultname = "coqrc" -let rcfile = ref "" -let rcfile_specified = ref false -let set_rcfile s = rcfile := s; rcfile_specified := true -let load_rc = ref true -let no_load_rc () = load_rc := false - -let load_rcfile ~time doc sid = - if !load_rc then +let load_rcfile ~rcfile ~time doc sid = try - if !rcfile_specified then - if CUnix.file_readable_p !rcfile then - Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid !rcfile - else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) - else + match rcfile with + | Some rcfile -> + if CUnix.file_readable_p rcfile then + Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid rcfile + else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) + | None -> try let warn x = Feedback.msg_warning (str x) in let inferedrc = List.find CUnix.file_readable_p [ @@ -54,9 +48,6 @@ let load_rcfile ~time doc sid = let reraise = CErrors.push reraise in let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise - else - (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); - doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = @@ -77,13 +68,6 @@ let build_userlib_path ~unix_path = } } -(* Options -I, -I-as, and -R of the command line *) -let includes = ref [] -let push_include s alias implicit = - includes := (s, alias, implicit) :: !includes -let ml_includes = ref [] -let push_ml_include s = ml_includes := s :: !ml_includes - let ml_path_if c p = let open Mltop in let f x = { recursive = false; path_spec = MlPath x } in @@ -128,17 +112,7 @@ let libs_init_load_path ~load_init = coq_path = Libnames.default_root_prefix; implicit = false; has_ml = AddTopML } - } ] @ - - (* additional loadpaths, given with options -Q and -R *) - List.map - (fun (unix_path, coq_path, implicit) -> - { recursive = true; - path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) - (List.rev !includes) @ - - (* additional ml directories, given with option -I *) - List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev !ml_includes) + } ] (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 0d2da84bb..0ceba5b38 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -10,19 +10,12 @@ val set_debug : unit -> unit -val set_rcfile : string -> unit - -val no_load_rc : unit -> unit -val load_rcfile : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t - -val push_include : string -> Names.DirPath.t -> bool -> unit -(** [push_include phys_path log_path implicit] *) - -val push_ml_include : string -> unit +val load_rcfile : rcfile:(string option) -> time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) val toplevel_init_load_path : unit -> Mltop.coq_path list + (* LoadPath for Coq user libraries *) val libs_init_load_path : load_init:bool -> Mltop.coq_path list diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 400f7048d..9058f0846 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -7,8 +7,7 @@ (************************************************************************) open Pp -open CErrors -open Libnames +open Coqargs let () = at_exit flush_all @@ -31,66 +30,21 @@ let print_header () = let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) -let toploop = ref None - -let color : [`ON | `AUTO | `OFF] ref = ref `AUTO -let set_color = function -| "yes" | "on" -> color := `ON -| "no" | "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 && - (* emacs compilation buffer does not support colors by default, - its TERM variable is set to "dumb". *) - try Sys.getenv "TERM" <> "dumb" with Not_found -> false - 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 *) - Topfmt.init_terminal_output ~color:true - | Some "" -> - (** No color output *) - Topfmt.init_terminal_output ~color:false - | Some s -> - (** Overwrite all colors *) - Topfmt.clear_styles (); - Topfmt.parse_color_config s; - Topfmt.init_terminal_output ~color:true - end - else - Topfmt.init_terminal_output ~color:false - -let toploop_init = ref begin fun x -> - let () = init_color () in - let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in - x - end - (* Feedback received in the init stage, this is different as the STM will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) let coqtop_init_feed = Coqloop.coqloop_feed let drop_last_doc = ref None -let measure_time = ref false (* Default toplevel loop *) -let console_toploop_run doc = +let console_toploop_run opts doc = (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in if Dumpglob.dump () then begin Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - let doc = Coqloop.loop ~time:!measure_time doc in + let doc = Coqloop.loop ~time:opts.time doc in (* Initialise and launch the Ocaml toplevel *) drop_last_doc := Some doc; Coqinit.init_ocaml_path(); @@ -100,10 +54,7 @@ let console_toploop_run doc = let toploop_run = ref console_toploop_run -let output_context = ref false - let memory_stat = ref false - let print_memory_stat () = begin (* -m|--memory from the command-line *) if !memory_stat then @@ -124,133 +75,87 @@ let print_memory_stat () = let _ = at_exit print_memory_stat (******************************************************************************) -(* Engagement *) -(******************************************************************************) -let impredicative_set = ref Declarations.PredicativeSet -let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet -let set_type_in_type () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_universes = false } -let engage () = - Global.set_engagement !impredicative_set - -(******************************************************************************) -(* Interactive toplevel name *) -(******************************************************************************) -let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) -let toplevel_name = ref toplevel_default_name -let set_toplevel_name dir = - if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); - toplevel_name := dir - -(******************************************************************************) (* Input/Output State *) (******************************************************************************) -let warn_deprecated_inputstate = - CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" - (fun () -> strbrk "The inputstate option is deprecated and discouraged.") - -let inputstate = ref "" -let set_inputstate s = - warn_deprecated_inputstate (); - inputstate:=s -let inputstate () = - if not (CString.is_empty !inputstate) then - let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in - States.intern_state fname - -let warn_deprecated_outputstate = - CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" - (fun () -> - strbrk "The outputstate option is deprecated and discouraged.") - -let outputstate = ref "" -let set_outputstate s = - warn_deprecated_outputstate (); - outputstate:=s -let outputstate () = - if not (CString.is_empty !outputstate) then - let fname = CUnix.make_suffix !outputstate ".coq" in - States.extern_state fname +let inputstate opts = + Option.iter (fun istate_file -> + let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in + States.intern_state fname) opts.inputstate + +let outputstate opts = + Option.iter (fun ostate_file -> + let fname = CUnix.make_suffix ostate_file ".coq" in + States.extern_state fname) opts.outputstate (******************************************************************************) (* Interactive Load File Simulation *) (******************************************************************************) -let load_vernacular_list = ref ([] : (string * bool) list) - -let add_load_vernacular verb s = - load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list - -let load_vernacular ~time doc sid = +let load_vernacular opts doc sid = List.fold_left (fun (doc,sid) (f_in, verbosely) -> let s = Loadpath.locate_file f_in in if !Flags.beautify then - Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid) f_in + Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid) f_in else - Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid s) - (doc, sid) (List.rev !load_vernacular_list) - -let load_init_vernaculars ~time doc sid = - let doc, sid = Coqinit.load_rcfile ~time doc sid in - load_vernacular ~time doc sid + Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid s) + (doc, sid) (List.rev opts.load_vernacular_list) + +let load_init_vernaculars opts doc sid = + let doc, sid = if opts.load_rcfile then + Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time doc sid + else begin + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + doc,sid + end in + load_vernacular opts doc sid (******************************************************************************) -(* Required Modules *) +(* Startup LoadPath and Modules *) (******************************************************************************) -let set_include d p implicit = - let p = dirpath_of_string p in - Coqinit.push_include d p implicit +(* prelude_data == From Coq Require Export Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some true -(* None = No Import; Some false = Import; Some true = Export *) -let require_list = ref ([] : (string * string option * bool option) list) -let add_require s = require_list := s :: !require_list +let require_libs opts = + if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires -let load_init = ref true +let cmdline_load_path opts = + let open Mltop in + (* loadpaths given by options -Q and -R *) + List.map + (fun (unix_path, coq_path, implicit) -> + { recursive = true; + path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) + (List.rev opts.vo_includes) @ -(* From Coq Require Import Prelude. *) -let prelude_data = "Prelude", Some "Coq", Some true + (* additional ml directories, given with option -I *) + List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev opts.ml_includes) -let require_libs () = - if !load_init then prelude_data :: !require_list else !require_list - -let add_compat_require v = - match v with - | Flags.V8_5 -> add_require ("Coq.Compat.Coq85", None, Some false) - | Flags.V8_6 -> add_require ("Coq.Compat.Coq86", None, Some false) - | Flags.V8_7 -> add_require ("Coq.Compat.Coq87", None, Some false) - | Flags.VOld | Flags.Current -> () +let build_load_path opts = + Coqinit.libs_init_load_path ~load_init:opts.load_init @ + cmdline_load_path opts (******************************************************************************) -(* File Compilation *) +(* Fatal Errors *) (******************************************************************************) -let glob_opt = ref false - -let compile_list = ref ([] : (bool * string) list) - -type compilation_mode = BuildVo | BuildVio | Vio2Vo -let compilation_mode = ref BuildVo -let compilation_output_name = ref None - -let batch_mode = ref false -let set_batch_mode () = - System.trust_file_cache := false; - batch_mode := true - -let add_compile verbose s = - set_batch_mode (); - Flags.quiet := 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 +(** Prints info which is either an error or an anomaly and then exits + with the appropriate error code *) +let fatal_error msg = + Topfmt.std_logger Feedback.Error msg; + flush_all (); + exit 1 + +let fatal_error_exn ?extra exn = + Topfmt.print_err_exn ?extra exn; + flush_all (); + let exit_code = + if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in - compile_list := (verbose,s) :: !compile_list + exit exit_code +(******************************************************************************) +(* File Compilation *) +(******************************************************************************) let warn_file_no_extension = CWarnings.create ~name:"file-no-extension" ~category:"filesystem" (fun (f,ext) -> @@ -268,16 +173,11 @@ let ensure_ext ext f = let chop_extension f = try Filename.chop_extension f with _ -> f -let compile_error msg = - Topfmt.std_logger Feedback.Error msg; - flush_all (); - exit 1 - let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in if src <> tgt then - compile_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + fatal_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ str "Source: " ++ str src ++ fnl () ++ str "Target: " ++ str tgt) @@ -289,25 +189,23 @@ let ensure_vio v vio = ensure ".vio" v vio let ensure_exists f = if not (Sys.file_exists f) then - compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) - -let top_stm_options = ref Stm.AsyncOpts.default_opts + fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) -let compile ~time ~verbosely ~f_in ~f_out = +let compile opts ~verbosely ~f_in ~f_out = let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in if not (CList.is_empty pfs) then - compile_error (str "There are pending proofs: " + fatal_error (str "There are pending proofs: " ++ (pfs |> List.rev |> prlist_with_sep pr_comma Names.Id.print) ++ str ".") in - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in - let require_libs = require_libs () in - let stm_options = !top_stm_options in - match !compilation_mode with + let iload_path = build_load_path opts in + let require_libs = require_libs opts in + let stm_options = opts.stm_flags in + match opts.compilation_mode with | BuildVo -> Flags.record_aux_file := true; let long_f_dot_v = ensure_v f_in in @@ -319,12 +217,10 @@ let compile ~time ~verbosely ~f_in ~f_out = let doc, sid = Stm.(new_doc { doc_type = VoDoc long_f_dot_vo; - iload_path; - require_libs; - stm_options; + iload_path; require_libs; stm_options; }) in - let doc, sid = load_init_vernaculars ~time doc sid in + let doc, sid = load_init_vernaculars opts doc sid in let ldir = Stm.get_ldir ~doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) @@ -332,7 +228,7 @@ let compile ~time ~verbosely ~f_in ~f_out = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in + let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in let _doc = Stm.join ~doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -354,17 +250,26 @@ let compile ~time ~verbosely ~f_in ~f_out = | None -> long_f_dot_v ^ "io" | Some f -> ensure_vio long_f_dot_v f in + (* We need to disable error resiliency, otherwise some errors + will be ignored in batch mode. c.f. #6707 + + This is not necessary in the vo case as it fully checks the + document anyways. *) + let stm_options = let open Stm.AsyncOpts in + { stm_options with + async_proofs_cmd_error_resilience = false; + async_proofs_tac_error_resilience = `None; + } in + let doc, sid = Stm.(new_doc { doc_type = VioDoc long_f_dot_vio; - iload_path; - require_libs; - stm_options; + iload_path; require_libs; stm_options; }) in - let doc, sid = load_init_vernaculars ~time doc sid in + let doc, sid = load_init_vernaculars opts doc sid in let ldir = Stm.get_ldir ~doc in - let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in + let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in let doc = Stm.finish ~doc in check_pending_proofs (); let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in @@ -379,91 +284,96 @@ let compile ~time ~verbosely ~f_in ~f_out = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile ~time ~verbosely ~f_in ~f_out = +let compile opts ~verbosely ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile ~time ~verbosely ~f_in ~f_out; + compile opts ~verbosely ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file (verbosely,f_in) = +let compile_file opts (f_in, verbosely) = if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile ~verbosely ~f_in ~f_out:None) f_in + (fun f_in -> compile opts ~verbosely ~f_in ~f_out:None) f_in else - compile ~verbosely ~f_in ~f_out:None + compile opts ~verbosely ~f_in ~f_out:None -let compile_files ~time = - if !compile_list == [] then () - else List.iter (compile_file ~time) (List.rev !compile_list) +let compile_files opts = + let compile_list = List.rev opts.compile_list in + List.iter (compile_file opts) compile_list (******************************************************************************) (* VIO Dispatching *) (******************************************************************************) - -let vio_tasks = ref [] -let add_vio_task f = - set_batch_mode (); - Flags.quiet := true; - vio_tasks := f :: !vio_tasks - -let check_vio_tasks () = +let check_vio_tasks opts = 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 + true (List.rev opts.vio_tasks) in + if not rc then fatal_error Pp.(str "VIO Task Check failed") (* vio files *) -let vio_files = ref [] -let vio_files_j = ref 0 -let vio_checking = ref false -let add_vio_file f = - set_batch_mode (); - Flags.quiet := 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 schedule_vio () = +let schedule_vio opts = (* We must add update the loadpath here as the scheduling process happens outside of the STM *) - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in + let iload_path = build_load_path opts in List.iter Mltop.add_coq_path iload_path; - if !vio_checking then - Vio_checking.schedule_vio_checking !vio_files_j !vio_files + if opts.vio_checking then + Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files else - Vio_checking.schedule_vio_compilation !vio_files_j !vio_files + Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files (******************************************************************************) -(* UI Options *) +(* Color Options *) (******************************************************************************) -(** Options for proof general *) - -let set_emacs () = - if not (Option.is_empty !toploop) then - user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); - Coqloop.print_emacs := true; - Printer.enable_goal_tags_printing := true; - color := `OFF - -(** Options for CoqIDE *) - -let set_ideslave () = - if !Coqloop.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); - toploop := Some "coqidetop"; - Flags.ide_slave := true +let init_color color_mode = + let has_color = match color_mode with + | `OFF -> false + | `ON -> true + | `AUTO -> + Terminal.has_style Unix.stdout && + Terminal.has_style Unix.stderr && + (* emacs compilation buffer does not support colors by default, + its TERM variable is set to "dumb". *) + try Sys.getenv "TERM" <> "dumb" with Not_found -> false + 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 *) + Topfmt.init_terminal_output ~color:true + | Some "" -> + (** No color output *) + Topfmt.init_terminal_output ~color:false + | Some s -> + (** Overwrite all colors *) + Topfmt.clear_styles (); + Topfmt.parse_color_config s; + Topfmt.init_terminal_output ~color:true + end + else + Topfmt.init_terminal_output ~color:false -(** Options for slaves *) +let toploop_init = ref begin fun opts x -> + let () = init_color opts.color in + let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in + x + end -let set_toploop name = - if !Coqloop.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible"); - toploop := Some name +let print_style_tags opts = + let () = init_color opts.color in + let tags = Topfmt.dump_tags () in + let iter (t, st) = + let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in + print_string opt + in + let make (t, st) = + let tags = List.map string_of_int (Terminal.repr st) in + (t ^ "=" ^ String.concat ";" tags) + in + let repr = List.map make tags in + let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in + let () = List.iter iter tags in + flush_all () (** GC tweaking *) @@ -490,339 +400,37 @@ let init_gc () = Gc.minor_heap_size = 33554432; (** 4M *) Gc.space_overhead = 120} -(*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_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" - (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") - -exception NoCoqLib - -let usage batch = - begin - try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) - with NoCoqLib -> usage_no_coqlib () - end; - let lp = Coqinit.toplevel_init_load_path () in - (* Necessary for finding the toplevels below *) - List.iter Mltop.add_coq_path lp; - if batch 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 = Topfmt.dump_tags () in - let iter (t, st) = - let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in - print_string opt - in - let make (t, st) = - let tags = List.map string_of_int (Terminal.repr st) in - (t ^ "=" ^ String.concat ";" tags) - in - let repr = List.map make tags in - let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in - let () = List.iter iter tags in - flush_all () - -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 filter_opts = ref false -let exitcode () = if !filter_opts then 2 else 0 - -let print_where = ref false -let print_config = ref false -let print_tags = ref false - -let get_priority opt s = - try CoqworkmgrApi.priority_of_string s - with Invalid_argument _ -> - prerr_endline ("Error: low/high expected after "^opt); exit 1 - -let get_async_proofs_mode opt = let open Stm.AsyncOpts in function - | "no" | "off" -> APoff - | "yes" | "on" -> APon - | "lazy" -> APonLazy - | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 - -let get_cache opt = function - | "force" -> Some Stm.AsyncOpts.Force - | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 - - -let set_worker_id opt s = - assert (s <> "master"); - Flags.async_proofs_worker_id := s - -let get_bool opt = function - | "yes" | "on" -> true - | "no" | "off" -> false - | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 - -let get_int opt n = - try int_of_string n - with Failure _ -> - prerr_endline ("Error: integer expected after option "^opt); exit 1 - -let get_float opt n = - try float_of_string n - with Failure _ -> - prerr_endline ("Error: float expected after option "^opt); exit 1 - -let get_host_port opt s = - match CString.split ':' s with - | [host; portr; portw] -> - Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) - | ["stdfds"] -> Some Spawned.AnonPipe - | _ -> - prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); - exit 1 - -let get_error_resilience opt = function - | "on" | "all" | "yes" -> `All - | "off" | "no" -> `None - | s -> `Only (CString.split ',' s) - -let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) - -let is_not_dash_option = function - | Some f when String.length f > 0 && f.[0] <> '-' -> true - | _ -> false - -let get_native_name s = - (* We ignore even critical errors because this mode has to be super silent *) - try - String.concat "/" [Filename.dirname s; - Nativelib.output_dir; Library.native_name_from_filename s] - with _ -> "" - -(** Prints info which is either an error or an anomaly and then exits - with the appropriate error code *) -let fatal_error ?extra exn = - Topfmt.print_err_exn ?extra exn; - let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in - exit exit_code - -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 :: rem -> Coqinit.push_ml_include d; args := rem - | [] -> error_missing_arg opt - end - |"-Q" -> - begin match rem with - | d :: p :: rem -> set_include d p false; args := rem - | _ -> error_missing_arg opt - end - |"-R" -> - begin match rem with - | d :: p :: rem -> set_include d p true; args := rem - | _ -> error_missing_arg opt - end - - (* 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" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) - } - |"-async-proofs-j" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) - } - |"-async-proofs-cache" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) - } - |"-async-proofs-tac-j" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ())) - } - |"-async-proofs-worker-priority" -> - WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()) - |"-async-proofs-private-flags" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); - } - |"-async-proofs-tactic-error-resilience" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()); - } - |"-async-proofs-command-error-resilience" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ()) - } - |"-async-proofs-delegation-threshold" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) - } - |"-worker-id" -> set_worker_id opt (next ()) - |"-compat" -> - let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in - Flags.compat_version := v; add_compat_require v - |"-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" -> System.exclude_directory (next ()) - |"-init-file" -> Coqinit.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_require (next (), None, None) - |"-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 - |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) - |"-require" -> add_require (next (), None, Some false) - |"-top" -> set_toplevel_name (dirpath_of_string (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 ()); - compilation_mode := Vio2Vo - |"-toploop" -> set_toploop (next ()) - |"-w" | "-W" -> - let w = next () in - if w = "none" then CWarnings.set_flags w - else - let w = CWarnings.get_flags () ^ "," ^ w in - CWarnings.set_flags (CWarnings.normalize_flags_string w) - |"-o" -> compilation_output_name := Some (next()) - - (* Options with zero arg *) - |"-async-queries-always-delegate" - |"-async-proofs-always-delegate" - |"-async-proofs-full" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_full = true; - } - |"-async-proofs-never-reopen-branch" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_never_reopen_branch = true; - } - |"-batch" -> set_batch_mode () - |"-test-mode" -> Flags.test_mode := true - |"-beautify" -> Flags.beautify := true - |"-boot" -> Flags.boot := true; Coqinit.no_load_rc () - |"-bt" -> Backtrace.record_backtrace true - |"-color" -> set_color (next ()) - |"-config"|"--config" -> print_config := true - |"-debug" -> Coqinit.set_debug () - |"-stm-debug" -> Stm.stm_debug := true - |"-emacs" -> set_emacs () - |"-filteropts" -> filter_opts := true - |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode - |"-ideslave" -> set_ideslave () - |"-impredicative-set" -> set_impredicative_set () - |"-indices-matter" -> Indtypes.enforce_indices_matter () - |"-m"|"--memory" -> memory_stat := true - |"-noinit"|"-nois" -> load_init := false - |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true - |"-native-compiler" -> - if not Coq_config.native_compiler then - warning "Native compilation was disabled at configure time." - else Flags.output_native_objects := true - |"-output-context" -> output_context := true - |"-profile-ltac" -> Flags.profile_ltac := true - |"-q" -> Coqinit.no_load_rc () - |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false - |"-quick" -> compilation_mode := BuildVio - |"-list-tags" -> print_tags := true - |"-time" -> measure_time := true - |"-type-in-type" -> set_type_in_type () - |"-unicode" -> add_require ("Utf8_core", None, Some false) - |"-v"|"--version" -> Usage.version (exitcode ()) - |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) - |"-where" -> print_where := true - - (* Unknown option *) - | s -> extras := s :: !extras - end; - parse () - in - try - parse () - with any -> fatal_error any - +(** Main init routine *) let init_toplevel arglist = (* Coq's init process, phase 1: - - OCaml parameters, and basic structures and IO + OCaml parameters, basic structures, and IO *) CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in Lib.init(); + (* Coq's init process, phase 2: - - Basic Coq environment, load-path, plugins. + Basic Coq environment, load-path, plugins. *) let res = begin try - let extras = parse_args arglist in + let opts,extras = parse_args arglist in + memory_stat := opts.memory_stat; + (* 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 ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); - if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ())); - if !print_tags then (print_style_tags (); exit (exitcode ())); - if !filter_opts then (print_string (String.concat "\n" extras); exit 0); + if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts)); + if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts)); + if opts.print_tags then (print_style_tags opts; exit (exitcode opts)); + if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0); let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; - Option.iter Mltop.load_ml_object_raw !toploop; - let extras = !toploop_init extras in + Option.iter Mltop.load_ml_object_raw opts.toploop; + let extras = !toploop_init opts extras in if not (CList.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"; @@ -830,10 +438,10 @@ let init_toplevel arglist = end; Flags.if_verbose print_header (); Mltop.init_known_plugins (); - engage (); + Global.set_engagement opts.impredicative_set; (* Allow the user to load an arbitrary state here *) - inputstate (); + inputstate opts; (* This state will be shared by all the documents *) Stm.init_core (); @@ -842,9 +450,7 @@ let init_toplevel arglist = It is essential that the module system is in a consistent state before we take the first snapshot. This was not - guaranteed in the past. In particular, we want to be sure we - have called start_library before loading the prelude and rest - of required files. + guaranteed in the past, but now is thanks to the STM API. We split the codepath here depending whether coqtop is called in interactive mode or not. *) @@ -852,39 +458,37 @@ let init_toplevel arglist = (* The condition for starting the interactive mode is a bit convoluted, we should really refactor batch/compilation_mode more. *) - if (not !batch_mode - || CList.(is_empty !compile_list && is_empty !vio_files && is_empty !vio_tasks)) + if (not opts.batch_mode + || CList.(is_empty opts.compile_list && is_empty opts.vio_files && is_empty opts.vio_tasks)) (* Interactive *) then begin - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in - let require_libs = require_libs () in - let stm_options = !top_stm_options in - try - let doc, sid = Stm.(new_doc - { doc_type = Interactive !toplevel_name; - iload_path; - require_libs; - stm_options; - }) in - Some (load_init_vernaculars ~time:!measure_time doc sid) - with any -> flush_all(); fatal_error any - (* Non interactive *) + let iload_path = build_load_path opts in + let require_libs = require_libs opts in + let stm_options = opts.stm_flags in + try let doc, sid = + Stm.(new_doc + { doc_type = Interactive opts.toplevel_name; + iload_path; require_libs; stm_options; + }) in + Some (load_init_vernaculars opts doc sid), opts + with any -> flush_all(); fatal_error_exn any + (* Non interactive: we perform a sequence of compilation steps *) end else begin try - compile_files ~time:!measure_time; + compile_files opts; (* Vio compile pass *) - if !vio_files <> [] then schedule_vio (); + if opts.vio_files <> [] then schedule_vio opts; (* Vio task pass *) - check_vio_tasks (); + check_vio_tasks opts; (* Allow the user to output an arbitrary state *) - outputstate (); - None - with any -> flush_all(); fatal_error any + outputstate opts; + None, opts + with any -> flush_all(); fatal_error_exn any end; with any -> flush_all(); let extra = Some (str "Error during initialization: ") in - fatal_error ?extra any + fatal_error_exn ?extra any end in Feedback.del_feeder init_feeder; res @@ -892,12 +496,12 @@ let init_toplevel arglist = let start () = match init_toplevel (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) - | Some (doc, sid) when not !batch_mode -> - !toploop_run doc; + | Some (doc, sid), opts when not opts.batch_mode -> + !toploop_run opts doc; exit 1 - | _ -> + | _ , opts -> flush_all(); - if !output_context then begin + if opts.output_context then begin let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 5b9494eaa..4d625a03d 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -11,7 +11,7 @@ state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [Coqloop.loop]. *) -val init_toplevel : string list -> (Stm.doc * Stateid.t) option +val init_toplevel : string list -> (Stm.doc * Stateid.t) option * Coqargs.coq_cmdopts val start : unit -> unit @@ -19,6 +19,6 @@ val start : unit -> unit val drop_last_doc : Stm.doc option ref (* For other toploops *) -val toploop_init : (string list -> string list) ref -val toploop_run : (Stm.doc -> unit) ref +val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref +val toploop_run : (Coqargs.coq_cmdopts -> Stm.doc -> unit) ref diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 10bf48647..9fb2e33d7 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -2,4 +2,5 @@ Vernac Usage Coqloop Coqinit +Coqargs Coqtop diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 7e96f28de..1ad7ead72 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Feedback open Pp (** Pp control also belongs here as the terminal is private to the toplevel *) @@ -138,7 +137,7 @@ let make_body quoter info ?pre_hdr s = (* The empty quoter *) let noq x = x (* Generic logger *) -let gen_logger dbg warn ?pre_hdr level msg = match level with +let gen_logger dbg warn ?pre_hdr level msg = let open Feedback in match level with | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) | Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7223389c4..35ef4bfa4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -58,20 +58,20 @@ let show_proof () = let p = Proof_global.give_me_the_proof () in let sigma, env = Pfedit.get_current_context () in let pprf = Proof.partial_proof p in - Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) + Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma)) + pr_evars_int sigma 1 (Evd.undefined_map sigma) let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in - Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma)); - Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx) + Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ + str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx (* Simulate the Intro(s) tactic *) let show_intro all = @@ -83,11 +83,12 @@ let show_intro all = let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in - Feedback.msg_notice (hov 0 (prlist_with_sep spc Id.print lid)) + hov 0 (prlist_with_sep spc Id.print lid) else if not (List.is_empty l) then let n = List.last l in - Feedback.msg_notice (Id.print (List.hd (Tactics.find_intro_names [n] gl))) - end + Id.print (List.hd (Tactics.find_intro_names [n] gl)) + else mt () + end else mt () (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -146,8 +147,8 @@ let show_match id = let pr_branch l = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" in - Feedback.msg_notice (v 1 (str "match # with" ++ fnl () ++ - prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())) + v 1 (str "match # with" ++ fnl () ++ + prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ()) (* "Print" commands *) @@ -186,21 +187,21 @@ let print_module r = let globdir = Nametab.locate_dir qid in match globdir with DirModule { obj_dir; obj_mp; _ } -> - Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp) + Printmod.print_module (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with - Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) let print_modtype r = let (loc,qid) = qualid_of_reference r in try let kn = Nametab.locate_modtype qid in - Feedback.msg_notice (Printmod.print_modtype kn) + Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - Feedback.msg_notice (Printmod.print_module false mp) + Printmod.print_module false mp with Not_found -> user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) @@ -272,7 +273,7 @@ let print_namespace ns = acc ) constants (str"") in - Feedback.msg_notice ((print_list Id.print ns)++str":"++fnl()++constants_in_namespace) + (print_list Id.print ns)++str":"++fnl()++constants_in_namespace let print_strategy r = let open Conv_oracle in @@ -302,7 +303,7 @@ let print_strategy r = else str "Constant strategies" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_strategy cst_lvl) in - Feedback.msg_notice (var_msg ++ cst_msg) + var_msg ++ cst_msg | Some r -> let r = Smartlocate.smart_global r in let key = match r with @@ -311,7 +312,7 @@ let print_strategy r = | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable") in let lvl = get_strategy oracle key in - Feedback.msg_notice (pr_strategy (r, lvl)) + pr_strategy (r, lvl) let dump_universes_gen g s = let output = open_out s in @@ -345,7 +346,7 @@ let dump_universes_gen g s = try UGraph.dump_universes output_constraint g; close (); - Feedback.msg_info (str "Universes written to file \"" ++ str s ++ str "\".") + str "Universes written to file \"" ++ str s ++ str "\"." with reraise -> let reraise = CErrors.push reraise in close (); @@ -360,12 +361,9 @@ let locate_file f = let msg_found_library = function | Library.LibLoaded, fulldir, file -> - Feedback.msg_info (hov 0 - (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ - str file)) + hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file) | Library.LibInPath, fulldir, file -> - Feedback.msg_info (hov 0 - (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)) + hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) let err_unmapped_library ?loc ?from qid = let dir = fst (repr_qualid qid) in @@ -944,7 +942,6 @@ let vernac_chdir = function end; Flags.if_verbose Feedback.msg_info (str (Sys.getcwd())) - (********************) (* State management *) @@ -1595,9 +1592,9 @@ let vernac_check_may_eval ~atts redexp glopt rc = let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in - Feedback.msg_notice (print_judgment env sigma' j ++ - pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx_set sigma uctx) + print_judgment env sigma' j ++ + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ + Printer.pr_universe_ctx_set sigma uctx | Some r -> let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = @@ -1605,7 +1602,7 @@ let vernac_check_may_eval ~atts redexp glopt rc = let (_, c) = redfun env evm c in c in - Feedback.msg_notice (print_eval redfun env sigma' rc j) + print_eval redfun env sigma' rc j let vernac_declare_reduction ~atts s r = let local = make_locality atts.locality in @@ -1621,8 +1618,8 @@ let vernac_global_check c = let senv = Safe_typing.push_context_set false uctx senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - Feedback.msg_notice (print_safe_judgment env sigma j ++ - pr_universe_ctx_set sigma uctx) + print_safe_judgment env sigma j ++ + pr_universe_ctx_set sigma uctx let get_nth_goal n = @@ -1630,7 +1627,7 @@ let get_nth_goal n = let gls,_,_,_,sigma = Proof.proof pf in let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in gl - + exception NoHyp (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the @@ -1664,31 +1661,32 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~atts env sigma = - let open Feedback in let loc = atts.loc in function - | PrintTables -> msg_notice (print_tables ()) - | PrintFullContext-> msg_notice (print_full_context_typ env sigma) - | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid) - | PrintInspect n -> msg_notice (inspect env sigma n) - | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent) - | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir) - | PrintModules -> msg_notice (print_modules ()) + | PrintTables -> print_tables () + | PrintFullContext-> print_full_context_typ env sigma + | PrintSectionContext qid -> print_sec_context_typ env sigma qid + | PrintInspect n -> inspect env sigma n + | PrintGrammar ent -> Metasyntax.pr_grammar ent + | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir + | PrintModules -> print_modules () | PrintModule qid -> print_module qid | PrintModuleType qid -> print_modtype qid | PrintNamespace ns -> print_namespace ns - | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ()) - | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) - | PrintDebugGC -> msg_notice (Mltop.print_gc ()) - | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) - | PrintGraph -> msg_notice (Prettyp.print_graph env sigma) - | PrintClasses -> msg_notice (Prettyp.print_classes()) - | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) - | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) - | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) + | PrintMLLoadPath -> Mltop.print_ml_path () + | PrintMLModules -> Mltop.print_ml_modules () + | PrintDebugGC -> Mltop.print_gc () + | PrintName (qid,udecl) -> + dump_global qid; + print_name env sigma qid udecl + | PrintGraph -> Prettyp.print_graph env sigma + | PrintClasses -> Prettyp.print_classes() + | PrintTypeClasses -> Prettyp.print_typeclasses() + | PrintInstances c -> Prettyp.print_instances (smart_global c) + | PrintCoercions -> Prettyp.print_coercions env sigma | PrintCoercionPaths (cls,clt) -> - msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)) - | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) + Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt) + | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma | PrintUniverses (b, dst) -> let univ = Global.universes () in let univ = if b then UGraph.sort_universes univ else univ in @@ -1697,23 +1695,24 @@ let vernac_print ~atts env sigma = else str"There may remain asynchronous universe constraints" in begin match dst with - | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) + | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining | Some s -> dump_universes_gen univ s end - | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r)) - | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) - | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s) - | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma) + | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) + | PrintHintGoal -> Hints.pr_applicable_hint () + | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s + | PrintHintDb -> Hints.pr_searchtable env sigma | PrintScopes -> - msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env))) + Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)) | PrintScope s -> - msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s) + Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s | PrintVisibility s -> - msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s) + Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> - msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt) + print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt | PrintImplicit qid -> - dump_global qid; msg_notice (print_impargs qid) + dump_global qid; + print_impargs qid | PrintAssumptions (o,t,r) -> (* Prints all the axioms and section variables used by a term *) let gr = smart_global r in @@ -1721,7 +1720,7 @@ let vernac_print ~atts env sigma = let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in - msg_notice (Printer.pr_assumptionset env sigma nassums) + Printer.pr_assumptionset env sigma nassums | PrintStrategy r -> print_strategy r let global_module r = @@ -1807,19 +1806,18 @@ let vernac_search ~atts s gopt r = | SearchAbout sl -> (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search -let vernac_locate = let open Feedback in function - | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) - | LocateTerm (AN qid) -> msg_notice (print_located_term qid) +let vernac_locate = function + | LocateAny (AN qid) -> print_located_qualid qid + | LocateTerm (AN qid) -> print_located_term qid | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *) | LocateTerm (ByNotation (_, (ntn, sc))) -> let _, env = Pfedit.get_current_context () in - msg_notice - (Notation.locate_notation - (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc) + Notation.locate_notation + (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc | LocateLibrary qid -> print_located_library qid - | LocateModule qid -> msg_notice (print_located_module qid) - | LocateOther (s, qid) -> msg_notice (print_located_other s qid) - | LocateFile f -> msg_notice (locate_file f) + | LocateModule qid -> print_located_module qid + | LocateOther (s, qid) -> print_located_other s qid + | LocateFile f -> locate_file f let vernac_register id r = if Proof_global.there_are_pending_proofs () then @@ -1851,7 +1849,7 @@ let vernac_unfocus () = let vernac_unfocused () = let p = Proof_global.give_me_the_proof () in if Proof.unfocused p then - Feedback.msg_notice (str"The proof is indeed fully unfocused.") + str"The proof is indeed fully unfocused." else user_err Pp.(str "The proof is not fully unfocused.") @@ -1878,21 +1876,20 @@ let vernac_bullet (bullet : Proof_bullet.t) = Proof_global.simple_with_current_proof (fun _ p -> Proof_bullet.put p bullet) -let vernac_show = let open Feedback in function +let vernac_show = function | ShowScript -> assert false (* Only the stm knows the script *) | ShowGoal goalref -> let proof = Proof_global.give_me_the_proof () in - let info = match goalref with - | OpenSubgoals -> pr_open_subgoals ~proof - | NthGoal n -> pr_nth_open_subgoal ~proof n - | GoalId id -> pr_goal_by_id ~proof id - in - msg_notice info + begin match goalref with + | OpenSubgoals -> pr_open_subgoals ~proof + | NthGoal n -> pr_nth_open_subgoal ~proof n + | GoalId id -> pr_goal_by_id ~proof id + end | ShowProof -> show_proof () | ShowExistentials -> show_top_evars () | ShowUniverses -> show_universes () | ShowProofNames -> - msg_notice (pr_sequence Id.print (Proof_global.get_all_proof_names())) + pr_sequence Id.print (Proof_global.get_all_proof_names()) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id @@ -1907,8 +1904,7 @@ let vernac_check_guard () = (str "The condition holds up to here") with UserError(_,s) -> (str ("Condition violated: ") ++s) - in - Feedback.msg_notice message + in message exception End_of_input @@ -2063,26 +2059,32 @@ let interp ?proof ~atts ~st c = | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key - | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~atts r g c + | VernacCheckMayEval (r,g,c) -> + Feedback.msg_notice @@ vernac_check_may_eval ~atts r g c | VernacDeclareReduction (s,r) -> vernac_declare_reduction ~atts s r - | VernacGlobalCheck c -> vernac_global_check c + | VernacGlobalCheck c -> + Feedback.msg_notice @@ vernac_global_check c | VernacPrint p -> let sigma, env = Pfedit.get_current_context () in - vernac_print ~atts env sigma p + Feedback.msg_notice @@ vernac_print ~atts env sigma p | VernacSearch (s,g,r) -> vernac_search ~atts s g r - | VernacLocate l -> vernac_locate l + | VernacLocate l -> + Feedback.msg_notice @@ vernac_locate l | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n") (* Proof management *) | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () - | VernacUnfocused -> vernac_unfocused () + | VernacUnfocused -> + Feedback.msg_notice @@ vernac_unfocused () | VernacBullet b -> vernac_bullet b | VernacSubproof n -> vernac_subproof n | VernacEndSubproof -> vernac_end_subproof () - | VernacShow s -> vernac_show s - | VernacCheckGuard -> vernac_check_guard () + | VernacShow s -> + Feedback.msg_notice @@ vernac_show s + | VernacCheckGuard -> + Feedback.msg_notice @@ vernac_check_guard () | VernacProof (tac, using) -> let using = Option.append using (Proof_using.get_default_proof_using ()) in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in @@ -2277,8 +2279,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = then Flags.verbosely control c else control c -(* XXX: There is a bug here in case of an exception, see @gares - comments on the PR *) +(* Be careful with the cache here in case of an exception. *) let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; try |