From 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 8 Sep 2008 00:15:04 +0200 Subject: Imported Upstream version 8.2~beta4.svn20080907+dfsg --- INSTALL | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 68cd2faf..626417d6 100644 --- a/INSTALL +++ b/INSTALL @@ -2,6 +2,7 @@ INSTALLATION PROCEDURES FOR THE COQ V8.2 SYSTEM ----------------------------------------------- + WHAT DO YOU NEED ? ================== @@ -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