aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-07 11:45:34 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-07 11:45:34 +0000
commit69e52c438714e01fbaefc05b61f47a5ae95a7205 (patch)
tree2d85f30d0b27a57952792b70b6078ecb57f2ea4f /INSTALL
parenteb54de0f8a4c0fd1d1240f91baab103d527b659a (diff)
Update CHANGES and INSTALL
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11379 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'INSTALL')
-rw-r--r--INSTALL41
1 files changed, 40 insertions, 1 deletions
diff --git a/INSTALL b/INSTALL
index ed12c6eb2..b9b7a6194 100644
--- a/INSTALL
+++ b/INSTALL
@@ -2,6 +2,7 @@
INSTALLATION PROCEDURES FOR THE COQ V8.1 SYSTEM
-----------------------------------------------
+
WHAT DO YOU NEED ?
==================
@@ -38,7 +39,7 @@ WHAT DO YOU NEED ?
urpmi coq
- Should you need or prefer to compile Coq V8.1 yourself, you need:
+ Should you need or prefer to compile Coq V8.2 yourself, you need:
- Objective Caml version 3.07 or later
(available at http://caml.inria.fr/)
@@ -160,6 +161,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
Disable the Objective Caml compiler warnings. This option has no
effect on the result of the compilation.
+-browser <command>
+ Use <command> to open an URL in a browser. %s must appear in <command>,
+ and will be replaced by the URL.
+
5- Still in the root directory, do
make world
@@ -249,6 +254,7 @@ THE AVAILABLE COMMANDS.
There is also a tutorial and a FAQ; see http://coq.inria.fr/doc1-eng.html
+
COMMON PROBLEMS.
================
@@ -263,6 +269,9 @@ COMMON PROBLEMS.
not be present on certain systems. To fix that, try to replace
mkdirhier with mkdir -p
+ * See also section on dynamically loaded libraries.
+
+
COMPILING FOR DIFFERENT ARCHITECTURES.
======================================
@@ -308,3 +317,33 @@ MOVING BINARIES OR LIBRARY.
the binaries directory) and -libdir (for the standard library directory) :
coqtop -bindir <new directory> -libdir <new directory>
+
+ See also next section.
+
+
+DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
+======================================================
+
+ Some bytecode executables of Coq use the OCaml runtime, which dynamically
+ loads a shared library (.so or .dll). When it is not installed properly, you
+ can get an error message of this kind:
+
+ Fatal error: cannot load shared library dllcoqrun
+ Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
+
+ In this case, you need either:
+ - to set the CAML_LD_LIBRARY_PATH environment variable to point to the
+ directory where dllcoqrun.so is; this is suitable when you want to run
+ the command a limited number of times in a controlled environment (e.g.
+ during compilation of binary packages);
+ - install dllcoqrun.so in a location listed in the file ld.conf that is in
+ the directory of the standard library of OCaml;
+ - recompile your bytecode executables after reconfiguring the location of
+ of the shared library:
+ ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ...
+ where <path> is the directory where the dllcoqrun.so is installed;
+ - (not recommended) compile bytecode executables with a custom OCaml
+ runtime by using:
+ ./configure -coqrunbyteflags -custom ...
+ be aware that stripping executables generated this way, or performing
+ other executable-specific operations, will make them useless.