diff options
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 34 |
1 files changed, 15 insertions, 19 deletions
@@ -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 <new directory> -libdir <new directory> + you have to indicate where Coq will find the libraries: - See also next section. + coqtop -coqlib <directory> DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. @@ -344,6 +340,6 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. 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 ... + ./configure -custom ... be aware that stripping executables generated this way, or performing other executable-specific operations, will make them useless. |