aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/ccompile.ml15
-rw-r--r--toplevel/coqargs.ml21
-rw-r--r--toplevel/coqargs.mli6
-rw-r--r--toplevel/coqinit.ml69
-rw-r--r--toplevel/coqinit.mli9
-rw-r--r--toplevel/coqloop.ml17
-rw-r--r--toplevel/coqtop.ml25
-rw-r--r--toplevel/vernac.ml9
8 files changed, 73 insertions, 98 deletions
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..ef97e57a5c 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,11 @@ 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
+ let coqlib = Envars.coqlib () in
+ Coqinit.libs_init_load_path ~coqlib 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..4041d02953 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -47,66 +47,46 @@ 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 []
-
-(* LoadPath for developers *)
-let toplevel_init_load_path () =
- let coqlib = Envars.coqlib () in
- (* NOTE: These directories are searched from last to first *)
- (* first, developer specific directory to open *)
- ml_path_if Coq_config.local [coqlib/"dev"]
-
(* LoadPath for Coq user libraries *)
-let libs_init_load_path () =
+let libs_init_load_path ~coqlib =
let open Loadpath in
- let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
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 *)
@@ -116,14 +96,3 @@ let libs_init_load_path () =
(* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath)
-
-(* 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]))
- in
- Loadpath.add_coq_path (lp (Envars.coqlib ()));
- List.iter add_subdir Coq_config.all_src_dirs
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index f3a007d987..eb6b37000e 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -14,10 +14,7 @@ val set_debug : unit -> unit
val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t
-val init_ocaml_path : unit -> unit
-
-(* LoadPath for toploop toplevels *)
-val toplevel_init_load_path : unit -> Loadpath.coq_path list
-
(* LoadPath for Coq user libraries *)
-val libs_init_load_path : unit -> Loadpath.coq_path list
+val libs_init_load_path
+ : coqlib:CUnix.physical_path
+ -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e4508e9bfc..7ff58039d4 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;
@@ -501,10 +501,16 @@ let rec vernac_loop ~state =
let state, drop = read_and_execute ~state in
if drop then state else vernac_loop ~state
-(* Default toplevel loop *)
+(* Default toplevel loop, machinery for drop is below *)
let drop_args = ref None
+(* Initialises the Ocaml toplevel before launching it, so that it can
+ find the "include" file in the *source* directory *)
+let init_ocaml_path ~coqlib =
+ let add_subdir dl = Mltop.add_ml_dir (Filename.concat coqlib dl) in
+ List.iter add_subdir ("dev" :: Coq_config.all_src_dirs)
+
let loop ~opts ~state =
drop_args := Some opts;
let open Coqargs in
@@ -517,7 +523,8 @@ let loop ~opts ~state =
(* Call the main loop *)
let _ : Vernac.State.t = vernac_loop ~state in
(* Initialise and launch the Ocaml toplevel *)
- Coqinit.init_ocaml_path();
+ let coqlib = Envars.coqlib () in
+ init_ocaml_path ~coqlib;
Mltop.ocaml_toploop();
(* We delete the feeder after the OCaml toploop has ended so users
of Drop can see the feedback. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1ea48ee766..876388092d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -155,19 +155,22 @@ let print_style_tags opts =
let () = List.iter iter tags in
flush_all ()
-let init_setup = function
- | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
- | Some s -> Envars.set_user_coqlib s
+let init_coqlib opts = match opts.config.coqlib with
+ | None when opts.pre.boot -> ()
+ | None ->
+ Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+ | Some s ->
+ Envars.set_user_coqlib s
let print_query opts = function
| PrintVersion -> Usage.version ()
| PrintMachineReadableVersion -> Usage.machine_readable_version ()
| PrintWhere ->
- let () = init_setup opts.config.coqlib in
+ let () = init_coqlib opts in
print_endline (Envars.coqlib ())
| PrintHelp h -> Usage.print_usage stderr h
| PrintConfig ->
- let () = init_setup opts.config.coqlib in
+ let () = init_coqlib opts in
Envars.print_config stdout Coq_config.all_src_dirs
| PrintTags -> print_style_tags opts.config
@@ -217,16 +220,12 @@ let init_parse parse_extra help init_opts =
end;
opts, customopts
+(** Coq's init process, phase 2: Basic Coq environment, plugins. *)
let init_execution opts custom_init =
- (* Coq's init process, phase 2:
- Basic Coq environment, load-path, plugins.
- *)
(* 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 ();
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;
CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
Mltop.init_known_plugins ();
(* Configuration *)
@@ -268,7 +267,7 @@ let init_toplevel custom =
match opts.main with
| Queries q -> List.iter (print_query opts) q; exit 0
| Run ->
- let () = init_setup opts.config.coqlib in
+ let () = init_coqlib opts in
let customstate = init_execution opts (custom.init customopts) in
opts, customopts, customstate
@@ -281,14 +280,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 00:50:37 +0000