diff options
| -rw-r--r-- | CHANGES | 9 | ||||
| -rw-r--r-- | INSTALL | 41 |
2 files changed, 47 insertions, 3 deletions
@@ -444,8 +444,13 @@ Miscellaneous Whelp search tool. - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into "Test Printing Let for ref" and "Test Printing If for ref". -- An overhauled build system (new Makefiles); see dev/doc/build-system.txt -- Add -browser option to configure script +- An overhauled build system (new Makefiles); see dev/doc/build-system.txt. +- Add -browser option to configure script. +- Build a shared library for the C part of Coq, and use it by default. + Bytecode executables are now pure. The behaviour is configurable with + the -coqrunbyteflags configure option. +- Complexity tests can be skipped by setting the environment variable + COQTEST_SKIPCOMPLEXITY. Changes from V8.1gamma to V8.1 ============================== @@ -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. |