From 0e4c44431739bd607f3eb95d6287ea35b4613e5d Mon Sep 17 00:00:00 2001 From: glondu Date: Tue, 27 Sep 2011 13:59:42 +0000 Subject: In Coq_config: get rid of coqsrc and make coqlib optional I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7 --- config/coq_config.mli | 3 +-- configure | 10 ++++++++-- ide/coq.ml | 7 ++++++- lib/envars.ml | 28 +++++++++++++++++----------- lib/envars.mli | 3 ++- lib/flags.ml | 14 +++++++++++++- myocamlbuild.ml | 5 +---- plugins/xml/xmlcommand.ml | 2 +- scripts/coqc.ml | 2 +- tools/coqdoc/cdglobals.ml | 41 ++++++++++++++++++++++++++++++----------- tools/coqdoc/main.ml | 25 +++++-------------------- toplevel/coqinit.ml | 3 +-- 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 *) diff --git a/configure b/configure index 0a7619740..f771c5e30 100755 --- a/configure +++ b/configure @@ -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 "" 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; -- cgit v1.2.3