From 69e52c438714e01fbaefc05b61f47a5ae95a7205 Mon Sep 17 00:00:00 2001 From: glondu Date: Sun, 7 Sep 2008 11:45:34 +0000 Subject: Update CHANGES and INSTALL git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11379 85f007b7-540e-0410-9357-904b9bb8a0f7 --- INSTALL | 41 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 40 insertions(+), 1 deletion(-) (limited to 'INSTALL') 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 + Use to open an URL in a browser. %s must appear in , + 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 -libdir + + 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 " ... + where 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. -- cgit v1.2.3