diff options
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rwxr-xr-x | configure | 11 | ||||
| -rw-r--r-- | lib/envars.ml | 23 | ||||
| -rw-r--r-- | lib/envars.mli | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 20 |
5 files changed, 34 insertions, 22 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index e7dd2f1e8..950b0092f 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -10,6 +10,7 @@ val local : bool (* local use (no installation) *) val coqlib : string (* where the std library is installed *) val coqsrc : string (* where are the sources *) +val docdir : string (* where the doc is installed *) val ocaml : string (* names of ocaml binaries *) val ocamlc : string @@ -782,13 +782,13 @@ case $mandir_spec/$prefix_spec/$local in esac case $docdir_spec/$prefix_spec/$local in - yes/*/*) DOCDIR=$docdir; HTMLREFMANDIR=$DOCDIR/html/refman;; - */yes/*) DOCDIR=$prefix/share/doc/coq; HTMLREFMANDIR=$DOCDIR/html/refman;; - */*/true) DOCDIR=$COQTOP/doc; HTMLREFMANDIR=$DOCDIR/refman/html;; + yes/*/*) DOCDIR=$docdir;; + */yes/*) DOCDIR=$prefix/share/doc/coq;; + */*/true) DOCDIR=$COQTOP/doc;; *) printf "Where should I install the Coq documentation [$docdir_def]? " read DOCDIR case $DOCDIR in - "") DOCDIR=$docdir_def; HTMLREFMANDIR=$DOCDIR/html/refman;; + "") DOCDIR=$docdir_def;; *) true;; esac;; esac @@ -1002,6 +1002,7 @@ let local = $local let coqrunbyteflags = "$COQRUNBYTEFLAGS" let coqlib = "$LIBDIR" let coqsrc = "$COQSRC" +let docdir = "$DOCDIR" let ocaml = "$ocamlexec" let ocamlc = "$bytecamlc" let ocamlopt = "$nativecamlc" @@ -1037,7 +1038,7 @@ let browser = "$BROWSER" let wwwcoq = "$WWWCOQ" let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/" let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/" -let localwwwrefman = "file://$HTMLREFMANDIR/" +let localwwwrefman = "file:/" ^ docdir ^ "html/refman" END_OF_COQ_CONFIG diff --git a/lib/envars.ml b/lib/envars.ml index f19834527..c260a8648 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -21,23 +21,26 @@ let _ = if Coq_config.arch = "win32" then 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 + if Sys.file_exists (Filename.concat out testfile) then out else oth + let guess_coqlib () = let file = "states/initial.coq" in if Sys.file_exists (Filename.concat Coq_config.coqlib file) then Coq_config.coqlib - else - let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in - let prefix = Filename.dirname coqbin in - let rpath = if Coq_config.local then [] else - (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in - let coqlib = List.fold_left Filename.concat prefix rpath 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" + else reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file + (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 ()) +let docdir () = + reldir (if Coq_config.arch = "win32" then ["doc"] else ["share";"doc";"coq"]) "html" Coq_config.docdir + let path_to_list p = let sep = if Sys.os_type = "Win32" then ';' else ':' in Util.split_string_at sep p @@ -84,7 +87,9 @@ let camllib () = let camlp4bin () = if !Flags.camlp4bin_spec then !Flags.camlp4bin else if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () with _ -> Coq_config.camlp4bin + try guess_camlp4bin () with _ -> let cb = camlbin () in + if Sys.file_exists (Filename.concat cb Coq_config.camlp4) then cb + else Coq_config.camlp4bin let camlp4lib () = if !Flags.boot diff --git a/lib/envars.mli b/lib/envars.mli index 6d053be6d..c8a372906 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -10,6 +10,7 @@ as coqlib) *) val coqlib : unit -> string +val docdir : unit -> string val coqbin : unit -> string (* coqpath is stored in reverse order, since that is the order it * gets added to the searc path *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e09706325..93ef0b201 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -91,12 +91,16 @@ let print_usage_coqc () = let print_config () = if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; - Printf.printf "COQLIB=%s/\n" Coq_config.coqlib; - Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc; - Printf.printf "CAMLBIN=%s/\n" Coq_config.camlbin; - Printf.printf "CAMLLIB=%s/\n" Coq_config.camllib; + Printf.printf "COQLIB=%s/\n" (Envars.coqlib ()); + (*Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc;*) + Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); + Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep; + Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc; + Printf.printf "OCAMLOPT=%s\n" Coq_config.ocamlopt; + Printf.printf "OCAMLDOC=%s\n" Coq_config.ocamldoc; + Printf.printf "CAMLBIN=%s/\n" (Envars.camlbin ()); + Printf.printf "CAMLLIB=%s/\n" (Envars.camllib ()); Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; - Printf.printf "CAMLP4BIN=%s\n" Coq_config.camlp4bin; - Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib - - + Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ()); + Printf.printf "CAMLP4LIB=%s\n" (Envars.camlp4lib ()); + Printf.printf "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false") |