INSTALL

            INSTALLATION PROCEDURES FOR THE COQ V8.5 SYSTEM
            -----------------------------------------------


WHAT DO YOU NEED ?
==================

   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
   install it. E.g.:

   - Debian GNU/Linux derivatives (or Debian GNU/k*BSD or ...):

     aptitude install coq

   - Gentoo GNU/Linux:

     emerge sci-mathematics/coq

   - Fedora GNU/Linux:

     urpmi coq

   - MacPorts for MacOS X

     port install coq

   To compile Coq V8.5 yourself, you need:

   - Objective Caml version 3.12.1 or later
     (available at http://caml.inria.fr/)

   - Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be less
     well supported)

   - From Objective Caml version 4.06.0, the Num library

   - GNU Make version 3.81 or later

   - a C compiler

   - 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
3. make install (you may need superuser rights)
4. make clean


INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
=================================================

1- Check that you have the Objective Caml compiler installed on your
   computer and that "ocamlc" (or, better, its native code version
   "ocamlc.opt") lies in a directory which is present in your $PATH
   environment variable. At the time of writing this sentence, all
   versions of Objective Caml later or equal to 3.12.1 are
   supported to the exception of Objective Caml 4.02.0.

   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 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 Camlp5/4 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 300 Mb of disk space
   for the whole system in native-code compilation). Once installed, the
   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:

	./configure <options>

   The "configure" script will ask you for directories where to put
   the Coq binaries, standard library, man pages, etc. It will propose
   you some default values.

   For a list of options accepted by the "configure" script, run
   "./configure -help". The main options accepted are:

-prefix <dir>
	Binaries, library, man pages and Emacs mode will be respectively
	installed in <dir>/bin, <dir>/lib/coq, <dir>/man and
	<dir>/lib/emacs/site-lisp

-bindir <dir>                   (default: /usr/local/bin)
        Directory where the binaries will be installed

-libdir <dir>                   (default: /usr/local/lib/coq)
        Directory where the Coq standard library will be installed

-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)
	Directory where the Coq Emacs mode will be installed

-arch <value>			(default is the result of the command "arch")
	An arbitrary architecture name for your machine (useful when
	compiling Coq on two different architectures for which the
	result of "arch" is the same, e.g. Sun OS and Solaris)

-local
        Compile Coq to run in its source directory. The installation (step 6)
        is not necessary in that case.

-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

   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.

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
   configuration time (step 3). Just do

	umask 022
       	make install

   Of course, you may need superuser rights to do that.
   To use the Coq emacs mode you also need to put the following lines
   in you .emacs file:

        (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
        (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)

7- You can now clean all the sources. (You can even erase them.)

	make clean


INSTALLATION PROCEDURE FOR ADVANCED USERS.
==========================================

   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>

   Then compile the sources as described in step 5 above. The resulting
   binaries will reside in the subdirectory bin/.

   If you want to compile the sources for debugging (i.e. with the option
   -g of the Caml compiler) then add the -debug option at configuration
   step :

	./configure -debug <other options>

   and then compile the sources (step 5). Then you must make a Coq toplevel
   including your own tactics, which must be compiled with -g, with coqmktop.
   See the chapter 16 of the Coq Reference Manual for details about how
   to use coqmktop and the Objective Caml debugger with Coq.


THE AVAILABLE COMMANDS.
=======================

   There are two Coq commands:

	coqtop		The Coq toplevel
	coqc		The Coq compiler

   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.

    * `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".

   A detailed description of these commands and of their options is given
   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.

   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 :

   o  save some time during compilation by not cleaning the architecture
      independent files;

   o  save some space during installation by sharing the Coq standard
      library (which is fully architecture independent).

   So, in order to compile Coq for a new architecture, proceed as follows:

   * Omit step 7 above and clean only the architecture dependent files:
     it is done automatically with the command

		make archclean

   * Configure the system for the new architecture:

		./configure <options>

     You can specify the same directory for the standard library but you
     MUST specify a different directory for the binaries (of course).

   * Compile and install the system as described in steps 5 and 6 above.


MOVING BINARIES OR LIBRARY.
===========================

   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: cannot guess a path for Coq libraries; please use -coqlib option

   You can then indicate the new places to Coq, using the options -coqlib :

	coqtop -coqlib <new directory>

   See also next section.


DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
======================================================

   Some bytecode executables of Coq use the OCaml runtime, which dynamically
   loads a shared library (.so or .dll). When it is not installed properly, you
   can get an error message of this kind:

	Fatal error: cannot load shared library dllcoqrun
	Reason: dllcoqrun.so: cannot open shared object file: No such file or directory

   In this case, you need either:
     - to set the CAML_LD_LIBRARY_PATH environment variable to point to the
       directory where dllcoqrun.so is; this is suitable when you want to run
       the command a limited number of times in a controlled environment (e.g.
       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 the shared library:
         ./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:
         ./configure -custom ...
       be aware that stripping executables generated this way, or performing
       other executable-specific operations, will make them useless.