diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/envars.ml | 28 | ||||
| -rw-r--r-- | lib/envars.mli | 3 | ||||
| -rw-r--r-- | lib/flags.ml | 14 |
3 files changed, 32 insertions, 13 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index 4f33ccb7f3..0991fb7a12 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -9,34 +9,40 @@ (* This file gathers environment variables needed by Coq to run (such as coqlib) *) -let coqbin () = - if !Flags.boot || Coq_config.local - then Filename.concat Coq_config.coqsrc "bin" - else System.canonical_path_name (Filename.dirname Sys.executable_name) +let coqbin = + System.canonical_path_name (Filename.dirname Sys.executable_name) + +(* The following only makes sense when executables are running from + source tree (e.g. during build or in local mode). *) +let coqroot = Filename.dirname coqbin (* On win32, we add coqbin to the PATH at launch-time (this used to be done in a .bat script). *) let _ = if Coq_config.arch = "win32" then - Unix.putenv "PATH" (coqbin() ^ ";" ^ System.getenv_else "PATH" "") + Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "") let reldir instdir testfile oth = - let prefix = Filename.dirname (coqbin ()) in let rpath = if Coq_config.local then [] else instdir in - let out = List.fold_left Filename.concat prefix rpath in + let out = List.fold_left Filename.concat coqroot rpath in if Sys.file_exists (Filename.concat out testfile) then out else oth () let guess_coqlib () = let file = "states/initial.coq" in reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file - (fun () -> if Sys.file_exists (Filename.concat Coq_config.coqlib file) - then Coq_config.coqlib - else Util.error "cannot guess a path for Coq libraries; please use -coqlib option") + (fun () -> + let coqlib = match Coq_config.coqlib with + | Some coqlib -> coqlib + | None -> coqroot + in + if Sys.file_exists (Filename.concat coqlib file) + then coqlib + else Util.error "cannot guess a path for Coq libraries; please use -coqlib option") let coqlib () = if !Flags.coqlib_spec then !Flags.coqlib else - (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ()) + (if !Flags.boot then coqroot else guess_coqlib ()) let docdir () = reldir (if Coq_config.arch = "win32" then ["doc"] else ["share";"doc";"coq"]) "html" (fun () -> Coq_config.docdir) diff --git a/lib/envars.mli b/lib/envars.mli index c8a372906c..3f8ac5ecc2 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -11,7 +11,8 @@ val coqlib : unit -> string val docdir : unit -> string -val coqbin : unit -> string +val coqbin : string +val coqroot : string (* coqpath is stored in reverse order, since that is the order it * gets added to the searc path *) val coqpath : unit -> string list diff --git a/lib/flags.ml b/lib/flags.ml index 9b19efea78..470cf81f18 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -115,9 +115,21 @@ let is_standard_doc_url url = url = Coq_config.wwwrefman || url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) +(* same as in System, but copied here because of dependencies *) +let canonical_path_name p = + let current = Sys.getcwd () in + Sys.chdir p; + let result = Sys.getcwd () in + Sys.chdir current; + result + (* Options for changing coqlib *) let coqlib_spec = ref false -let coqlib = ref Coq_config.coqlib +let coqlib = ref ( + (* same as Envars.coqroot, but copied here because of dependencies *) + Filename.dirname + (canonical_path_name (Filename.dirname Sys.executable_name)) +) (* Options for changing camlbin (used by coqmktop) *) let camlbin_spec = ref false |