From 25020ba614315ce143f657511696fb7bf5135b00 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Nov 2016 19:29:29 +0100 Subject: Dead code (xdg_config_dirs). --- lib/envars.ml | 10 ---------- lib/envars.mli | 1 - 2 files changed, 11 deletions(-) diff --git a/lib/envars.ml b/lib/envars.ml index 79516bb1b..0974368f6 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -191,16 +191,6 @@ let xdg_data_dirs warn = in xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir -let xdg_config_dirs warn = - let sys_dirs = - try - List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS")) - with - | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "config"] - | Not_found -> ["/etc/xdg/coq"] - in - xdg_config_home warn :: sys_dirs @ opt2list Coq_config.configdir - let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) diff --git a/lib/envars.mli b/lib/envars.mli index b164e789d..c33a08c40 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -66,7 +66,6 @@ val camlp4 : unit -> string *) val xdg_config_home : (string -> unit) -> string val xdg_data_home : (string -> unit) -> string -val xdg_config_dirs : (string -> unit) -> string list val xdg_data_dirs : (string -> unit) -> string list val xdg_dirs : warn : (string -> unit) -> string list -- cgit v1.2.3 From 96ec7b5e65f79118914b7c81e14587d0dc065cc1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Nov 2016 20:27:27 +0100 Subject: Mini-renaming in configure.ml to avoid switching back and forth from "libdir" to "COQLIBINSTALL" then "libdir", then "coqlib". For the record, here is how installation options are named at the current time in the different places they are used (if any): Name in Name in Name in Name of option Name in Name of option config/Makefile coqtop -config config/coq_config.ml in configure lib/envars.ml for coqtop/coqdep -------------------------------------------------------------------------------------------------------- COQLIBINSTALL COQLIB coqlib -libdir coqlib -coqlib DOCDIR DOCDIR docdir -docdir docdir CONFIGDIR configdir -configdir DATADIR datadir -datadir BINDIR -bindir MANDIR -mandir EMACSLIB -emacslib COQDOCDIR -coqdocdir Note: in envars.ml, docdir and coqlib are recomputed --- configure.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/configure.ml b/configure.ml index 7af18cb85..4aca89561 100644 --- a/configure.ml +++ b/configure.ml @@ -905,7 +905,7 @@ let install_dirs = let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs -let libdir = let (_,_,d,_) = select "COQLIBINSTALL" in d +let coqlib = let (_,_,d,_) = select "COQLIBINSTALL" in d let docdir = let (_,_,d,_) = select "DOCDIR" in d @@ -940,7 +940,7 @@ let config_runtime () = | _ -> let ld="CAML_LD_LIBRARY_PATH" in build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld; - ["-dllib";"-lcoqrun";"-dllpath";libdir/"kernel/byterun"] + ["-dllib";"-lcoqrun";"-dllpath";coqlib/"kernel/byterun"] let vmbyteflags = config_runtime () @@ -1026,7 +1026,7 @@ let write_configml f = pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); pr_b "local" !Prefs.local; pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n"; - pr_o "coqlib" (if !Prefs.local then None else Some libdir); + pr_o "coqlib" (if !Prefs.local then None else Some coqlib); pr_o "configdir" configdir; pr_o "datadir" datadir; pr_s "docdir" docdir; -- cgit v1.2.3 From 615047314c4e3331db09883b30c067544a03023b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Nov 2016 21:05:02 +0100 Subject: Unified terminology in configure.ml/coq_config.ml: arch_win32 -> arch_is_win32. --- configure.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/configure.ml b/configure.ml index 4aca89561..f95144912 100644 --- a/configure.ml +++ b/configure.ml @@ -425,11 +425,11 @@ let arch = match !Prefs.arch with else if arch <> "" then arch else try_archs arch_progs -(** NB: [arch_win32] is broader than [os_type_win32], cf. cygwin *) +(** NB: [arch_is_win32] is broader than [os_type_win32], cf. cygwin *) -let arch_win32 = (arch = "win32") +let arch_is_win32 = (arch = "win32") -let exe = exe := if arch_win32 then ".exe" else ""; !exe +let exe = exe := if arch_is_win32 then ".exe" else ""; !exe let dll = if os_type_win32 then ".dll" else ".so" (** * VCS @@ -449,7 +449,7 @@ let vcs = let browser = match !Prefs.browser with | Some b -> b - | None when arch_win32 -> "start %s" + | None when arch_is_win32 -> "start %s" | None when arch = "Darwin" -> "open %s" | _ -> "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &" @@ -854,7 +854,7 @@ let withdoc = check_doc () let coqtop = Sys.getcwd () -let unix = os_type_cygwin || not arch_win32 +let unix = os_type_cygwin || not arch_is_win32 (** Variable name, description, ref in Prefs, default dir, prefix-relative *) @@ -864,10 +864,10 @@ let install = [ "/bin"; "COQLIBINSTALL", "the Coq library", Prefs.libdir, (if unix then "/usr/local/lib/coq" else "C:/coq/lib"), - (if arch_win32 then "" else "/lib/coq"); + (if arch_is_win32 then "" else "/lib/coq"); "CONFIGDIR", "the Coqide configuration files", Prefs.configdir, (if unix then "/etc/xdg/coq" else "C:/coq/config"), - (if arch_win32 then "/config" else "/etc/xdg/coq"); + (if arch_is_win32 then "/config" else "/etc/xdg/coq"); "DATADIR", "the Coqide data files", Prefs.datadir, (if unix then "/usr/local/share/coq" else "C:/coq/share"), "/share/coq"; @@ -879,10 +879,10 @@ let install = [ "/share/doc/coq"; "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib, (if unix then "/usr/local/share/emacs/site-lisp" else "C:/coq/emacs"), - (if arch_win32 then "/emacs" else "/share/emacs/site-lisp"); + (if arch_is_win32 then "/emacs" else "/share/emacs/site-lisp"); "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir, (if unix then "/usr/local/share/texmf/tex/latex/misc" else "C:/coq/latex"), - (if arch_win32 then "/latex" else "/share/emacs/site-lisp"); + (if arch_is_win32 then "/latex" else "/share/emacs/site-lisp"); ] let do_one_instdir (var,msg,r,dflt,suff) = @@ -920,7 +920,7 @@ let datadir = (** Do we use -custom (yes by default on Windows and MacOS) *) -let custom_os = arch_win32 || arch = "Darwin" +let custom_os = arch_is_win32 || arch = "Darwin" let use_custom = match !Prefs.custom with | Some b -> b @@ -1048,7 +1048,7 @@ let write_configml f = pr_s "date" short_date; pr_s "compile_date" full_date; pr_s "arch" arch; - pr_b "arch_is_win32" arch_win32; + pr_b "arch_is_win32" arch_is_win32; pr_s "exec_extension" exe; pr_s "coqideincl" !lablgtkincludes; pr_s "has_coqide" coqide; -- cgit v1.2.3 From 5b506165097047aa8b6b431db9f2cbc8dbf6c3de Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Nov 2016 23:35:47 +0100 Subject: Unifying the layout of installation directories. There seems to have been several bugs, when -prefix is given: - Under win32: "" instead of "lib" (presumably introduced in ab442aed8, 2006) - Under win32: datadir, mandir, docdir should presumably be in "share", "man", "doc", as given in default - Under non-win32: coqdoc files should be in latex subdir not emacs subdir --- configure.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/configure.ml b/configure.ml index f95144912..a0b0a7087 100644 --- a/configure.ml +++ b/configure.ml @@ -864,25 +864,25 @@ let install = [ "/bin"; "COQLIBINSTALL", "the Coq library", Prefs.libdir, (if unix then "/usr/local/lib/coq" else "C:/coq/lib"), - (if arch_is_win32 then "" else "/lib/coq"); + (if arch_is_win32 then "/lib" else "/lib/coq"); "CONFIGDIR", "the Coqide configuration files", Prefs.configdir, (if unix then "/etc/xdg/coq" else "C:/coq/config"), (if arch_is_win32 then "/config" else "/etc/xdg/coq"); "DATADIR", "the Coqide data files", Prefs.datadir, (if unix then "/usr/local/share/coq" else "C:/coq/share"), - "/share/coq"; + (if arch_is_win32 then "/share" else "/share/coq"); "MANDIR", "the Coq man pages", Prefs.mandir, (if unix then "/usr/local/share/man" else "C:/coq/man"), - "/share/man"; + (if arch_is_win32 then "/man" else "/share/man"); "DOCDIR", "the Coq documentation", Prefs.docdir, (if unix then "/usr/local/share/doc/coq" else "C:/coq/doc"), - "/share/doc/coq"; + (if arch_is_win32 then "/doc" else "/share/doc/coq"); "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib, (if unix then "/usr/local/share/emacs/site-lisp" else "C:/coq/emacs"), (if arch_is_win32 then "/emacs" else "/share/emacs/site-lisp"); "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir, (if unix then "/usr/local/share/texmf/tex/latex/misc" else "C:/coq/latex"), - (if arch_is_win32 then "/latex" else "/share/emacs/site-lisp"); + (if arch_is_win32 then "/latex" else "/share/texmf/tex/latex/misc"); ] let do_one_instdir (var,msg,r,dflt,suff) = -- cgit v1.2.3 From 168bb8fd5fe62beebd5e4998e903777b33654a4a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 12 May 2017 21:18:45 +0200 Subject: More structure and more code factorization in building default installation paths in unix or win32. There are two layouts (self-contained or unix-like) and we build absolute paths from them. Under unix, there is a fully relative layout (when user gives a prefix) and a standard semi-relative layout (where most file are under /usr/local with the absolute /etc/xdg/coq as an exception). I respected the existing semantics that under cygwin, the unix layout is the default one when prefix is not given, but the self-contained layout is the default one when a prefix is given. --- configure.ml | 44 +++++++++++++++++++++++++------------------- 1 file changed, 25 insertions(+), 19 deletions(-) diff --git a/configure.ml b/configure.ml index a0b0a7087..9902946e3 100644 --- a/configure.ml +++ b/configure.ml @@ -858,37 +858,43 @@ let unix = os_type_cygwin || not arch_is_win32 (** Variable name, description, ref in Prefs, default dir, prefix-relative *) +type path_style = + | Absolute of string (* Should start with a "/" *) + | Relative of string (* Should not start with a "/" *) + let install = [ "BINDIR", "the Coq binaries", Prefs.bindir, - (if unix then "/usr/local/bin" else "C:/coq/bin"), - "/bin"; + Relative "bin", Relative "bin"; "COQLIBINSTALL", "the Coq library", Prefs.libdir, - (if unix then "/usr/local/lib/coq" else "C:/coq/lib"), - (if arch_is_win32 then "/lib" else "/lib/coq"); + Relative "lib", Relative "lib/coq"; "CONFIGDIR", "the Coqide configuration files", Prefs.configdir, - (if unix then "/etc/xdg/coq" else "C:/coq/config"), - (if arch_is_win32 then "/config" else "/etc/xdg/coq"); + Relative "config", Absolute "/etc/xdg/coq"; "DATADIR", "the Coqide data files", Prefs.datadir, - (if unix then "/usr/local/share/coq" else "C:/coq/share"), - (if arch_is_win32 then "/share" else "/share/coq"); + Relative "share", Relative "share/coq"; "MANDIR", "the Coq man pages", Prefs.mandir, - (if unix then "/usr/local/share/man" else "C:/coq/man"), - (if arch_is_win32 then "/man" else "/share/man"); + Relative "man", Relative "share/man"; "DOCDIR", "the Coq documentation", Prefs.docdir, - (if unix then "/usr/local/share/doc/coq" else "C:/coq/doc"), - (if arch_is_win32 then "/doc" else "/share/doc/coq"); + Relative "doc", Relative "share/doc/coq"; "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib, - (if unix then "/usr/local/share/emacs/site-lisp" else "C:/coq/emacs"), - (if arch_is_win32 then "/emacs" else "/share/emacs/site-lisp"); + Relative "emacs", Relative "share/emacs/site-lisp"; "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir, - (if unix then "/usr/local/share/texmf/tex/latex/misc" else "C:/coq/latex"), - (if arch_is_win32 then "/latex" else "/share/texmf/tex/latex/misc"); + Relative "latex", Relative "share/texmf/tex/latex/misc"; ] -let do_one_instdir (var,msg,r,dflt,suff) = - let dir = match !r, !Prefs.prefix with +let use_suffix prefix = function + | Relative suff -> prefix ^ "/" ^ suff + | Absolute path -> path + +let relativize = function + (* Turn a global layout based on some prefix to a relative layout *) + | Relative _ as suffix -> suffix + | Absolute path -> Relative (String.sub path 1 (String.length path - 1)) + +let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout) = + let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in + let dir = match !uservalue, !Prefs.prefix with | Some d, _ -> d - | _, Some p -> p^suff + | _, Some p -> use_suffix p (if arch_is_win32 then selfcontainedlayout else relativize unixlayout) | _ -> let () = printf "Where should I install %s [%s]? " msg dflt in let line = read_line () in -- cgit v1.2.3 From 417ac448411ce924444915da8e7e6fb81a12bc57 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 11 Nov 2016 11:11:20 +0100 Subject: Configuration: always giving a value to configdir and datadir. They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories. --- config/coq_config.mli | 4 ++-- configure.ml | 30 ++++++++++++++---------------- ide/minilib.ml | 4 ++-- lib/envars.ml | 4 +--- 4 files changed, 19 insertions(+), 23 deletions(-) diff --git a/config/coq_config.mli b/config/coq_config.mli index c171bd355..59c96f73d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -9,8 +9,8 @@ val local : bool (* local use (no installation) *) val coqlib : string option (* where the std library is installed *) -val configdir : string option (* where configuration files are installed *) -val datadir : string option (* where extra data files are installed *) +val configdir : string (* where configuration files are installed *) +val datadir : string (* where extra data files are installed *) val docdir : string (* where the doc is installed *) val ocaml : string (* names of ocaml binaries *) diff --git a/configure.ml b/configure.ml index 9902946e3..128751ea3 100644 --- a/configure.ml +++ b/configure.ml @@ -891,35 +891,33 @@ let relativize = function | Absolute path -> Relative (String.sub path 1 (String.length path - 1)) let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout) = - let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in let dir = match !uservalue, !Prefs.prefix with | Some d, _ -> d | _, Some p -> use_suffix p (if arch_is_win32 then selfcontainedlayout else relativize unixlayout) | _ -> + let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in let () = printf "Where should I install %s [%s]? " msg dflt in let line = read_line () in if line = "" then dflt else line - in (var,msg,dir,dir<>dflt) + in (var,msg,dir) let do_one_noinst (var,msg,_,_,_) = - if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true) - else (var,msg,coqtop^"/doc",false) + if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide") + else (var,msg,coqtop^"/doc") let install_dirs = let f = if !Prefs.local then do_one_noinst else do_one_instdir in List.map f install -let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs +let select var = List.find (fun (v,_,_) -> v=var) install_dirs -let coqlib = let (_,_,d,_) = select "COQLIBINSTALL" in d +let coqlib = let (_,_,d) = select "COQLIBINSTALL" in d -let docdir = let (_,_,d,_) = select "DOCDIR" in d +let docdir = let (_,_,d) = select "DOCDIR" in d -let configdir = - let (_,_,d,b) = select "CONFIGDIR" in if b then Some d else None +let configdir = let (_,_,d) = select "CONFIGDIR" in d -let datadir = - let (_,_,d,b) = select "DATADIR" in if b then Some d else None +let datadir = let (_,_,d) = select "DATADIR" in d (** * OCaml runtime flags *) @@ -986,7 +984,7 @@ let print_summary () = else (pr " Paths for true installation:\n"; List.iter - (fun (_,msg,dir,_) -> pr " - %s will be copied in %s\n" msg dir) + (fun (_,msg,dir) -> pr " - %s will be copied in %s\n" msg dir) install_dirs); pr "\n"; pr "If anything is wrong above, please restart './configure'.\n\n"; @@ -1033,8 +1031,8 @@ let write_configml f = pr_b "local" !Prefs.local; pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n"; pr_o "coqlib" (if !Prefs.local then None else Some coqlib); - pr_o "configdir" configdir; - pr_o "datadir" datadir; + pr_s "configdir" configdir; + pr_s "datadir" datadir; pr_s "docdir" docdir; pr_s "ocaml" camlexec.top; pr_s "ocamlfind" camlexec.find; @@ -1119,8 +1117,8 @@ let write_makefile f = pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags); pr "%s\n\n" !build_loadpath; pr "# Paths for true installation\n"; - List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs; - List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs; + List.iter (fun (v,msg,_) -> pr "# %s: path for %s\n" v msg) install_dirs; + List.iter (fun (v,_,dir) -> pr "%s=%S\n" v dir) install_dirs; pr "\n# Coq version\n"; pr "VERSION=%s\n" coq_version; pr "VERSION4MACOS=%s\n\n" coq_macos_version; diff --git a/ide/minilib.ml b/ide/minilib.ml index 2c24e46f8..c9cef5639 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -54,12 +54,12 @@ let coqide_config_home () = let coqide_data_dirs () = coqify (Glib.get_user_data_dir ()) :: List.map coqify (Glib.get_system_data_dirs ()) - @ Option.List.cons Coq_config.datadir [] + @ [Coq_config.datadir] let coqide_config_dirs () = coqide_config_home () :: List.map coqify (Glib.get_system_config_dirs ()) - @ Option.List.cons Coq_config.configdir [] + @ [Coq_config.configdir] let is_prefix_of pre s = let i = ref 0 in diff --git a/lib/envars.ml b/lib/envars.ml index 0974368f6..989a18db9 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -23,8 +23,6 @@ let ( / ) a b = let coqify d = d / "coq" -let opt2list = function None -> [] | Some x -> [x] - let home ~warn = getenv_else "HOME" (fun () -> try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> @@ -189,7 +187,7 @@ let xdg_data_dirs warn = | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"] | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"] in - xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir + xdg_data_home warn :: sys_dirs @ [Coq_config.datadir] let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) -- cgit v1.2.3 From 34a2f9eb315da8b794f2573bdfc8ff941d81bdbe Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 11 Nov 2016 11:14:10 +0100 Subject: Configure: viewing compilation in -local itself as an installation layout. Consequence: docdir is always defined, no more "" in external preferences for manual and stdlib when using coqide in -local mode. --- configure.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/configure.ml b/configure.ml index 128751ea3..1d2003501 100644 --- a/configure.ml +++ b/configure.ml @@ -864,24 +864,25 @@ type path_style = let install = [ "BINDIR", "the Coq binaries", Prefs.bindir, - Relative "bin", Relative "bin"; + Relative "bin", Relative "bin", Relative "bin"; "COQLIBINSTALL", "the Coq library", Prefs.libdir, - Relative "lib", Relative "lib/coq"; + Relative "lib", Relative "lib/coq", Relative ""; "CONFIGDIR", "the Coqide configuration files", Prefs.configdir, - Relative "config", Absolute "/etc/xdg/coq"; + Relative "config", Absolute "/etc/xdg/coq", Relative "ide"; "DATADIR", "the Coqide data files", Prefs.datadir, - Relative "share", Relative "share/coq"; + Relative "share", Relative "share/coq", Relative "ide"; "MANDIR", "the Coq man pages", Prefs.mandir, - Relative "man", Relative "share/man"; + Relative "man", Relative "share/man", Relative "man"; "DOCDIR", "the Coq documentation", Prefs.docdir, - Relative "doc", Relative "share/doc/coq"; + Relative "doc", Relative "share/doc/coq", Relative "doc"; "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib, - Relative "emacs", Relative "share/emacs/site-lisp"; + Relative "emacs", Relative "share/emacs/site-lisp", Relative "tools"; "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir, - Relative "latex", Relative "share/texmf/tex/latex/misc"; + Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc"; ] let use_suffix prefix = function + | Relative "" -> prefix | Relative suff -> prefix ^ "/" ^ suff | Absolute path -> path @@ -890,7 +891,7 @@ let relativize = function | Relative _ as suffix -> suffix | Absolute path -> Relative (String.sub path 1 (String.length path - 1)) -let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout) = +let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,_) = let dir = match !uservalue, !Prefs.prefix with | Some d, _ -> d | _, Some p -> use_suffix p (if arch_is_win32 then selfcontainedlayout else relativize unixlayout) @@ -901,9 +902,8 @@ let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout) = if line = "" then dflt else line in (var,msg,dir) -let do_one_noinst (var,msg,_,_,_) = - if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide") - else (var,msg,coqtop^"/doc") +let do_one_noinst (var,msg,_,_,_,locallayout) = + (var,msg,use_suffix coqtop locallayout) let install_dirs = let f = if !Prefs.local then do_one_noinst else do_one_instdir in -- cgit v1.2.3 From d53ba17d1761261593c598b6a88cfd6ce0eb3514 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 03:08:56 +0100 Subject: Using Coq_config.local rather than None to tell that Coq_config.coqlib is local. This goes towards an approach where a local layout can be seen as an installed layout. --- config/coq_config.mli | 2 +- configure.ml | 5 +---- lib/envars.ml | 7 ++----- tools/coq_makefile.ml | 8 +------- tools/coqdoc/cdglobals.ml | 26 +++++++++++++------------- 5 files changed, 18 insertions(+), 30 deletions(-) diff --git a/config/coq_config.mli b/config/coq_config.mli index 59c96f73d..28a40ca93 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -8,7 +8,7 @@ val local : bool (* local use (no installation) *) -val coqlib : string option (* where the std library is installed *) +val coqlib : string (* where the std library is installed *) val configdir : string (* where configuration files are installed *) val datadir : string (* where extra data files are installed *) val docdir : string (* where the doc is installed *) diff --git a/configure.ml b/configure.ml index 1d2003501..1a851ef45 100644 --- a/configure.ml +++ b/configure.ml @@ -1022,15 +1022,12 @@ let write_configml f = let pr_s = pr "let %s = %S\n" in let pr_b = pr "let %s = %B\n" in let pr_i = pr "let %s = %d\n" in - let pr_o s o = pr "let %s = %s\n" s - (match o with None -> "None" | Some d -> sprintf "Some %S" d) - in pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n"; pr "(* Exact command that generated this file: *)\n"; pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); pr_b "local" !Prefs.local; pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n"; - pr_o "coqlib" (if !Prefs.local then None else Some coqlib); + pr_s "coqlib" coqlib; pr_s "configdir" configdir; pr_s "datadir" datadir; pr_s "docdir" docdir; diff --git a/lib/envars.ml b/lib/envars.ml index 989a18db9..b71a3f629 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -110,11 +110,8 @@ let guess_coqlib fail = let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in check_file_else ~dir ~file:prelude (fun () -> - let coqlib = match Coq_config.coqlib with - | Some coqlib -> coqlib - | None -> coqroot - in - if Sys.file_exists (coqlib / prelude) then coqlib + if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude) + then Coq_config.coqlib else fail "cannot guess a path for Coq libraries; please use -coqlib option") diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 78c92e68b..8e2f75fc9 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -119,14 +119,8 @@ let read_whole_file s = Buffer.contents b let makefile_template = - let open Filename in let template = "/tools/CoqMakefile.in" in - if Coq_config.local then - let coqbin = CUnix.canonical_path_name (dirname Sys.executable_name) in - dirname coqbin ^ template - else match Coq_config.coqlib with - | None -> assert false - | Some dir -> dir ^ template + Coq_config.coqlib ^ template let quote s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 5d48473d8..4b5c5d2e5 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -74,19 +74,19 @@ let normalize_filename f = let guess_coqlib () = let file = "theories/Init/Prelude.vo" in - match Coq_config.coqlib with - | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib - | Some _ | None -> - let coqbin = normalize_path (Filename.dirname Sys.executable_name) in - let prefix = Filename.dirname coqbin in - let rpath = - if Coq_config.local then [] - else if Coq_config.arch_is_win32 then ["lib"] - else ["lib/coq"] - in - let coqlib = List.fold_left (/) prefix rpath in - if Sys.file_exists (coqlib / file) then coqlib - else prefix + if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file) + then Coq_config.coqlib + else + let coqbin = normalize_path (Filename.dirname Sys.executable_name) in + let prefix = Filename.dirname coqbin in + let rpath = + if Coq_config.local then [] + else if Coq_config.arch_is_win32 then ["lib"] + else ["lib/coq"] + in + let coqlib = List.fold_left (/) prefix rpath in + if Sys.file_exists (coqlib / file) then coqlib + else prefix let header_trailer = ref true let header_file = ref "" -- cgit v1.2.3 From 58935ddbaf6f0e2470716d30f70ea18a9f8151c4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 03:08:34 +0100 Subject: Exporting the suffixes needed to build coqlib, docdir, etc. This allows to centralize in the configuration file the description of the 3 possible installation layouts (dispatched over directories shared by multiple application as in unix, self-contained style like in windows, local non-installation as with option -local). Also supporting relocalisation when -prefix or -libdir and co is given. --- config/coq_config.mli | 8 +++++++ configure.ml | 58 +++++++++++++++++++++++++++++++++-------------- lib/envars.ml | 8 +++---- tools/coqdoc/cdglobals.ml | 7 +----- 4 files changed, 53 insertions(+), 28 deletions(-) diff --git a/config/coq_config.mli b/config/coq_config.mli index 28a40ca93..2b3bc2c25 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -8,11 +8,19 @@ val local : bool (* local use (no installation) *) +(* The fields below are absolute paths *) val coqlib : string (* where the std library is installed *) val configdir : string (* where configuration files are installed *) val datadir : string (* where extra data files are installed *) val docdir : string (* where the doc is installed *) +(* The fields below are paths relative to the installation prefix *) +(* However, if an absolute path, it means discarding the actual prefix *) +val coqlibsuffix : string (* std library relative to installation prefix *) +val configdirsuffix : string (* config files relative to installation prefix *) +val datadirsuffix : string (* data files relative to installation prefix *) +val docdirsuffix : string (* doc directory relative to installation prefix *) + val ocaml : string (* names of ocaml binaries *) val ocamlfind : string val ocamllex : string diff --git a/configure.ml b/configure.ml index 1a851ef45..64165fab0 100644 --- a/configure.ml +++ b/configure.ml @@ -881,6 +881,9 @@ let install = [ Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc"; ] +let strip_trailing_slash_if_any p = + if p.[String.length p - 1] = '/' then String.sub p 0 (String.length p - 1) else p + let use_suffix prefix = function | Relative "" -> prefix | Relative suff -> prefix ^ "/" ^ suff @@ -891,34 +894,48 @@ let relativize = function | Relative _ as suffix -> suffix | Absolute path -> Relative (String.sub path 1 (String.length path - 1)) +let find_suffix prefix path = match prefix with + | None -> Absolute path + | Some p -> + let p = strip_trailing_slash_if_any p in + let lpath = String.length path in + let lp = String.length p in + if lpath > lp && String.sub path 0 lp = p then + Relative (String.sub path (lp+1) (lpath - lp - 1)) + else + Absolute path + let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,_) = - let dir = match !uservalue, !Prefs.prefix with - | Some d, _ -> d - | _, Some p -> use_suffix p (if arch_is_win32 then selfcontainedlayout else relativize unixlayout) - | _ -> - let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in + let dir,suffix = match !uservalue, !Prefs.prefix with + | Some d, p -> d,find_suffix p d + | _, Some p -> + let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in + use_suffix p suffix, suffix + | _, p -> + let suffix = if unix then unixlayout else selfcontainedlayout in + let base = if unix then "/usr/local" else "C:/coq" in + let dflt = use_suffix base suffix in let () = printf "Where should I install %s [%s]? " msg dflt in let line = read_line () in - if line = "" then dflt else line - in (var,msg,dir) + if line = "" then (dflt,suffix) else (line,find_suffix p line) + in (var,msg,dir,suffix) let do_one_noinst (var,msg,_,_,_,locallayout) = - (var,msg,use_suffix coqtop locallayout) + (var,msg,use_suffix coqtop locallayout,locallayout) let install_dirs = let f = if !Prefs.local then do_one_noinst else do_one_instdir in List.map f install -let select var = List.find (fun (v,_,_) -> v=var) install_dirs +let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs -let coqlib = let (_,_,d) = select "COQLIBINSTALL" in d +let coqlib,coqlibsuffix = let (_,_,d,s) = select "COQLIBINSTALL" in d,s -let docdir = let (_,_,d) = select "DOCDIR" in d +let docdir,docdirsuffix = let (_,_,d,s) = select "DOCDIR" in d,s -let configdir = let (_,_,d) = select "CONFIGDIR" in d - -let datadir = let (_,_,d) = select "DATADIR" in d +let configdir,configdirsuffix = let (_,_,d,s) = select "CONFIGDIR" in d,s +let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s (** * OCaml runtime flags *) @@ -984,7 +1001,7 @@ let print_summary () = else (pr " Paths for true installation:\n"; List.iter - (fun (_,msg,dir) -> pr " - %s will be copied in %s\n" msg dir) + (fun (_,msg,dir,_) -> pr " - %s will be copied in %s\n" msg dir) install_dirs); pr "\n"; pr "If anything is wrong above, please restart './configure'.\n\n"; @@ -1022,6 +1039,9 @@ let write_configml f = let pr_s = pr "let %s = %S\n" in let pr_b = pr "let %s = %B\n" in let pr_i = pr "let %s = %d\n" in + let pr_p s o = pr "let %s = %S\n" s + (match o with Relative s -> s | Absolute s -> s) + in pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n"; pr "(* Exact command that generated this file: *)\n"; pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); @@ -1031,6 +1051,10 @@ let write_configml f = pr_s "configdir" configdir; pr_s "datadir" datadir; pr_s "docdir" docdir; + pr_p "coqlibsuffix" coqlibsuffix; + pr_p "configdirsuffix" configdirsuffix; + pr_p "datadirsuffix" datadirsuffix; + pr_p "docdirsuffix" docdirsuffix; pr_s "ocaml" camlexec.top; pr_s "ocamlfind" camlexec.find; pr_s "ocamllex" camlexec.lex; @@ -1114,8 +1138,8 @@ let write_makefile f = pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags); pr "%s\n\n" !build_loadpath; pr "# Paths for true installation\n"; - List.iter (fun (v,msg,_) -> pr "# %s: path for %s\n" v msg) install_dirs; - List.iter (fun (v,_,dir) -> pr "%s=%S\n" v dir) install_dirs; + List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs; + List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs; pr "\n# Coq version\n"; pr "VERSION=%s\n" coq_version; pr "VERSION4MACOS=%s\n\n" coq_macos_version; diff --git a/lib/envars.ml b/lib/envars.ml index b71a3f629..feb5b3497 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -102,13 +102,12 @@ let _ = If the check fails, then [oth ()] is evaluated. Using file system equality seems well enough for this heuristic *) let check_file_else ~dir ~file oth = - let path = if Coq_config.local then coqroot else coqroot / dir in + let path = coqroot / dir in if Sys.file_exists (path / file) then path else oth () let guess_coqlib fail = let prelude = "theories/Init/Prelude.vo" in - let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in - check_file_else ~dir ~file:prelude + check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude (fun () -> if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude) then Coq_config.coqlib @@ -125,8 +124,7 @@ let set_coqlib ~fail = let coqlib () = !Flags.coqlib let docdir () = - let dir = if Coq_config.arch_is_win32 then "doc" else "share/doc/coq" in - check_file_else ~dir ~file:"html" (fun () -> Coq_config.docdir) + check_file_else ~dir:Coq_config.docdirsuffix ~file:"html" (fun () -> Coq_config.docdir) let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 4b5c5d2e5..a1987387f 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -79,12 +79,7 @@ let guess_coqlib () = else let coqbin = normalize_path (Filename.dirname Sys.executable_name) in let prefix = Filename.dirname coqbin in - let rpath = - if Coq_config.local then [] - else if Coq_config.arch_is_win32 then ["lib"] - else ["lib/coq"] - in - let coqlib = List.fold_left (/) prefix rpath in + let coqlib = prefix / Coq_config.coqlibsuffix in if Sys.file_exists (coqlib / file) then coqlib else prefix -- cgit v1.2.3 From 66b98ecd41bac232bbee19a9b3484feefd71df3c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 03:47:08 +0100 Subject: Generalizing to docdir and datadir the test for a relocated installation. Also standardizing the choice of the default datadir (I don't see why we should add by default both /usr/local/share/coq and /usr/share/coq when we know that the installation is in only one of them). Open question: test for possible relocation of the installed coq should be done on raw dirname of the executable or on the standardization of this name wrt symbolic links? --- lib/envars.ml | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/lib/envars.ml b/lib/envars.ml index feb5b3497..78f14273d 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -79,9 +79,6 @@ let expand_path_macros ~warn s = (** {2 Coq paths} *) -let relative_base = - Filename.dirname (Filename.dirname Sys.executable_name) - let coqbin = CUnix.canonical_path_name (Filename.dirname Sys.executable_name) @@ -96,13 +93,18 @@ let _ = if Coq_config.arch_is_win32 then Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> "")) +(** Add a local installation suffix (unless the suffix is itself + absolute in which case the prefix does not matter) *) +let use_suffix prefix suffix = + if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix + (** [check_file_else ~dir ~file oth] checks if [file] exists in - the installation directory [dir] given relatively to [coqroot]. - If this Coq is only locally built, then [file] must be in [coqroot]. + the installation directory [dir] given relatively to [coqroot], + which maybe has been relocated. If the check fails, then [oth ()] is evaluated. Using file system equality seems well enough for this heuristic *) let check_file_else ~dir ~file oth = - let path = coqroot / dir in + let path = use_suffix coqroot dir in if Sys.file_exists (path / file) then path else oth () let guess_coqlib fail = @@ -124,7 +126,14 @@ let set_coqlib ~fail = let coqlib () = !Flags.coqlib let docdir () = - check_file_else ~dir:Coq_config.docdirsuffix ~file:"html" (fun () -> Coq_config.docdir) + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.docdirsuffix in + if Sys.file_exists path then path else Coq_config.docdir + +let datadir () = + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.datadirsuffix in + if Sys.file_exists path then path else Coq_config.datadir let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in @@ -179,10 +188,9 @@ let xdg_data_dirs warn = try List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS")) with - | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"] - | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"] + | Not_found -> [datadir ()] in - xdg_data_home warn :: sys_dirs @ [Coq_config.datadir] + xdg_data_home warn :: sys_dirs let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) -- cgit v1.2.3 From 5c875b6ab907cb48b0d06aba48d4c733cfd2ff06 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 04:01:29 +0100 Subject: Relying on computation done in Envars to discover the installation directories. This allows to share the test for possible relocalisation done in envars.ml. --- ide/ideutils.ml | 2 +- ide/minilib.ml | 4 ++-- ide/preferences.ml | 4 ++-- lib/envars.ml | 5 +++++ lib/envars.mli | 12 +++++++++--- 5 files changed, 19 insertions(+), 8 deletions(-) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index a08ab07b5..8a0e507c0 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -422,7 +422,7 @@ let browse prerr url = let doc_url () = if doc_url#get = use_default_doc_url || doc_url#get = "" then - let addr = List.fold_left Filename.concat (Coq_config.docdir) + let addr = List.fold_left Filename.concat (Envars.docdir ()) ["html";"refman";"index.html"] in if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman diff --git a/ide/minilib.ml b/ide/minilib.ml index c9cef5639..2b278fac6 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -54,12 +54,12 @@ let coqide_config_home () = let coqide_data_dirs () = coqify (Glib.get_user_data_dir ()) :: List.map coqify (Glib.get_system_data_dirs ()) - @ [Coq_config.datadir] + @ [Envars.datadir ()] let coqide_config_dirs () = coqide_config_home () :: List.map coqify (Glib.get_system_config_dirs ()) - @ [Coq_config.configdir] + @ [Envars.configdir ()] let is_prefix_of pre s = let i = ref 0 in diff --git a/ide/preferences.ml b/ide/preferences.ml index 9fe9c6337..d97e49927 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -918,7 +918,7 @@ let configure ?(apply=(fun () -> ())) () = in let doc_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]); + "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]); Coq_config.wwwrefman; use_default_doc_url ] in @@ -931,7 +931,7 @@ let configure ?(apply=(fun () -> ())) () = doc_url#get in let library_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]); + "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]); Coq_config.wwwstdlib ] in combo diff --git a/lib/envars.ml b/lib/envars.ml index 78f14273d..bc8012297 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -135,6 +135,11 @@ let datadir () = let path = use_suffix coqroot Coq_config.datadirsuffix in if Sys.file_exists path then path else Coq_config.datadir +let configdir () = + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.configdirsuffix in + if Sys.file_exists path then path else Coq_config.configdir + let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in let make_search_path path = diff --git a/lib/envars.mli b/lib/envars.mli index c33a08c40..c8bbf17d9 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -27,12 +27,18 @@ val home : warn:(string -> unit) -> string (** [coqlib] is the path to the Coq library. *) val coqlib : unit -> string +(** [docdir] is the path to the installed documentation. *) +val docdir : unit -> string + +(** [datadir] is the path to the installed data directory. *) +val datadir : unit -> string + +(** [configdir] is the path to the installed config directory. *) +val configdir : unit -> string + (** [set_coqlib] must be runned once before any access to [coqlib] *) val set_coqlib : fail:(string -> string) -> unit -(** [docdir] is the path to the Coq documentation. *) -val docdir : unit -> string - (** [coqbin] is the name of the current executable. *) val coqbin : string -- cgit v1.2.3 From 886c222fabd6658d0ef1fe0ed18ff9d5fba9982a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 11:37:17 +0100 Subject: Using the same strategy in coqdoc than in coqtop to guess the coqlib. --- tools/coqdoc/cdglobals.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index a1987387f..ef203960b 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -70,18 +70,21 @@ let normalize_filename f = let dirname = Filename.dirname f in normalize_path dirname, basename +(** Add a local installation suffix (unless the suffix is itself + absolute in which case the prefix does not matter) *) +let use_suffix prefix suffix = + if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix + (** A weaker analog of the function in Envars *) let guess_coqlib () = let file = "theories/Init/Prelude.vo" in + let coqbin = normalize_path (Filename.dirname Sys.executable_name) in + let prefix = Filename.dirname coqbin in + let coqlib = use_suffix prefix Coq_config.coqlibsuffix in + if Sys.file_exists (coqlib / file) then coqlib else if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file) - then Coq_config.coqlib - else - let coqbin = normalize_path (Filename.dirname Sys.executable_name) in - let prefix = Filename.dirname coqbin in - let coqlib = prefix / Coq_config.coqlibsuffix in - if Sys.file_exists (coqlib / file) then coqlib - else prefix + then Coq_config.coqlib else prefix let header_trailer = ref true let header_file = ref "" -- cgit v1.2.3 From a0cec18b3ac2427aaf15d2808cf021a8931a2516 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 11:40:20 +0100 Subject: Configuration with -local definitively seen as an installation layout like others. --- configure.ml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/configure.ml b/configure.ml index 64165fab0..0d2a9881f 100644 --- a/configure.ml +++ b/configure.ml @@ -905,8 +905,10 @@ let find_suffix prefix path = match prefix with else Absolute path -let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,_) = - let dir,suffix = match !uservalue, !Prefs.prefix with +let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout) = + let dir,suffix = + if !Prefs.local then (use_suffix coqtop locallayout,locallayout) + else match !uservalue, !Prefs.prefix with | Some d, p -> d,find_suffix p d | _, Some p -> let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in @@ -920,12 +922,7 @@ let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,_) = if line = "" then (dflt,suffix) else (line,find_suffix p line) in (var,msg,dir,suffix) -let do_one_noinst (var,msg,_,_,_,locallayout) = - (var,msg,use_suffix coqtop locallayout,locallayout) - -let install_dirs = - let f = if !Prefs.local then do_one_noinst else do_one_instdir in - List.map f install +let install_dirs = List.map do_one_instdir install let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs -- cgit v1.2.3