From a0a94c1340a63cdb824507b973393882666ba52a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 19 Feb 2009 13:13:14 +0100 Subject: Imported Upstream version 8.2-1+dfsg --- INSTALL | 34 +++++++++++++++------------------- 1 file changed, 15 insertions(+), 19 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 626417d6..47d2cb2e 100644 --- a/INSTALL +++ b/INSTALL @@ -71,10 +71,12 @@ WHAT DO YOU NEED ? - a C compiler - - for Coqide, the Lablgtk development files, and the GTK libraries, see INSTALL.ide for more details + - 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. + Coq sources distribution comes as a single compressed tar-file. You + have probably already decompressed it if you are reading this + document. QUICK INSTALLATION PROCEDURE. @@ -99,21 +101,18 @@ 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 - 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. +2- If you are using OCaml version >= 3.10.0, 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 Camlp5 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 + space during the compilation (reckon on about 250 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. + binaries take about 65 Mb, and the library about 60 Mb. 4- First you need to configure the system. It is done automatically with the command: @@ -313,12 +312,9 @@ MOVING BINARIES OR LIBRARY. Error: Can't find file initial.coq on loadpath If you really have (or want) to move the binaries or the library, then - you have to indicate their new places to Coq, using the options -bindir (for - the binaries directory) and -libdir (for the standard library directory) : - - coqtop -bindir -libdir + you have to indicate where Coq will find the libraries: - See also next section. + coqtop -coqlib DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. @@ -344,6 +340,6 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. 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 ... + ./configure -custom ... be aware that stripping executables generated this way, or performing other executable-specific operations, will make them useless. -- cgit v1.2.3