From 5122eb4da3691d32483acd3e481c89d9e5c5c5b9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 19 Jun 2018 17:50:31 +0200 Subject: [coqtop] Give priority to stdlib load path over current directory When initilazing the load path, coqtop adds implicit bindings for stdlib and for the current directory (-R stdlib Coq -R . ""). In case of a clash, the binding of the current directory had priority, which makes it impossible to edit stdlib files (when they Require files from the same directory) using PG, or from CoqIDE when launched from the directory containing the file. Example to reproduce the problem: ``` cd plugins/omega coqide Omega.v ``` some of the Requires will fail. --- toplevel/coqinit.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e61f830f3..e1d35e537 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -92,6 +92,14 @@ let libs_init_load_path ~load_init = let coqpath = Envars.coqpath in let coq_path = Names.DirPath.make [Libnames.coq_root] in + (* current directory (not recursively!) *) + [ { recursive = false; + path_spec = VoPath { unix_path = "."; + coq_path = Libnames.default_root_prefix; + implicit = false; + has_ml = AddTopML } + } ] @ + (* then standard library and plugins *) [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false; build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_path ~with_ml:true ] @ @@ -102,15 +110,7 @@ let libs_init_load_path ~load_init = ) @ (* 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) @ - - (* then current directory (not recursively!) *) - [ { recursive = false; - path_spec = VoPath { unix_path = "."; - coq_path = Libnames.default_root_prefix; - implicit = false; - has_ml = AddTopML } - } ] + 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 *) -- cgit v1.2.3