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(-) (limited to 'configure.ml') 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(-) (limited to 'configure.ml') 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(-) (limited to 'configure.ml') 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(-) (limited to 'configure.ml') 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(-) (limited to 'configure.ml') 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(-) (limited to 'configure.ml') 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(-) (limited to 'configure.ml') 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(-) (limited to 'configure.ml') 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 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(-) (limited to 'configure.ml') 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