diff options
| -rw-r--r-- | config/coq_config.mli | 3 | ||||
| -rwxr-xr-x | configure | 10 | ||||
| -rw-r--r-- | ide/coq.ml | 7 | ||||
| -rw-r--r-- | lib/envars.ml | 28 | ||||
| -rw-r--r-- | lib/envars.mli | 3 | ||||
| -rw-r--r-- | lib/flags.ml | 14 | ||||
| -rw-r--r-- | myocamlbuild.ml | 5 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 2 | ||||
| -rw-r--r-- | scripts/coqc.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/cdglobals.ml | 41 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 25 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 3 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
13 files changed, 86 insertions, 58 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index 5e393e320..4ad8dc58f 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -8,8 +8,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 coqlib : string option (* where the std library is installed *) val docdir : string (* where the doc is installed *) val ocaml : string (* names of ocaml binaries *) @@ -757,6 +757,7 @@ esac case $libdir_spec/$prefix_spec/$local in yes/*/*) LIBDIR=$libdir;; */yes/*) + libdir_spec=yes case $ARCH in win32) LIBDIR=$prefix ;; *) LIBDIR=$prefix/lib/coq ;; @@ -764,12 +765,18 @@ case $libdir_spec/$prefix_spec/$local in */*/true) LIBDIR=$COQTOP ;; *) printf "Where should I install the Coq library [$libdir_def]? " read LIBDIR + libdir_spec=yes case $LIBDIR in "") LIBDIR=$libdir_def;; *) true;; esac;; esac +case $libdir_spec in + yes) LIBDIR_OPTION="Some \"$LIBDIR\"";; + *) LIBDIR_OPTION="None";; +esac + case $mandir_spec/$prefix_spec/$local in yes/*/*) MANDIR=$mandir;; */yes/*) MANDIR=$prefix/man ;; @@ -1001,8 +1008,7 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file let local = $local let coqrunbyteflags = "$COQRUNBYTEFLAGS" -let coqlib = "$LIBDIR" -let coqsrc = "$COQSRC" +let coqlib = $LIBDIR_OPTION let docdir = "$DOCDIR" let ocaml = "$ocamlexec" let ocamlc = "$bytecamlc" diff --git a/ide/coq.ml b/ide/coq.ml index a5b2d38ab..f635ad407 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -16,7 +16,12 @@ let get_version_date () = then Coq_config.date else "<date not printable>" in try - let ch = open_in (Coq_config.coqsrc^"/revision") in + (* the following makes sense only when running with local layout *) + let coqroot = Filename.concat + (Filename.dirname Sys.executable_name) + Filename.parent_dir_name + in + let ch = open_in (Filename.concat coqroot "revision") in let ver = input_line ch in let rev = input_line ch in (ver,rev) diff --git a/lib/envars.ml b/lib/envars.ml index 4f33ccb7f..0991fb7a1 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 c8a372906..3f8ac5ecc 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 9b19efea7..470cf81f1 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 diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 9f3dca6ac..6ffd3e2a5 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -92,7 +92,6 @@ let flag_dynlink = if hasdynlink then A"-DHasDynlink" else N let dep_dynlink = if hasdynlink then N else Sh"-natdynlink no" let lablgtkincl = Sh Coq_config.coqideincl let local = Coq_config.local -let coqsrc = Coq_config.coqsrc let cflags = S[A"-ccopt";A Coq_config.cflags] (** Do we want to inspect .ml generated from .ml4 ? *) @@ -261,10 +260,8 @@ let extra_rules () = begin if w32 then cp "config/coq_config.ml" "coq_config.ml" else let lines = read_file "config/coq_config.ml" in let lines = List.map (fun s -> s^"\n") lines in - let srcbuild = Filename.concat coqsrc !_build in let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in - let line1 = "let coqsrc = \""^srcbuild^"\"\n" in - let line2 = "let coqlib = \""^srcbuild^"\"\n" in + let line2 = "let coqlib = None\n" in (* TODO : line3 isn't completely accurate with respect to ./configure: the case of -local -coqrunbyteflags foo isn't supported *) let line3 = diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 78048c8ee..1037bbf08 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -652,7 +652,7 @@ let _ = end ; Option.iter (fun fn -> - let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in + let coqdoc = Filename.concat Envars.coqbin ("coqdoc" ^ Coq_config.exec_extension) in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then diff --git a/scripts/coqc.ml b/scripts/coqc.ml index b1e91cb30..688f7c32a 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -192,7 +192,7 @@ let main () = end; let coqtopname = if !image <> "" then !image - else Filename.concat (Envars.coqbin ()) (!binary ^ Coq_config.exec_extension) + else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension) in (* List.iter (compile coqtopname args) cfiles*) Unix.handle_unix_error (compile coqtopname args) cfiles diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index a412e6865..6b8a3f5e7 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -49,21 +49,40 @@ type glob_source_t = let glob_source = ref DotGlob +(*s Manipulations of paths and path aliases *) + +let normalize_path p = + (* We use the Unix subsystem to normalize a physical path (relative + or absolute) and get rid of symbolic links, relative links (like + ./ or ../ in the middle of the path; it's tricky but it + works... *) + (* Rq: Sys.getcwd () returns paths without '/' at the end *) + let orig = Sys.getcwd () in + Sys.chdir p; + let res = Sys.getcwd () in + Sys.chdir orig; + res + +let normalize_filename f = + let basename = Filename.basename f in + let dirname = Filename.dirname f in + normalize_path dirname, basename + (** A weaker analog of the function in Envars *) 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 = 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 - Coq_config.coqlib + match Coq_config.coqlib with + | Some coqlib when Sys.file_exists (Filename.concat 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 = "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 prefix let header_trailer = ref true let header_file = ref "" diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 98204a856..7dc2c3bf2 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -106,25 +106,6 @@ let check_if_file_exists f = end -(*s Manipulations of paths and path aliases *) - -let normalize_path p = - (* We use the Unix subsystem to normalize a physical path (relative - or absolute) and get rid of symbolic links, relative links (like - ./ or ../ in the middle of the path; it's tricky but it - works... *) - (* Rq: Sys.getcwd () returns paths without '/' at the end *) - let orig = Sys.getcwd () in - Sys.chdir p; - let res = Sys.getcwd () in - Sys.chdir orig; - res - -let normalize_filename f = - let basename = Filename.basename f in - let dirname = Filename.dirname f in - normalize_path dirname, basename - (* [paths] maps a physical path to a name *) let paths = ref [] @@ -354,7 +335,11 @@ let parse () = | ("--coqlib" | "-coqlib") :: [] -> usage () | ("--boot" | "-boot") :: rem -> - Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem + Cdglobals.coqlib_path := normalize_path ( + Filename.concat + (Filename.dirname Sys.executable_name) + Filename.parent_dir_name + ); parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: d :: rem -> Cdglobals.coqlib_path := d; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: [] -> diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 977b8f4c7..e91cf3353 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -121,9 +121,8 @@ let init_library_roots () = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = - let coqsrc = Coq_config.coqsrc in let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) + Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl) in Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 93ef0b201..512632316 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -92,7 +92,6 @@ 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" (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; |