diff options
69 files changed, 299 insertions, 359 deletions
diff --git a/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst new file mode 100644 index 0000000000..77fa556321 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst @@ -0,0 +1,9 @@ +- **Changed:** + Recursive OCaml loadpaths are not supported anymore; the command + ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the + preferred one. We have also dropped support for the non-qualified + version of the :cmd:`Add LoadPath` command, that is to say, + the ``Add LoadPath dir`` version; now, + you must always specify a prefix now using ``Add Loadpath dir as Prefix.`` + (`#11618 <https://github.com/coq/coq/pull/11618>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a38c26c2b3..d1f3dcc309 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -745,11 +745,6 @@ the toplevel, and using them in source files is discouraged. :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. - .. cmdv:: Add LoadPath @string - - Performs as :n:`Add LoadPath @string @dirpath` but - for the empty directory path. - .. cmd:: Add Rec LoadPath @string as @dirpath @@ -757,11 +752,6 @@ the toplevel, and using them in source files is discouraged. :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. - .. cmdv:: Add Rec LoadPath @string - - Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty - logical directory path. - .. cmd:: Remove LoadPath @string @@ -784,12 +774,6 @@ the toplevel, and using them in source files is discouraged. loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`). -.. cmd:: Add Rec ML Path @string - - This command adds the directory :n:`@string` and all its subdirectories to - the current OCaml loadpath (see the command :cmd:`Declare ML Module`). - - .. cmd:: Print ML Path @string This command displays the current OCaml loadpath. This diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 1caf2c2722..76d98c5ddd 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -89,12 +89,12 @@ struct let catch = fun s h -> (); fun () -> try s () with Exception e as src -> - let (src, info) = CErrors.push src in + let (src, info) = Exninfo.capture src in h (e, info) () let read_line = fun () -> try read_line () with e -> - let (e, info) = CErrors.push e in - raise (e, info) () + let (e, info) = Exninfo.capture e in + raise (e,info) () let print_char = fun c -> (); fun () -> print_char c @@ -104,8 +104,8 @@ struct let make f = (); fun () -> try f () with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in - Util.iraise (Exception e, info) + let (e, info) = Exninfo.capture e in + Exninfo.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) let print_debug s = make (fun _ -> Feedback.msg_debug s) @@ -115,8 +115,8 @@ struct let run = fun x -> try x () with Exception e as src -> - let (src, info) = CErrors.push src in - Util.iraise (e, info) + let (src, info) = Exninfo.capture src in + Exninfo.iraise (e, info) end (** {6 Logical layer} *) diff --git a/engine/proofview.ml b/engine/proofview.ml index a26ce71141..6a4e490408 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -228,7 +228,7 @@ let apply ~name ~poly env t sp = let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in let ans = Logic_monad.NonLogical.run ans in match ans with - | Nil (e, info) -> iraise (TacticFailure e, info) + | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info) | Cons ((r, (state, _), status, info), _) -> let (status, gaveup) = status in let status = (status, state.shelf, gaveup) in @@ -328,8 +328,8 @@ let tclEXACTLY_ONCE e t = (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) type 'a case = -| Fail of iexn -| Next of 'a * (iexn -> 'a tactic) +| Fail of Exninfo.iexn +| Next of 'a * (Exninfo.iexn -> 'a tactic) let tclCASE t = let open Logic_monad in let map = function @@ -1096,7 +1096,7 @@ module Goal = struct let (gl, sigma) = nf_gmake env sigma goal in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end end @@ -1114,7 +1114,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end end @@ -1127,7 +1127,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end | _ -> @@ -1218,7 +1218,7 @@ module V82 = struct InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >> Pv.set { ps with solution = evd; comb = sgs; } with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e @@ -1261,8 +1261,8 @@ module V82 = struct let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) let put_status = Status.put @@ -1271,7 +1271,7 @@ module V82 = struct let wrap_exceptions f = try f () with e when catchable_exception e -> - let (e, info) = CErrors.push e in tclZERO ~info e + let (e, info) = Exninfo.capture e in tclZERO ~info e end diff --git a/engine/proofview.mli b/engine/proofview.mli index a92179ab5b..5bfbc6a649 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -14,7 +14,6 @@ ['a tactic] is the (abstract) type of tactics modifying the proof state and returning a value of type ['a]. *) -open Util open EConstr (** Main state of tactics *) @@ -194,18 +193,18 @@ val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic the successes of [t1] have been depleted and it failed with [e], then it behaves as [t2 e]. In other words, [tclOR] inserts a backtracking point. *) -val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic +val tclOR : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic (** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one success or [t2 e] if [t1] fails with [e]. It is analogous to [try/with] handler of exception in that it is not a backtracking point. *) -val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic +val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic (** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a] fails with [e], then it behaves as [f e]. *) -val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic +val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails @@ -227,8 +226,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic continuation. It is the most general primitive to control backtracking. *) type 'a case = - | Fail of iexn - | Next of 'a * (iexn -> 'a tactic) + | Fail of Exninfo.iexn + | Next of 'a * (Exninfo.iexn -> 'a tactic) val tclCASE : 'a tactic -> 'a case tactic (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of @@ -236,7 +235,7 @@ val tclCASE : 'a tactic -> 'a case tactic failure with an exception [e] such that [p e = Some e'] is raised. At which point it drops the remaining successes, failing with [e']. [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *) -val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic +val tclBREAK : (Exninfo.iexn -> Exninfo.iexn option) -> 'a tactic -> 'a tactic (** {7 Focusing tactics} *) @@ -508,8 +507,8 @@ end module UnsafeRepr : sig type state = Proofview_monad.Logical.Unsafe.state - val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t - val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic + val repr : 'a tactic -> ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t + val make : ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t -> 'a tactic end (** {6 Goal-dependent tactics} *) diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 5b9ea17ba7..790b427e4c 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -21,7 +21,6 @@ let commands = [ "Add Printing Let"; "Add Printing Record"; "Add Rec LoadPath"; - "Add Rec ML Path"; "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. "; "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]."; "Add Relation"; diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index dfc16d39f3..4292e91252 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.ml @@ -327,11 +327,7 @@ let main = { xml_printer = op; xml_parser = ip } in let init () = match base_eval_call ~print:false (Xmlprotocol.init None) coq with - | Interface.Good id -> - let dir = Filename.dirname input_file in - let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in - let eid, tip = add_sentence ~name:"initial" phrase in - after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq) + | Interface.Good id -> () | Interface.Fail _ -> error "init call failed" in let finish () = match base_eval_call (Xmlprotocol.status true) coq with diff --git a/ide/idetop.ml b/ide/idetop.ml index 9eb0b972b6..57e9792845 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -69,7 +69,7 @@ let ide_cmd_checks ~last_valid { CAst.loc; v } = let user_error s = try CErrors.user_err ?loc ~hdr:"IDE" (str s) with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Stateid.add info ~valid:last_valid Stateid.dummy in Exninfo.iraise (e, info) in @@ -477,7 +477,7 @@ let print_xml = fun oc xml -> Mutex.lock m; try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m - with e -> let e = CErrors.push e in Mutex.unlock m; iraise e + with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e let slave_feeder fmt xml_oc msg = let xml = Xmlprotocol.(of_feedback fmt msg) in diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml index a2c80ea118..2e78642f2e 100644 --- a/ide/protocol/xmlprotocol.ml +++ b/ide/protocol/xmlprotocol.ml @@ -679,7 +679,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) with any -> - let any = CErrors.push any in + let any = Exninfo.capture any in Fail (handler.handle_exn any) (** brain dead code, edit if protocol messages are added/removed *) diff --git a/interp/impargs.ml b/interp/impargs.ml index 78c4b21920..1365b97d82 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -77,9 +77,9 @@ let with_implicit_protection f x = implicit_args := oflags; rslt with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = implicit_args := oflags in - iraise reraise + Exninfo.iraise reraise type on_trailing_implicit = Error | Info | Silent diff --git a/interp/notation.ml b/interp/notation.ml index 2086e08f79..b869cb2a36 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1959,6 +1959,6 @@ let with_notation_protection f x = let fs = freeze ~marshallable:false in try let a = f x in unfreeze fs; a with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = unfreeze fs in - iraise reraise + Exninfo.iraise reraise diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c6035f78ff..1be86f2bf8 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -962,7 +962,7 @@ let check_one_fix renv recpos trees def = let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the match away by looking for a constructor in c_0 (we unfold definitions too) *) let c_0 = whd_all renv.env c_0 in @@ -1007,7 +1007,7 @@ let check_one_fix renv recpos trees def = check_nested_fix_body illformed renv' (decrArg+1) arg_sp body else check_rec_call renv' [] body) with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the fix away by looking for a constructor in l[decrArg] (we unfold definitions too) *) if List.length l <= decrArg then Exninfo.iraise exn; @@ -1055,7 +1055,7 @@ let check_one_fix renv recpos trees def = List.iter (check_rec_call renv []) l; check_rec_call renv [] c with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the proj away by looking for a constructor in c (we unfold definitions too) *) let c = whd_all renv.env c in diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 86eaaddc90..3f2e63b984 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -180,8 +180,8 @@ let call_linker ?(fatal=true) env ~prefix f upds = if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix with Dynlink.Error _ as exn -> - let exn = CErrors.push exn in - if fatal then iraise exn + let exn = Exninfo.capture exn in + if fatal then Exninfo.iraise exn else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8db8a044a8..d8e1b6537e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1262,7 +1262,7 @@ let export ?except ~output_native_objects senv dir = let senv = try join_safe_environment ?except senv with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in CErrors.user_err ~hdr:"export" (CErrors.iprint e) in assert(senv.future_cst = []); diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 1660a00244..ec81694177 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -14,7 +14,7 @@ (** {6 Error handling} *) val push : exn -> Exninfo.iexn -(** Alias for [Backtrace.add_backtrace]. *) +[@@ocaml.deprecated "please use [Exninfo.capture]"] (** {6 Generic errors.} diff --git a/lib/future.ml b/lib/future.ml index ddf841b7fc..e8d232ad96 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -131,7 +131,7 @@ let rec compute ck : 'a value = let data = f () in c := Val data; `Val data with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let e = fix_exn e in match e with | (NotReady _, _) -> `Exn e diff --git a/lib/system.ml b/lib/system.ml index 2d68fd2fdf..9089eda564 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -248,9 +248,9 @@ let extern_state magic filename val_0 = marshal_out channel val_0; close_out channel with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = try_remove filename in - iraise reraise + Exninfo.iraise reraise with Sys_error s -> CErrors.user_err ~hdr:"System.extern_state" (str "System error: " ++ str s) diff --git a/lib/util.mli b/lib/util.mli index 2f1a03a19c..1417d6dfcb 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -119,8 +119,10 @@ val delayed_force : 'a delayed -> 'a (** {6 Enriched exceptions} *) type iexn = Exninfo.iexn +[@@ocaml.deprecated "please use [Exninfo.iexn]"] -val iraise : iexn -> 'a +val iraise : Exninfo.iexn -> 'a +[@@ocaml.deprecated "please use [Exninfo.iraise]"] (** {6 Misc. } *) diff --git a/library/states.ml b/library/states.ml index 90303a2a5c..c656dfb952 100644 --- a/library/states.ml +++ b/library/states.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util - type state = Lib.frozen * Summary.frozen let lib_of_state = fst @@ -31,5 +29,5 @@ let with_state_protection f x = try let a = f x in unfreeze st; a with reraise -> - let reraise = CErrors.push reraise in - (unfreeze st; iraise reraise) + let reraise = Exninfo.capture reraise in + (unfreeze st; Exninfo.iraise reraise) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index d1a6e0eda2..55558eaed0 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -685,9 +685,9 @@ let with_grammar_rule_protection f x = let fs = freeze ~marshallable:false in try let a = f x in unfreeze fs; a with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = unfreeze fs in - iraise reraise + Exninfo.iraise reraise (** Registering grammar of generic arguments *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b2ee0f9370..45fafd2872 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -520,7 +520,7 @@ let funind_purify f x = let st = Vernacstate.freeze_interp_state ~marshallable:false in try f x with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in Vernacstate.unfreeze_interp_state st; Exninfo.iraise e diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 513f5ca77b..d0c94e7903 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -670,7 +670,7 @@ let hResolve id c occ t = Pretyping.understand env sigma t_hole with | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) in diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 8344f9dae3..82c64a9857 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -114,7 +114,7 @@ END (** Eauto *) -TACTIC EXTEND prolog +TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () } | [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> { Eauto.prolog_tac (eval_uconstrs ist l) n } END @@ -253,4 +253,3 @@ VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF (match dbnames with None -> ["core"] | Some l -> l) entry; } END - diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6e620b71db..1d7fe335d1 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -165,8 +165,8 @@ let catching_error call_trace fail (e, info) = let catch_error call_trace f x = try f x with e when CErrors.noncritical e -> - let e = CErrors.push e in - catching_error call_trace iraise e + let e = Exninfo.capture e in + catching_error call_trace Exninfo.iraise e let wrap_error tac k = if is_traced () then Proofview.tclORELSE tac k else tac @@ -717,13 +717,13 @@ let interp_may_eval f ist env sigma = function try f ist env sigma c with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"interpretation of term " ++ pr_glob_constr_env env (fst c))); - iraise reraise + Exninfo.iraise reraise (* Interprets a constr expression possibly to first evaluate *) let interp_constr_may_eval ist env sigma c = @@ -731,12 +731,12 @@ let interp_constr_may_eval ist env sigma c = try interp_may_eval interp_constr ist env sigma c with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term")); - iraise reraise + Exninfo.iraise reraise in begin (* spiwack: to avoid unnecessary modifications of tacinterp, as this diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index f95672a15d..6ff79ebb9b 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1095,11 +1095,11 @@ let tclDO n tac = try tac gl with | CErrors.UserError (l, s) as e -> - let _, info = CErrors.push e in - let e' = CErrors.UserError (l, prefix i ++ s) in - Util.iraise (e', info) + let _, info = Exninfo.capture e in + let e' = CErrors.UserError (l, prefix i ++ s) in + Exninfo.iraise (e', info) | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) -> - raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in + raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 55c1f41c2c..afe776dced 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -73,11 +73,11 @@ let error_wrong_numarg_inductive ?loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f.") else Exninfo.iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> - let e = CErrors.push e in + let e = Exninfo.capture e in aux (e::errors) t in aux [] l diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ac1a4e88ef..1269488af3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -87,9 +87,9 @@ let search_guard ?loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with reraise -> - let (e, info) = CErrors.push reraise in + let (e, info) = Exninfo.capture reraise in let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in - iraise (e, info)); + Exninfo.iraise (e, info)); indexes else (* we now search recursively among all combinations *) @@ -266,8 +266,8 @@ let apply_heuristics env sigma fail_evar = let flags = default_flags_of (Typeclasses.classes_transparent_state ()) in try solve_unif_constraints_with_heuristics ~flags env sigma with e when CErrors.noncritical e -> - let e = CErrors.push e in - if fail_evar then iraise e else sigma + let e = Exninfo.capture e in + if fail_evar then Exninfo.iraise e else sigma let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen = (* Naive way, call resolution again with failure flag *) @@ -753,9 +753,9 @@ struct let cofix = (i, fixdecls) in (try check_cofix !!env (i, nf_fix sigma fixdecls) with reraise -> - let (e, info) = CErrors.push reraise in + let (e, info) = Exninfo.capture reraise in let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info)); + Exninfo.iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon @@ -946,9 +946,9 @@ struct try judge_of_product !!env name j j' with TypeError _ as e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info) in + Exninfo.iraise (e, info) in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_letin self (name, c1, t, c2) = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 98eb33273f..b07ae8788a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1465,7 +1465,7 @@ let report_anomaly (e, info) = UserError (None, msg) else e in - iraise (e, info) + Exninfo.iraise (e, info) let f_conv ?l2r ?reds env ?evars x y = let inj = EConstr.Unsafe.to_constr in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5b87603d54..1df377b20e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1149,10 +1149,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); - iraise e - + Exninfo.iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 832a749ef2..fd73ab1b5a 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -209,8 +209,8 @@ let catch_failerror (e, info) = | FailError (0,_) -> Control.check_for_interrupt () | FailError (lvl,s) -> - iraise (FailError (lvl - 1, s), info) - | e -> iraise (e, info) + Exninfo.iraise (FailError (lvl - 1, s), info) + | e -> Exninfo.iraise (e, info) (** FIXME: do we need to add a [Errors.push] here? *) (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) @@ -219,7 +219,7 @@ let tclORELSE0 t1 t2 g = t1 g with (* Breakpoint *) | e when CErrors.noncritical e -> - let e = CErrors.push e in catch_failerror e; t2 g + let e = Exninfo.capture e in catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -232,7 +232,7 @@ let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) with e when CErrors.noncritical e -> - let e = CErrors.push e in catch_failerror e; None + let e = Exninfo.capture e in catch_failerror e; None with | None -> t2else gls | Some sgl -> diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index fd689602df..9eb0924bd6 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -372,7 +372,7 @@ module Make(T : Task) () = struct let with_n_workers n priority f = let q = create n priority in try let rc = f q in destroy q; rc - with e -> let e = CErrors.push e in destroy q; iraise e + with e -> let e = Exninfo.capture e in destroy q; Exninfo.iraise e let n_workers { active } = Pool.n_workers active diff --git a/stm/stm.ml b/stm/stm.ml index 95c58b9043..a5b868343d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1014,7 +1014,7 @@ end = struct (* {{{ *) if PG_compat.there_are_pending_proofs () then VCS.goals id (PG_compat.get_open_goals ()) with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let good_id = !cur_id in invalidate_cur_state (); VCS.reached id; @@ -1046,7 +1046,7 @@ end = struct (* {{{ *) unfreeze st; res with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in Vernacstate.invalidate_cache (); unfreeze st; Exninfo.iraise e @@ -1540,7 +1540,7 @@ end = struct (* {{{ *) RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) let e_error_at, e_safe_id = match Stateid.get info with @@ -1687,7 +1687,7 @@ end = struct (* {{{ *) `OK proof end with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (try match Stateid.get info with | None -> msg_warning Pp.( @@ -2092,7 +2092,7 @@ end = struct (* {{{ *) ignore(stm_vernac_interp r_for st { r_what with verbose = true }); feedback ~id:r_for Processed with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let msg = iprint e in feedback ~id:r_for (Message (Error, None, msg)) @@ -2337,7 +2337,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = else try f () with e when CErrors.noncritical e -> - let ie = CErrors.push e in + let ie = Exninfo.capture e in error_absorbing_tactic id blockname ie in (* Absorb errors from f x *) let resilient_command f x = @@ -2435,7 +2435,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Stateid.add info ~valid:prev id in Exninfo.iraise (e, info)); wall_clock_last_fork := Unix.gettimeofday () @@ -2569,28 +2569,32 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initialization routine *) -type stm_init_options = { - (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should disappear at some - some point. *) - doc_type : stm_doc_type; +(** STM initialization options: *) +type stm_init_options = + { doc_type : stm_doc_type + (** The STM does set some internal flags differently depending on + the specified [doc_type]. This distinction should disappear at + some some point. *) - (* Initial load path in scope for the document. Usually extracted - from -R options / _CoqProject *) - iload_path : Loadpath.coq_path list; + ; ml_load_path : CUnix.physical_path list + (** OCaml load paths for the document. *) - (* Require [require_libs] before the initial state is + ; vo_load_path : Loadpath.vo_path list + (** [vo] load paths for the document. Usually extracted from -R + options / _CoqProject *) + + ; require_libs : (string * string option * bool option) list + (** Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, [lib,prefix,import_export] means require library [lib] from optional [prefix] and [import_export] if [Some false/Some true] is used. *) - require_libs : (string * string option * bool option) list; - (* STM options that apply to the current document. *) - stm_options : AsyncOpts.stm_opt; -} -(* fb_handler : Feedback.feedback -> unit; *) + ; stm_options : AsyncOpts.stm_opt + (** Low-level STM options *) + } + + (* fb_handler : Feedback.feedback -> unit; *) (* let doc_type_module_name (std : stm_doc_type) = @@ -2615,7 +2619,7 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; iload_path; require_libs; stm_options } = +let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } = let require_file (dir, from, exp) = let mp = Libnames.qualid_of_string dir in @@ -2633,7 +2637,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module name by looking at the load path! *) - List.iter Loadpath.add_coq_path iload_path; + List.iter Mltop.add_ml_dir ml_load_path; + List.iter Loadpath.add_vo_path vo_load_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; @@ -2688,7 +2693,7 @@ let observe ~doc id = VCS.print (); doc with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in VCS.print (); VCS.restore vcs; Exninfo.iraise e @@ -2763,7 +2768,7 @@ let finish_tasks name u p (t,rcbackup as tasks) = let a, _ = List.fold_left finish_task u (info_tasks tasks) in (a,true), p with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 @@ -2987,7 +2992,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.print (); rc with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in handle_failure e vcs let get_ast ~doc id = @@ -3197,7 +3202,7 @@ let edit_at ~doc id = VCS.print (); doc, rc with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in match Stateid.get info with | None -> VCS.print (); diff --git a/stm/stm.mli b/stm/stm.mli index 841adcf05b..e56bac6e0f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,38 +52,30 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -(** Coq initialization options: - - - [doc_type]: Type of document being created. - - - [require_libs]: list of libraries/modules to be pre-loaded at - startup. A tuple [(modname,modfrom,import)] is equivalent to [From - modfrom Require modname]; [import] works similarly to - [Library.require_library_from_dirpath], [Some false] will import - the module, [Some true] will additionally export it. - -*) -type stm_init_options = { - (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should disappear at some - some point. *) - doc_type : stm_doc_type; - - (* Initial load path in scope for the document. Usually extracted - from -R options / _CoqProject *) - iload_path : Loadpath.coq_path list; - - (* Require [require_libs] before the initial state is +(** STM initialization options: *) +type stm_init_options = + { doc_type : stm_doc_type + (** The STM does set some internal flags differently depending on + the specified [doc_type]. This distinction should disappear at + some some point. *) + + ; ml_load_path : CUnix.physical_path list + (** OCaml load paths for the document. *) + + ; vo_load_path : Loadpath.vo_path list + (** [vo] load paths for the document. Usually extracted from -R + options / _CoqProject *) + + ; require_libs : (string * string option * bool option) list + (** Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, [lib,prefix,import_export] means require library [lib] from optional [prefix] and [import_export] if [Some false/Some true] is used. *) - require_libs : (string * string option * bool option) list; - (* STM options that apply to the current document. *) - stm_options : AsyncOpts.stm_opt; -} -(* fb_handler : Feedback.feedback -> unit; *) + ; stm_options : AsyncOpts.stm_opt + (** Low-level STM options *) + } (** The type of a STM document *) type doc diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 1e18028e7b..86e6a92a22 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -97,8 +97,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = which is an error irrelevant to the proof system (in fact it means that [e] comes from [tac] failing to yield enough success). Hence it reraises [e]. *) - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) in let body, effs = Future.force const.Declare.proof_entry_body in (* We drop the side-effects from the entry, they already exist in the ambient environment *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 28feeecb86..e49f5abb8c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -236,7 +236,7 @@ let unify_resolve_refine poly flags gl clenv = Tacticals.New.tclZEROMSG (str "Unable to unify") | e when CErrors.noncritical e -> Tacticals.New.tclZEROMSG (str "Unexpected error") - | _ -> iraise ie) + | _ -> Exninfo.iraise ie) (** Dealing with goals of the form A -> B and hints of the form C -> A -> B. @@ -770,7 +770,7 @@ module Search = struct (fun e' -> if CErrors.noncritical (fst e') then (pr_error e'; aux (merge_exceptions e e') tl) - else iraise e') + else Exninfo.iraise e') and aux e = function | x :: xs -> onetac e x xs | [] -> diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 9a1e6a6736..aca6b4734a 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -235,7 +235,7 @@ module SearchProblem = struct (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls, cost, pptac) :: aux tacl with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in Refiner.catch_failerror e; aux tacl in aux l diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index dbabc4e4e0..7cdfd0637a 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -130,8 +130,8 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~ | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") with reraise -> - let reraise = CErrors.push reraise in - iraise reraise + let reraise = Exninfo.capture reraise in + Exninfo.iraise reraise let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in @@ -160,8 +160,8 @@ let refine_by_tactic ~name ~poly env sigma ty tac = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (* Catch the inner error of the monad tactic *) - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) in (* Plug back the retrieved sigma *) let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4b93b81d1c..5fde6d2178 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -144,7 +144,7 @@ module New : sig (** [catch_failerror e] fails and decreases the level if [e] is an Ltac error with level more than 0. Otherwise succeeds. *) - val catch_failerror : Util.iexn -> unit tactic + val catch_failerror : Exninfo.iexn -> unit tactic val tclIDTAC : unit tactic val tclTHEN : unit tactic -> unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8371da76b2..83423b7556 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1848,12 +1848,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> - let e' = CErrors.push e in + let e' = Exninfo.capture e in try aux (clenv_push_prod clause) with NotExtensibleClause -> match e with | UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause - | _ -> iraise e' + | _ -> Exninfo.iraise e' in aux (make_clenv_binding env sigma (d,thm) lbind) @@ -1886,7 +1886,7 @@ let apply_in_once ?(respect_opaque = false) with_delta tac id ]) with e when with_destruct && CErrors.noncritical e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (descend_in_conjunctions (Id.Set.singleton targetid) (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) @@ -3155,7 +3155,7 @@ let clear_for_destruct ids = (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids) (function | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT () - | e -> iraise e) + | e -> Exninfo.iraise e) (* Either unfold and clear if defined or simply clear if not a definition *) let expand_hyp id = diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake index aa68fad39e..38c610a5a6 100644 --- a/test-suite/ide/debug_ltac.fake +++ b/test-suite/ide/debug_ltac.fake @@ -1,2 +1,3 @@ +ADD { Comments "fakeide doesn't support fail as the first sentence". } FAILADD { Debug On. } ADD { Set Debug On. } diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake index 5284c5d3a5..eb553f9dfa 100644 --- a/test-suite/ide/undo002.fake +++ b/test-suite/ide/undo002.fake @@ -3,6 +3,7 @@ # # Simple backtrack by 2 before two global definitions # +ADD initial { Comments "initial sentence". } ADD { Definition foo := 0. } ADD { Definition bar := 1. } EDIT_AT initial diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index dceb811d66..f75a706041 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -104,7 +104,7 @@ let compile opts copts ~echo ~f_in ~f_out = |> prlist_with_sep pr_comma Names.Id.print) ++ str ".") in - let iload_path = build_load_path opts in + let ml_load_path, vo_load_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.config.stm_flags in let output_native_objects = match opts.config.native_compiler with @@ -129,8 +129,8 @@ let compile opts copts ~echo ~f_in ~f_out = | BuildVo | BuildVok -> let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VoDoc long_f_dot_out; - iload_path; require_libs; stm_options; + Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path; + vo_load_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in @@ -181,8 +181,8 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VioDoc long_f_dot_out; - iload_path; require_libs; stm_options; + Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path; + vo_load_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in @@ -252,8 +252,9 @@ let do_vio opts copts = (* We must initialize the loadpath here as the vio scheduling process happens outside of the STM *) if copts.vio_files <> [] || copts.vio_tasks <> [] then - let iload_path = build_load_path opts in - List.iter Loadpath.add_coq_path iload_path; + let ml_lp, vo_lp = build_load_path opts in + List.iter Mltop.add_ml_dir ml_lp; + List.iter Loadpath.add_vo_path vo_lp; (* Vio compile pass *) if copts.vio_files <> [] then schedule_vio copts; diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 949a13974c..24cfecd057 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -70,8 +70,8 @@ type coqargs_pre = { load_init : bool; load_rcfile : bool; - ml_includes : Loadpath.coq_path list; - vo_includes : Loadpath.coq_path list; + ml_includes : string list; + vo_includes : Loadpath.vo_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) @@ -164,14 +164,13 @@ let default = { (* Functional arguments *) (******************************************************************************) let add_ml_include opts s = - Loadpath.{ opts with pre = { opts.pre with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.pre.ml_includes }} + { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }} let add_vo_include opts unix_path coq_path implicit = let open Loadpath in let coq_path = Libnames.dirpath_of_string coq_path in { opts with pre = { opts.pre with vo_includes = { - recursive = true; - path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.pre.vo_includes }} + unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }} let add_vo_require opts d p export = { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }} @@ -582,9 +581,7 @@ let prelude_data = "Prelude", Some "Coq", Some false let require_libs opts = if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires -let cmdline_load_path opts = - opts.pre.ml_includes @ opts.pre.vo_includes - let build_load_path opts = - (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @ - cmdline_load_path opts + let ml_path, vo_path = if opts.pre.boot then [],[] else Coqinit.libs_init_load_path () in + ml_path @ opts.pre.ml_includes , + vo_path @ opts.pre.vo_includes diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index aba6811f43..88de48967a 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -46,8 +46,8 @@ type coqargs_pre = { load_init : bool; load_rcfile : bool; - ml_includes : Loadpath.coq_path list; - vo_includes : Loadpath.coq_path list; + ml_includes : CUnix.physical_path list; + vo_includes : Loadpath.vo_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) @@ -83,4 +83,4 @@ val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * strin val error_wrong_arg : string -> unit val require_libs : t -> (string * string option * bool option) list -val build_load_path : t -> Loadpath.coq_path list +val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 7f3d4b570f..f6b173968f 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -47,38 +47,26 @@ let load_rcfile ~rcfile ~state = " found. Skipping rcfile loading.")) *) with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = Feedback.msg_info (str"Load of rcfile failed.") in - iraise reraise + Exninfo.iraise reraise -(* Recursively puts `.v` files in the LoadPath if -nois was not passed *) +(* Recursively puts `.v` files in the LoadPath *) let build_stdlib_vo_path ~unix_path ~coq_path = let open Loadpath in - { recursive = true; - path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true } - } - -let build_stdlib_ml_path ~dir = - let open Loadpath in - { recursive = true - ; path_spec = MlPath dir - } + { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true } let build_userlib_path ~unix_path = let open Loadpath in - { recursive = true; - path_spec = VoPath { - unix_path; - coq_path = Libnames.default_root_prefix; - has_ml = AddRecML; - implicit = false; - } + { unix_path + ; coq_path = Libnames.default_root_prefix + ; has_ml = true + ; implicit = false + ; recursive = true } let ml_path_if c p = - let open Loadpath in - let f x = { recursive = false; path_spec = MlPath x } in - if c then List.map f p else [] + if c then p else [] (* LoadPath for developers *) let toplevel_init_load_path () = @@ -97,16 +85,19 @@ let libs_init_load_path () = let coqpath = Envars.coqpath in let coq_path = Names.DirPath.make [Libnames.coq_root] in + (* ML includes *) + let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") in + List.map fst plugins_dirs, + (* current directory (not recursively!) *) - [ { recursive = false; - path_spec = VoPath { unix_path = "."; - coq_path = Libnames.default_root_prefix; - implicit = false; - has_ml = AddTopML } + [ { unix_path = "." + ; coq_path = Libnames.default_root_prefix + ; implicit = false + ; has_ml = true + ; recursive = false } ] @ (* then standard library *) - [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @ [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ (* then user-contrib *) @@ -120,10 +111,8 @@ let libs_init_load_path () = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = - let open Loadpath in - let lp s = { recursive = false; path_spec = MlPath s } in let add_subdir dl = - Loadpath.add_coq_path (lp (List.fold_left (/) (Envars.coqlib()) [dl])) + Mltop.add_ml_dir (List.fold_left (/) (Envars.coqlib()) [dl]) in - Loadpath.add_coq_path (lp (Envars.coqlib ())); - List.iter add_subdir Coq_config.all_src_dirs + Mltop.add_ml_dir (Envars.coqlib ()); + List.iter add_subdir Coq_config.all_src_dirs diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index f3a007d987..f099173808 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -17,7 +17,7 @@ val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) -val toplevel_init_load_path : unit -> Loadpath.coq_path list +val toplevel_init_load_path : unit -> CUnix.physical_path list (* LoadPath for Coq user libraries *) -val libs_init_load_path : unit -> Loadpath.coq_path list +val libs_init_load_path : unit -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e4508e9bfc..b0012f8978 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -265,7 +265,7 @@ let read_sentence ~state input = let open Vernac.State in try Stm.parse_sentence ~doc:state.doc state.sid ~entry:G_toplevel.vernac_toplevel input with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in discard_to_dot (); (* The caller of read_sentence does the error printing now, this should be re-enabled once we rely on the feedback error @@ -360,7 +360,7 @@ let top_goal_print ~doc c oldp newp = end with | exn -> - let (e, info) = CErrors.push exn in + let (e, info) = Exninfo.capture exn in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer @@ -484,7 +484,7 @@ let read_and_execute ~state = TopErr.print_error_for_buffer Feedback.Error msg top_buffer; exit 1 | any -> - let (e, info) = CErrors.push any in + let (e, info) = Exninfo.capture any in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1ea48ee766..1e6b1023fe 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -226,7 +226,7 @@ let init_execution opts custom_init = Spawned.init_channels (); if opts.post.memory_stat then at_exit print_memory_stat; let top_lp = Coqinit.toplevel_init_load_path () in - List.iter Loadpath.add_coq_path top_lp; + List.iter Mltop.add_ml_dir top_lp; CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority); Mltop.init_known_plugins (); (* Configuration *) @@ -281,14 +281,14 @@ let init_document opts = *) (* Next line allows loading .vos files when in interactive mode *) Flags.load_vos_libraries := true; - let iload_path = build_load_path opts in + let ml_load_path, vo_load_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.config.stm_flags in let open Vernac.State in let doc, sid = Stm.(new_doc { doc_type = Interactive opts.config.logic.toplevel_name; - iload_path; require_libs; stm_options; + ml_load_path; vo_load_path; require_libs; stm_options; }) in { doc; sid; proof = None; time = opts.config.time } diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index adcce67b0d..8e6cd8f4c7 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -69,7 +69,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> - let (reraise, info) = CErrors.push reraise in + let (reraise, info) = Exninfo.capture reraise in (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid); @@ -77,7 +77,8 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = match Loc.get_loc info with | None -> Option.cata (Loc.add_loc info) info loc | Some _ -> info - end in iraise (reraise, info) + end in + Exninfo.iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) let load_vernac_core ~echo ~check ~interactive ~state file = @@ -113,9 +114,9 @@ let load_vernac_core ~echo ~check ~interactive ~state file = in try loop state [] with any -> (* whatever the exception *) - let (e, info) = CErrors.push any in + let (e, info) = Exninfo.capture any in input_cleanup (); - iraise (e, info) + Exninfo.iraise (e, info) let process_expr ~state loc_ast = interp_vernac ~interactive:true ~check:true ~state loc_ast diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 196b28b274..f66ed7b4cf 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -573,7 +573,7 @@ let () = define1 "constr_check" constr begin fun c -> Proofview.Unsafe.tclEVARS sigma >>= fun () -> return (of_result Value.of_constr (Inl c)) with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in return (of_result Value.of_constr (Inr e)) end end @@ -1079,7 +1079,7 @@ let interp_constr flags ist c = Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT c with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in set_bt info >>= fun info -> match Exninfo.get info fatal_flag with | None -> Proofview.tclZERO ~info e diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index e57c324c9a..2b6f987fa6 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -37,9 +37,9 @@ module Hook = struct let call ?hook ?fix_exn x = try Option.iter (fun hook -> CEphemeron.get hook x) hook with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let e = Option.cata (fun fix -> fix e) e fix_exn in - Util.iraise e + Exninfo.iraise e end (* Locality stuff *) diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index c816a4eb4f..e645fc552b 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -935,9 +935,9 @@ let protect_summaries f = try f fs with reraise -> (* Something wrong: undo the whole process *) - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = Summary.unfreeze_summaries fs in - iraise reraise + Exninfo.iraise reraise let start_module export id args res = protect_summaries (RawModOps.start_module export id args res) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 8486de3aed..37b584f8d9 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -912,10 +912,11 @@ GRAMMAR EXTEND Gram | IDENT "Locate"; l = locatable -> { VernacLocate l } (* Managing load paths *) - | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> - { VernacAddLoadPath (false, dir, alias) } - | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; - alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) } + | IDENT "Add"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath -> + { VernacAddLoadPath { implicit = false; logical_path; physical_path } } + | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath -> + { VernacAddLoadPath { implicit = true; logical_path; physical_path } } + | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> { VernacRemoveLoadPath dir } @@ -934,9 +935,7 @@ GRAMMAR EXTEND Gram | IDENT "Inspect"; n = natural -> { VernacPrint (PrintInspect n) } | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> - { VernacAddMLPath (false, dir) } - | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> - { VernacAddMLPath (true, dir) } + { VernacAddMLPath dir } (* For acting on parameter tables *) | "Set"; table = option_table; v = option_setting -> @@ -1070,9 +1069,6 @@ GRAMMAR EXTEND Gram option_table: [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]] ; - as_dirpath: - [ [ d = OPT [ "as"; d = dirpath -> { d } ] -> { d } ] ] - ; ne_in_or_out_modules: [ [ IDENT "inside"; l = LIST1 global -> { SearchInside l } | IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ] diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 227d2f1554..80616ecc2a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -118,7 +118,7 @@ let alarm what internal msg = let try_declare_scheme what f internal names kn = try f internal names kn with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in let msg = match extract_exn (fst e) with | ParameterWithoutEquality cst -> @@ -166,11 +166,11 @@ let try_declare_scheme what f internal names kn = | e when CErrors.noncritical e -> alarm what internal (str "Unexpected error during scheme creation: " ++ CErrors.print e) - | _ -> iraise e + | _ -> Exninfo.iraise e in match msg with | None -> () - | Some msg -> iraise (UserError (None, msg), snd e) + | Some msg -> Exninfo.iraise (UserError (None, msg), snd e) let beq_scheme_msg mind = let mib = Global.lookup_mind mind in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index f7606f4ede..68f4f55d0e 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -375,8 +375,8 @@ let finish_proved env sigma idopt po info = (* This takes care of the implicits and hook for the current constant*) process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms with e when CErrors.noncritical e -> - let e = CErrors.push e in - iraise (fix_exn e) + let e = Exninfo.capture e in + Exninfo.iraise (fix_exn e) in () | _ -> CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") diff --git a/vernac/library.ml b/vernac/library.ml index 0f7e7d2aa0..5aff86c50c 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -440,11 +440,11 @@ let save_library_base f sum lib univs tasks proofs = System.marshal_out_segment f ch (proofs : seg_proofs); close_out ch with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in close_out ch; Feedback.msg_warning (str "Removed file " ++ str f); Sys.remove f; - iraise reraise + Exninfo.iraise reraise type ('document,'counters) todo_proofs = | ProofsTodoNone (* for .vo *) diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index 506b3bc505..38aa42c349 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -218,24 +218,18 @@ let try_locate_absolute_library dir = (** { 5 Extending the load path } *) -(* Adds a path to the Coq and ML paths *) -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; (* Filesystem path containing vo/ml files *) - coq_path : DP.t; (* Coq prefix for the path *) - implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) - has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} +type vo_path = + { unix_path : string + (** Filesystem path containing vo/ml files *) + ; coq_path : DP.t + (** Coq prefix for the path *) + ; implicit : bool + (** [implicit = true] avoids having to qualify with [coq_path] *) + ; has_ml : bool + (** If [has_ml] is true, the directory will also be added to the ml include path *) + ; recursive : bool + (** [recursive] will determine whether we explore sub-directories *) + } let warn_cannot_open_path = CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" @@ -255,9 +249,10 @@ let convert_string d = warn_cannot_use_directory d; raise Exit -let add_vo_path ~recursive lp = +let add_vo_path lp = let unix_path = lp.unix_path in let implicit = lp.implicit in + let recursive = lp.recursive in if System.exists_dir unix_path then let dirs = if recursive then System.all_subdirs ~unix_path else [] in let prefix = DP.repr lp.coq_path in @@ -268,22 +263,17 @@ let add_vo_path ~recursive lp = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - let add_ml_dir = Mltop.add_ml_dir ~recursive:false in - let () = match lp.has_ml with - | AddNoML -> () - | AddTopML -> - Mltop.add_ml_dir ~recursive:false unix_path - | AddRecML -> - List.iter (fun (lp,_) -> add_ml_dir lp) dirs; - add_ml_dir unix_path in + let () = + if lp.has_ml && not lp.recursive then + Mltop.add_ml_dir unix_path + else if lp.has_ml && lp.recursive then + (List.iter (fun (lp,_) -> Mltop.add_ml_dir lp) dirs; + Mltop.add_ml_dir unix_path) + else + () + in let add (path, dir) = add_load_path path ~implicit dir in let () = List.iter add dirs in add_load_path unix_path ~implicit lp.coq_path else warn_cannot_open_path unix_path - -let add_coq_path { recursive; path_spec } = match path_spec with - | VoPath lp -> - add_vo_path ~recursive lp - | MlPath dir -> - Mltop.add_ml_dir ~recursive dir diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli index 47d2d34125..68212b9a47 100644 --- a/vernac/loadpath.mli +++ b/vernac/loadpath.mli @@ -64,26 +64,17 @@ val try_locate_absolute_library : DirPath.t -> string (** {6 Extending the Load Path } *) (** Adds a path to the Coq and ML paths *) -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; +type vo_path = + { unix_path : string (** Filesystem path containing vo/ml files *) - coq_path : Names.DirPath.t; + ; coq_path : DirPath.t (** Coq prefix for the path *) - implicit : bool; + ; implicit : bool (** [implicit = true] avoids having to qualify with [coq_path] *) - has_ml : add_ml; - (** If [has_ml] is true, the directory will also be search for plugins *) -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} + ; has_ml : bool + (** If [has_ml] is true, the directory will also be added to the ml include path *) + ; recursive : bool + (** [recursive] will determine whether we explore sub-directories *) + } -val add_coq_path : coq_path -> unit +val add_vo_path : vo_path -> unit diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 3937f887ad..fedebc9700 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1466,9 +1466,9 @@ let with_lib_stk_protection f x = let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = Lib.unfreeze fs in - iraise reraise + Exninfo.iraise reraise let with_syntax_protection f x = with_lib_stk_protection diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 5046248e11..671dae7876 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -128,11 +128,6 @@ let add_ml_dir s = | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () -(* For Rec Add ML Path (-R) *) -let add_ml_dir ~recursive unix_path = - let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in - List.iter (fun (lp,_) -> add_ml_dir lp) dirs - (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = if Filename.check_suffix name ".cmo" then diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 271772d7ba..633a5c241d 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -32,7 +32,7 @@ val ocaml_toploop : unit -> unit (** {5 ML Dynlink} *) (** Adds a dir to the plugin search path *) -val add_ml_dir : recursive:bool -> string -> unit +val add_ml_dir : string -> unit (** Tests if we can load ML files *) val has_dynlink : bool diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 76dbf1ad5a..27eb821a6a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -428,7 +428,7 @@ let solve_by_tac ?loc name evi t poly ctx = Some (body, entry.Declare.proof_entry_type, ctx') with | Refiner.FailError (_, s) as exn -> - let _ = CErrors.push exn in + let _ = Exninfo.capture exn in user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) (* If the proof is open we absorb the error and leave the obligation open *) | Proof.OpenProof _ -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 314c423f65..33d9e3d98a 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1016,22 +1016,18 @@ let string_of_definition_object_kind = let open Decls in function return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) (* Auxiliary file and library management *) - | VernacAddLoadPath (fl,s,d) -> + | VernacAddLoadPath { implicit; physical_path; logical_path } -> return ( hov 2 (keyword "Add" ++ - (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ - keyword "LoadPath" ++ spc() ++ qs s ++ - (match d with - | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) - ) + (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++ + keyword "LoadPath" ++ spc() ++ qs physical_path ++ + spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path)) | VernacRemoveLoadPath s -> return (keyword "Remove LoadPath" ++ qs s) - | VernacAddMLPath (fl,s) -> + | VernacAddMLPath (s) -> return ( keyword "Add" - ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ keyword "ML Path" ++ qs s ) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index de02f7ecfb..509c164af8 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -361,7 +361,7 @@ let in_phase ~phase f x = with exn -> let iexn = Exninfo.capture exn in default_phase := op; - Util.iraise iexn + Exninfo.iraise iexn let pr_loc loc = let fname = loc.Loc.fname in @@ -394,7 +394,7 @@ let pr_phase ?loc () = None let print_err_exn any = - let (e, info) = CErrors.push any in + let (e, info) = Exninfo.capture any in let loc = Loc.get_loc info in let pre_hdr = pr_phase ?loc () in let msg = CErrors.iprint (e, info) ++ fnl () in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2eb1aa39b0..953faf6fdb 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -342,9 +342,9 @@ let dump_universes_gen prl g s = close (); str "Universes written to file \"" ++ str s ++ str "\"." with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in close (); - iraise reraise + Exninfo.iraise reraise let universe_subgraph ?loc g univ = let open Univ in @@ -1120,20 +1120,17 @@ let vernac_set_used_variables ~pstate e : Proof_global.t = let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename -let vernac_add_loadpath implicit pdir ldiropt = +let vernac_add_loadpath ~implicit pdir coq_path = let open Loadpath in let pdir = expand pdir in - let alias = Option.default Libnames.default_root_prefix ldiropt in - add_coq_path { recursive = true; - path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } } + add_vo_path { unix_path = pdir; coq_path; has_ml = true; implicit; recursive = true } let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) (* Coq syntax for ML or system commands *) -let vernac_add_ml_path isrec path = - let open Loadpath in - add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } +let vernac_add_ml_path path = + Mltop.add_ml_dir (expand path) let vernac_declare_ml_module ~local l = let local = Option.default false local in @@ -2106,18 +2103,18 @@ let translate_vernac ~atts v = let open Vernacextend in match v with unsupported_attributes atts; vernac_solve_existential ~pstate n c) (* Auxiliary file and library management *) - | VernacAddLoadPath (isrec,s,alias) -> + | VernacAddLoadPath { implicit; physical_path; logical_path } -> VtDefault(fun () -> unsupported_attributes atts; - vernac_add_loadpath isrec s alias) + vernac_add_loadpath ~implicit physical_path logical_path) | VernacRemoveLoadPath s -> VtDefault(fun () -> unsupported_attributes atts; vernac_remove_loadpath s) - | VernacAddMLPath (isrec,s) -> + | VernacAddMLPath (s) -> VtDefault(fun () -> unsupported_attributes atts; - vernac_add_ml_path isrec s) + vernac_add_ml_path s) | VernacDeclareMLModule l -> VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l) | VernacChdir s -> diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 45018a246c..22aaab2a68 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -98,7 +98,6 @@ type search_restriction = | SearchInside of qualid list | SearchOutside of qualid list -type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option @@ -363,9 +362,13 @@ type nonrec vernac_expr = | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) - | VernacAddLoadPath of rec_flag * string * DirPath.t option + | VernacAddLoadPath of { implicit : bool + ; physical_path : CUnix.physical_path + ; logical_path : DirPath.t + } + | VernacRemoveLoadPath of string - | VernacAddMLPath of rec_flag * string + | VernacAddMLPath of string | VernacDeclareMLModule of string list | VernacChdir of string option diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index f41df06f85..e0afb7f483 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -109,11 +109,11 @@ let type_vernac opn converted_args ~atts = phase := "Executing command"; hunk ~atts with - | reraise -> - let reraise = CErrors.push reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - iraise reraise + | reraise -> + let reraise = Exninfo.capture reraise in + if !Flags.debug then + Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); + Exninfo.iraise reraise (** VERNAC EXTEND registering *) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1ec09b6beb..8083098022 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -96,7 +96,7 @@ let with_fail f : (Pp.t, unit) result = (* Fail Timeout is a common pattern so we need to support it. *) | e when CErrors.noncritical e || e = CErrors.Timeout -> (* The error has to be printed in the failing state *) - Ok CErrors.(iprint (push e)) + Ok CErrors.(iprint (Exninfo.capture e)) (* We restore the state always *) let with_fail ~st f = @@ -262,10 +262,10 @@ let interp_gen ~verbosely ~st ~interp_fn cmd = Vernacstate.freeze_interp_state ~marshallable:false ) st with exn -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in Vernacstate.invalidate_cache (); - Util.iraise exn + Exninfo.iraise exn (* Regular interp *) let interp ?(verbosely=true) ~st cmd = diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 3c70961e06..59557a60a6 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -21,7 +21,7 @@ module Parser = struct Flags.with_option Flags.we_are_parsing (fun () -> try Pcoq.Entry.parse entry pa with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in Exninfo.iraise (e, info)) () |