From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- INSTALL | 46 +++++++++++++++++++--------------------------- 1 file changed, 19 insertions(+), 27 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 903465de..b1cc3af1 100644 --- a/INSTALL +++ b/INSTALL @@ -15,8 +15,8 @@ WHAT DO YOU NEED ? ppc) and FreeBSD. Automated tests are run under many, many different architectures under GNU/Linux. - Naturally, Coq will run faster on an architecture where OCaml can - compile to native code, rather than only bytecode. At time of + Naturally, Coq will run faster on an architecture where Objective Caml + can compile to native code, rather than only bytecode. At time of writing, that is IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64, HPPA and StrongArm. See http://caml.inria.fr/ocaml/portability.en.html for details. @@ -41,11 +41,13 @@ WHAT DO YOU NEED ? Should you need or prefer to compile Coq V8.3 yourself, you need: - - Objective Caml version 3.09.3 or later + - Objective Caml version 3.10.2 or later (available at http://caml.inria.fr/) - For Ocaml version >= 3.10.0, you also need to install camlp5 - (version <= 4.08, or 5.01 transitional) + For Objective Caml version >= 3.10.0, you also need to install + camlp5 (use "transitional" mode and choose a version compatible + with the corresponding version of Objective Caml, however + avoiding version 5.00) - GNU Make version 3.81 or later @@ -73,9 +75,6 @@ WHAT DO YOU NEED ? - for Coqide, the Lablgtk development files, and the GTK libraries, see INSTALL.ide for more details - By FTP, Coq comes as a single compressed tar-file. You have - probably already decompressed it if you are reading this document. - QUICK INSTALLATION PROCEDURE. ============================= @@ -89,7 +88,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.09.3 (or later) +1- Check that you have the Objective Caml compiler version 3.10.2 (or later) installed on your computer and that "ocamlmktop" and "ocamlc" (or its native code version "ocamlc.opt") lie in a directory which is present in your $PATH environment variable. @@ -99,23 +98,16 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). bigger), you will also need the "ocamlopt" (or its native code version "ocamlopt.opt") command. -2- Check that you have Camlp4 installed on your - computer and that the command "camlp4" lies in a directory which +2- If using Ocaml >= 3.10, check that you have Camlp5 installed on your + computer and that the command "camlp5" lies in a directory which is present in your $PATH environment variable path. - (You need Camlp4 in both bytecode and native versions if - your platform supports it). - - Note: in the latest ocaml distributions, camlp4 comes with ocaml so - you do not have to check this point anymore. + (You need Camlp5 in transitional mode and in both bytecode and + native versions if your platform supports it). -3- The uncompression and un-tarring of the distribution file gave birth - to a directory named "coq-8.xx". You can rename this directory and put - it wherever you want. Just keep in mind that you will need some spare - space during the compilation (reckon on about 50 Mb of disk space - for the whole system in native-code compilation). Once installed, the - binaries take about 14 Mb, and the library about 9 Mb. +2- You will need about 400Mo free on your disk to compile Coq in full + with its standard library and documentation. -4- First you need to configure the system. It is done automatically with +3- First you need to configure the system. It is done automatically with the command: ./configure @@ -209,7 +201,7 @@ INSTALLATION PROCEDURE FOR ADVANCED USERS. binaries will reside in the subdirectory bin/. If you want to compile the sources for debugging (i.e. with the option - -g of the Caml compiler) then add the -debug option at configuration + -g of the ocaml compiler) then add the -debug option at configuration step : ./configure -debug @@ -324,7 +316,7 @@ MOVING BINARIES OR LIBRARY. DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. ====================================================== - Some bytecode executables of Coq use the OCaml runtime, which dynamically + 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: @@ -337,12 +329,12 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. 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; + the directory of the standard library of Objective Caml; - 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 + - (not recommended) compile bytecode executables with a custom ocaml runtime by using: ./configure -custom ... be aware that stripping executables generated this way, or performing -- cgit v1.2.3