diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-27 13:59:42 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-27 13:59:42 +0000 |
| commit | 0e4c44431739bd607f3eb95d6287ea35b4613e5d (patch) | |
| tree | 4691781534276f65a4c37d10b7a37579748d97c0 /config | |
| parent | 9ab628374131e60217d550d670027b531125a74e (diff) | |
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
Diffstat (limited to 'config')
| -rw-r--r-- | config/coq_config.mli | 3 |
1 files changed, 1 insertions, 2 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 *) |