aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--INSTALL118
1 files changed, 48 insertions, 70 deletions
diff --git a/INSTALL b/INSTALL
index 276c57601..595fc606b 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,24 +1,21 @@
- INSTALLATION PROCEDURES FOR THE COQ V8.4 SYSTEM
+ INSTALLATION PROCEDURES FOR THE COQ V8.5 SYSTEM
-----------------------------------------------
WHAT DO YOU NEED ?
==================
- Coq is designed to work on computers equipped with a POSIX (Unix or
- a clone) operating system. It also works under Microsoft Windows
- (see INSTALL.win); for a precompiled MacOS X package, see
- INSTALL.macosx.
+ Coq is designed to work on computers equipped with a POSIX (Unix or a
+ clone) operating system. It also works under Microsoft Windows (see
+ INSTALL.win); for a MacOS X bundle application, see INSTALL.macosx.
- Coq is known to be actively used under GNU/Linux (i386, amd64 and
- ppc) and FreeBSD. Automated tests are run under many, many
- different architectures under GNU/Linux.
+ Coq is known to be actively used under GNU/Linux (i386 and amd64) 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
- writing, that is IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64,
- HPPA and StrongArm. See
+ Naturally, Coq will run faster on an architecture where OCaml can compile
+ to native code, rather than only bytecode. See
http://caml.inria.fr/ocaml/portability.en.html for details.
@@ -27,50 +24,36 @@ WHAT DO YOU NEED ?
version suits you, follow the usual procedure for your OS to
install it. E.g.:
- - Debian GNU/Linux (or Debian GNU/k*BSD or ...):
+ - Debian GNU/Linux derivatives (or Debian GNU/k*BSD or ...):
aptitude install coq
- - Gentoo GNU/Linux:
+ - Gentoo GNU/Linux:
emerge sci-mathematics/coq
- - Mandriva GNU/Linux:
+ - Fedora GNU/Linux:
urpmi coq
- Should you need or prefer to compile Coq V8.4 yourself, you need:
+ - MacOS:
+
+ port install coq
+
+ Should you need or prefer to compile Coq V8.5 yourself, you need:
- Objective Caml version 3.12.1 or later
(available at http://caml.inria.fr/)
- - Camlp5 (version <= 4.08, or 5.* transitional)
+ - Camlp5 (version >= 6.06) (Coq compiles with Camlp4 but might be less
+ well supported)
- GNU Make version 3.81 or later
- (
- available at http://www.gnu.org/software/make/, but also a
- standard or optional add-on part to most Unices and Unix
- clones, sometimes under the name "gmake".
-
- If a new enough version is not included in your system, nor
- easily available as an add-on, this should get you a working
- make:
-
- #Download it (wget is an example, use your favourite FTP or HTTP client)
- wget http://ftp.gnu.org/pub/gnu/make/make-3.81.tar.bz2
- bzip2 -cd make-3.81.tar.bz2 | tar x
- #If you don't have bzip2, you can download the gzipped version instead.
- cd make-3.81
- ./configure --prefix=${HOME}
- make install
-
- Then, make sure that ${HOME}/bin is first in your $PATH.
- )
- 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
+ incuding gtksourceview, 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.
@@ -98,21 +81,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
+2- Check that you have Camlp5 (or a supported Camlp4) 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
+ (You need Camlp5/4 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.
-
-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
+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 300 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 30 Mb, and the library about 200 Mb.
4- First you need to configure the system. It is done automatically with
the command:
@@ -137,7 +117,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
-libdir <dir> (default: /usr/local/lib/coq)
Directory where the Coq standard library will be installed
--mandir <dir> (default: /usr/local/man)
+-mandir <dir> (default: /usr/local/share/man)
Directory where the Coq manual pages will be installed
-emacslib <dir> (default: /usr/local/lib/emacs/site-lisp)
@@ -153,7 +133,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
is not necessary in that case.
-opt
- Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt
+ Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt
compiler instead of ocamlopt). Makes compilation faster (recommended).
-browser <command>
@@ -167,7 +147,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
to compile Coq in Objective Caml bytecode (and native-code if supported).
This will compile the entire system. This phase can take more or less time,
- depending on your architecture and is fairly verbose.
+ depending on your architecture and is fairly verbose.
6- You can now install the Coq system. Executables, libraries, manual pages
and emacs mode are copied in some standard places of your system, defined at
@@ -191,12 +171,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
INSTALLATION PROCEDURE FOR ADVANCED USERS.
==========================================
- If you wish to write tactics (and that really means that you belong
- to advanced users!) you *must* keep the Coq sources, without cleaning
- them. Therefore, to avoid a duplication of binaries and library, it is
- not necessary to do the installation step (6- above).
- You just have to tell it at configuration step (4- above) with the
- option -local :
+ If you wish to write plugins you *must* keep the Coq sources, without
+ cleaning them. Therefore, to avoid a duplication of binaries and library,
+ it is not necessary to do the installation step (6- above). You just have
+ to tell it at configuration step (4- above) with the option -local :
./configure -local <other options>
@@ -219,15 +197,15 @@ THE AVAILABLE COMMANDS.
=======================
There are two Coq commands:
-
+
coqtop The Coq toplevel
coqc The Coq compiler
- There are actually two binaries for the interactive system, coqtop.byte
- and coqtop.opt (respectively bytecode and native code versions of Coq).
- coqtop is a link to the fastest version, i.e. coqtop.opt if any, and
- coqtop.byte otherwise. coqc also invokes the fastest version of Coq.
- Options -opt and -byte to coqtop and coqc selects a particular binary.
+ Under architecture where ocamlopt is available, there are actually two
+ binaries for the interactive system, coqtop.byte and coqtop (respectively
+ bytecode and native code versions of Coq). coqtop is a link to coqtop.byte
+ otherwise. coqc also invokes the fastest version of Coq. Options -opt and
+ -byte to coqtop and coqc selects a particular binary.
* `coqtop' launches Coq in the interactive mode. By default it loads
basic logical definitions and tactics from the Init directory.
@@ -237,24 +215,24 @@ THE AVAILABLE COMMANDS.
coqc foo.v
- It will produce a file foo.vo, that you can now load through the Coq
- command "Require".
+ It will produce a file foo.vo, that you can now load through the Coq
+ command "Require".
A detailed description of these commands and of their options is given
in the Reference Manual (which you can get by FTP, in the doc/
directory, or read online on http://coq.inria.fr/doc/)
and in the corresponding manual pages.
- There is also a tutorial and a FAQ; see http://coq.inria.fr/doc1-eng.html
+ There is also a tutorial and a FAQ; see http://coq.inria.fr/getting-started
COMPILING FOR DIFFERENT ARCHITECTURES.
======================================
- This section explains how to compile Coq for several architecture,
- sharing the same sources. The important fact is that some files are
- architecture dependent (.cmx, .o and executable files for instance)
- but others are not (.cmo and .vo). Consequently, you can :
+ This section explains how to compile Coq for several architecture, sharing
+ the same sources. The important fact is that some files are architecture
+ dependent (.cmx, .o and executable files for instance) but others are not
+ (.cmo and .vo). Consequently, you can :
o save some time during compilation by not cleaning the architecture
independent files;