diff options
| -rw-r--r-- | toplevel/coqargs.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 22 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 9 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 11 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 21 |
5 files changed, 28 insertions, 41 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 24cfecd057..ef97e57a5c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -582,6 +582,10 @@ let require_libs opts = if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires let build_load_path opts = - let ml_path, vo_path = if opts.pre.boot then [],[] else Coqinit.libs_init_load_path () in + 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/coqinit.ml b/toplevel/coqinit.ml index f6b173968f..4041d02953 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -65,21 +65,10 @@ let build_userlib_path ~unix_path = ; recursive = true } -let ml_path_if c p = - if c then 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 @@ -107,12 +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 add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) (Envars.coqlib()) [dl]) - in - 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 f099173808..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 -> CUnix.physical_path list - (* LoadPath for Coq user libraries *) -val libs_init_load_path : unit -> CUnix.physical_path list * Loadpath.vo_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 b0012f8978..7ff58039d4 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -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 1e6b1023fe..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 Mltop.add_ml_dir 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 |