diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-12 03:08:56 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 12:12:56 +0200 |
commit | d53ba17d1761261593c598b6a88cfd6ce0eb3514 (patch) | |
tree | df442236534c337d8eaba771ff15bebf4e806240 | |
parent | 34a2f9eb315da8b794f2573bdfc8ff941d81bdbe (diff) |
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.
-rw-r--r-- | config/coq_config.mli | 2 | ||||
-rw-r--r-- | configure.ml | 5 | ||||
-rw-r--r-- | lib/envars.ml | 7 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 8 | ||||
-rw-r--r-- | 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 "" |