path: root/INSTALL

            INSTALLATION PROCEDURES FOR THE COQ V7 SYSTEM
            ---------------------------------------------

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

   Coq is designed to work on computers equipped with the Unix operating 
   system. In order to compile Coq V7 you need:

     - Objective Caml version 3.00 or later
       (available at http://caml.inria.fr/)
  
     - the Camlp4 preprocessor with same version number as ocaml
       (available at http://caml.inria.fr/camlp4/)

   Until now, it has mainly been tested on Sun workstations running Solaris,
   and DEC alpha and Pentium workstations running Linux. By ftp, Coq
   comes as a single compressed tar-file. You have probably already
   decompressed it if you are reading this document.


QUICK INSTALLATION PROCEDURE.
=============================

1. ./configure
2. make world
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 version 3.00 (or later)
   installed on your computer and that "ocamlmktop" and "ocamlc.opt" (or
   its bytecode version "ocamlc") lie in a directory which is present
   in your $PATH enviroment variable. 

   To get Coq in native-code, (it runs 4 to 10 times faster than
   bytecode, but it takes more time to compile, uses more space),
   you will also need the "ocamlopt.opt" (or its bytecode version
   "ocamlopt") 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  enviroment variable path.
   (You need Camlp4 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-7". 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 (about 20 Mb of disk space for the whole
   system in bytecode, and 15 Mb more for native-code compilation). Once
   installed, the binaries take about 14 Mb, and the library about 7 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.

   The "configure" script accepts the following options:

-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/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. SunOS and Solaris)

-local
        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).

-nowarnings
	Disable the Objective Caml compiler warnings. This option has no
	effect on the result of the compilation.

5- Still in the root directory, do

	make world

   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 (about 30 minutes for both complilations
   on a Pentium Pro 150), 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 "coq" "Major mode for editing Coq vernacular." t)

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

	make cleanall


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 :

	./configure -local <other options>

   Then compile the sources as described in step 5 above. The resulting
   binaires will reside in the subdirectory bin/<arch> where <arch> stands
   for your architecture (usually the result of the Unix command "arch").
   Once the compilation is done, you can clean some directories with
   "make clean-src" to save some disk space, the system still being usable.

   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.


UN-INSTALLATION.
================

  Maybe one day you want to move the binaries, libaries and man pages
of Coq to another place, remove them to install a newer version, or simply
remove completely Coq from your system.

  The installation procedure (during the "make install" invocation)
produces a file COQFILES which lists all files
copied during the installation. This file is created in the Coq Library
directory, which can be easily known by typing "coqtop -where"

  To remove the binaries and the library files on a Unix system, you
just have to type :

	coqtop -uninstall

Of course, you may need to be root to do that.

NOTA BENE : In order not to delete others files than the coq system files, 
	`coqtop -uninstall' deletes only files, not directories. Maybe after
	the un-installation, they are some empty directories. You can delete
	them (especially /usr/local/lib/coq) by hand after having verified
	that they are empty.

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

   There are two Coq commands:
	
	coqtop		The Coq toplevel
	coqc		The Coq compiler

   Add option "-opt" to get Coq running natively (but then you cannot load
   your own tactics dynamically -- see also option "-full")

    * `coqtop' launches Coq in the interactive mode. The default state
      (see the "-inputstate" option) is `tactics.coq', which contains some 
      basic logical definitions, the associated parsing and printing rules,
      and the following tactic modules: Tauto, ProPre, Program, Prolog and Inv.
      This top-level is built on a Objective Caml top-level. From the `coqtop'
      top-level, one can go to the Objective Caml top-level with the command:
	
		Drop. 

      One goes back to Coq through the Objective Caml commands:

                #use "include.ml";;
		go();;

    * `coqc' allows compilation of Coq files directly from the command line.
      To compile a file foo.v, do:

		coqc foo

      It will produce a file foo.vo, that you can now load through the Coq 
      command "Require". 

   For both coqtop and coqc the option -opt launches the native-code version,
   and the option -full a native-code version with all the tactics (that is 
   the tactics Linear, Extraction and Natural added to the standard tactics). 

   The `make world' and `make world-opt' commands create three distinct
   possible input states which can be used by `coqtop':

    * tactics, which is the default state described above.

    * state,  which is similar to `tactics' regarding the pre-loaded Coq
      definitions, but does not load any tactic file.

    * barestate, which gives you Coq without any pre-loaded definition. It is
      essentially used for compiling theories/INIT/ and thus building the 
      other state files.

   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) 
   and in the corresponding manual pages.


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. T fix that, try to replace
   mkdirhier with mkdir -p

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 binaires (of course).

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


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

   If you move the binaries or the library, Coq will be "lost". Usually,
   running "coqtop" will then return an error message of the kind:

	Error during initialization :
	Error: Can't find file tactics.coq on loadpath

   If you really have (or want) to move the binaries or the library, then
   you have to tell 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>