From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- INSTALL | 48 +++++++++++++++++++++++++++--------------------- 1 file changed, 27 insertions(+), 21 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index b1cc3af1..e88dc319 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 Objective Caml - can compile to native code, rather than only bytecode. At time of + Naturally, Coq will run faster on an architecture where OCaml 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. @@ -39,16 +39,12 @@ WHAT DO YOU NEED ? urpmi coq - Should you need or prefer to compile Coq V8.3 yourself, you need: + Should you need or prefer to compile Coq V8.2 yourself, you need: - - Objective Caml version 3.10.2 or later + - Objective Caml version 3.10.0 or later (available at http://caml.inria.fr/) - 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) - + - Camlp5 (version <= 4.08, or 5.* transitional) - GNU Make version 3.81 or later ( @@ -75,6 +71,9 @@ 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. ============================= @@ -88,7 +87,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.10.2 (or later) +1- Check that you have the Objective Caml compiler version 3.10.0 (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. @@ -98,16 +97,23 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). bigger), you will also need the "ocamlopt" (or its native code version "ocamlopt.opt") command. -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 +2- Check that you have Camlp4 installed on your + computer and that the command "camlp4" lies in a directory which is present in your $PATH environment variable path. - (You need Camlp5 in transitional mode and in both bytecode and - native versions if your platform supports it). + (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. -2- You will need about 400Mo free on your disk to compile Coq in full - with its standard library and documentation. +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. -3- First you need to configure the system. It is done automatically with +4- First you need to configure the system. It is done automatically with the command: ./configure @@ -201,7 +207,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 ocaml compiler) then add the -debug option at configuration + -g of the Caml compiler) then add the -debug option at configuration step : ./configure -debug @@ -316,7 +322,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: @@ -329,12 +335,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 Objective Caml; + 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 + - (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