Imported Upstream version 8.5~beta1+dfsg

1 files changed, 63 insertions, 104 deletions

diff --git a/INSTALL b/INSTALL
index 15f1b90a..2b387b01 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,49 +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:
 
-     - Objective Caml version 3.11.2 or later
+     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.
@@ -87,31 +71,28 @@ QUICK INSTALLATION PROCEDURE.
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
 
-1- Check that you have the Objective Caml compiler version 3.11.2 (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. 
+1- Check that you have the Objective Caml compiler version 3.12.1 (or later)
+   installed on your computer and that "ocamlc" (or its native code version
+   "ocamlc.opt") lie in a directory which is present in your $PATH environment
+   variable.
 
    To get Coq in native-code, (it runs 4 to 10 times faster than
    bytecode, but it takes more time to get compiled and the binary is
    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:
@@ -136,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)
@@ -152,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>
@@ -166,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
@@ -180,7 +161,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
    in you .emacs file:
 
         (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-        (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
+        (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
 
 7- You can now clean all the sources. (You can even erase them.)
 
@@ -190,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>
 
@@ -218,61 +197,42 @@ 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. The default state
-      (see the "-inputstate" option) is `initial.coq', which contains some 
-      basic logical definitions, the associated parsing and printing rules,
-      and the following tactic modules: Equality, Tauto, Inv, EAuto and Refine.
+    * `coqtop' launches Coq in the interactive mode. By default it loads
+      basic logical definitions and tactics from the Init directory.
 
     * `coqc' allows compilation of Coq files directly from the command line.
       To compile a file foo.v, do:
 
 		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
-
-
-COMMON PROBLEMS.
-================
-
-    * On some sites, when running `./configure', `pwd' returned a 
-    path which is not valid from another machine (it may look like 
-    "/tmp_mnt/foo/...") and, as a consequence, you won't be able to run
-    coqtop or coqc. The solution is to give the correct value, with
-
-	./configure -src <correct path> <other options>
-
-    * The `make install' procedure uses mkdirhier, a program that may
-   not be present on certain systems. To fix that, try to replace
-   mkdirhier with mkdir -p
-
-    * See also section on dynamically loaded libraries.
+   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;
@@ -300,17 +260,16 @@ COMPILING FOR DIFFERENT ARCHITECTURES.
 MOVING BINARIES OR LIBRARY.
 ===========================
 
-   If you move the binaries or the library, Coq will be "lost".
-   Running "coqtop" would then return an error message of the kind:
+   If you move both the binaries and the library in a consistent way,
+   Coq should be able to still run. Otherwise, Coq may be "lost",
+   running "coqtop" would then return an error message of the kind:
 
 	Error during initialization :
-	Error: Can't find file initial.coq on loadpath
+	Error: cannot guess a path for Coq libraries; please use -coqlib option
 
-   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) :
+   You can then indicate the new places to Coq, using the options -coqlib :
 
-	coqtop -bindir <new directory> -libdir <new directory>
+	coqtop -coqlib <new directory>
 
    See also next section.
 
@@ -334,7 +293,7 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
        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 <path>" ...
+         ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
        where <path> is the directory where the dllcoqrun.so is installed;
      - (not recommended) compile bytecode executables with a custom OCaml
        runtime by using: