aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL
diff options
context:
space:
mode:
Diffstat (limited to 'INSTALL')
-rw-r--r--INSTALL48
1 files changed, 14 insertions, 34 deletions
diff --git a/INSTALL b/INSTALL
index 2b387b017..955e605c3 100644
--- a/INSTALL
+++ b/INSTALL
@@ -6,19 +6,6 @@
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 MacOS X bundle application, see INSTALL.macosx.
-
- 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. See
- http://caml.inria.fr/ocaml/portability.en.html for details.
-
-
Your OS may already contain Coq under the form of a precompiled
package or ready-to-compile port. In this case, and if the supplied
version suits you, follow the usual procedure for your OS to
@@ -36,34 +23,31 @@ WHAT DO YOU NEED ?
urpmi coq
- - MacOS:
+ - MacPorts for MacOS X
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/)
+ To compile Coq V8.5 yourself, you need:
- - Camlp5 (version >= 6.06) (Coq compiles with Camlp4 but might be less
- well supported)
+ - Objective Caml version 3.12.1 or later
+ (available at http://caml.inria.fr/)
- - GNU Make version 3.81 or later
+ - Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be less
+ well supported)
- - a C compiler
+ - GNU Make version 3.81 or later
- - for Coqide, the Lablgtk development files, and the GTK libraries
- incuding gtksourceview, see INSTALL.ide for more details
+ - a C compiler
- By FTP, Coq comes as a single compressed tar-file. You have
- probably already decompressed it if you are reading this document.
+ - for Coqide, the Lablgtk development files, and the GTK libraries
+ incuding gtksourceview, see INSTALL.ide for more details
QUICK INSTALLATION PROCEDURE.
=============================
1. ./configure
-2. make world
+2. make
3. make install (you may need superuser rights)
4. make clean
@@ -132,17 +116,13 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
Compile Coq to run in its source directory. The installation (step 6)
is not necessary in that case.
--opt
- Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt
- compiler instead of ocamlopt). Makes compilation faster (recommended).
-
-browser <command>
Use <command> to open an URL in a browser. %s must appear in <command>,
and will be replaced by the URL.
5- Still in the root directory, do
- make world
+ make
to compile Coq in Objective Caml bytecode (and native-code if supported).
@@ -219,7 +199,7 @@ THE AVAILABLE COMMANDS.
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/
+ in the Reference Manual (which you can get in the doc/
directory, or read online on http://coq.inria.fr/doc/)
and in the corresponding manual pages.
@@ -291,7 +271,7 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
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;
- - recompile your bytecode executables after reconfiguring the location of
+ - recompile your bytecode executables after reconfiguring the location
of the shared library:
./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
where <path> is the directory where the dllcoqrun.so is installed;