C-CoRN, the Coq Constructive Repository at Nijmegen
---------------------------------------------------

This file contains some basic information about C-CoRN.

PREREQUISITES
-------------

C-CoRN (notice the capitals) is designed to run with Coq version 8.0.
A (no longer updated) version compatible with version 7.4 is also
available.

Before installing C-CoRN, please check that you have:
 - Coq version 8.0 (a compiled source tree, not only a binary package)
 - the OCaml you used to compile Coq
 - Coqdoc (http://www.lri.fr/~filliatr/coqdoc/) version striclty higher
   than 1.05 (if you want to generate the documentation)
 - at least 128MiB RAM memory available (and preferably more, especially if
   you plan to use the formalization of Real Analysis).

In order for C-CoRN to work, you need to set some environment variables.
We advise you to do this inside a .bash_profile or similar.
 - COQTOP should be set to the location of the Coq sources (e.g.
   /usr/local/src/coq-8.0/)
 - COQBIN should be set to the directory where the Coq binaries can
   be found, if different from ${COQTOP}/bin/.

FILES
-----

Any distribution of C-CoRN should include the following files at root
level:
 - Makefile
 - README
 - tree.ps.gz
and the directories
 - doc
 - tactics
 - tools

According to which version you downloaded you will also get some or all
of the following directories:
 - algebra
 - complex
 - fta
 - ftc
 - metrics
 - model
 - reals
 - transc

If you obtained C-CoRN via CVS, you will also have a directory named devel/.

Important note: if you plan to regularly update C-CoRN, you should
keep any files you work on under devel/ or out of the CoRN tree
altogether.  This will ensure that subsequent updates will not
overwrite your developments.

COMPILING
---------

C-CoRN now comes with a general purpose Makefile.  This allows you to
uniformly:
 - (re)compile C-CoRN;
 - automatically generate postscript or html documentation from C-CoRN;
 - refresh the list of dependencies;
 - see which commands are actually used for these tasks.

The default behaviour of make (with no target specified) is to recompile
all files that have been changed since the last compilation, as well as
everything that depends on these files.  The following targets are also
allowed:
 dep          -> recalculates the dependencies of modified files
                 Note that this is called automatically before
                 compilation, you normally don't need to call it
                 explicitly.
 clean        -> removes all .vo, .cmx, .cmi, .cmo, .o, .vi, .g, emacs
                 backup (*~) files, the CoRN toplevel and compiler and
                 the globals file. Also does depclean.
 depclean     -> forget all computed dependencies. Useful to force a
                 full recomputation of the dependencies.
 distclean    -> removes things that should not be distributed from a
                 CVS checkout.
 doc          -> produces both postscript and html documentation
 doc-clean    -> removes all documentation files
 doc-html     -> produces only html documentation
 doc-ps       -> produces only postscript documentation
 showcommands -> prints the actual command line that will be used to
                 compile files
 human        -> setup CoRN for human convenience (see `HUMAN CONVENIENCE' section)
 ide          -> setup CoRN for human convenience using coqide

Besides these, flags can also be given to make.  Currently, the following
are recognized.
 devel="space separated directories list"
              -> compile the files in these directory trees, too. Between a
                 command with some value of devel (e.g. unset) and a
                 command with some other value (e.g. set to anything but
                 empty), you _must_ force a complete recompilation of the
                 dependencies (make depclean). For example, to compile all
                 files in the devel/ sub-directory and all its
                 subdirectories (like devel=yes did before) use
                 devel=./devel . To compile files in devel/lcf and
                 devel/foo, use devel="./devel/lcf ./devel/foo" . Yes, this
                 means that directories containing a space in their name
                 won't work.
 OPT=[option] -> adds [option] to the Coq command line
 OCAMLC=file
 OCAMLOPT=file
              -> Choose an ocamlc and ocamlopt to use
 COQDOC=file  -> Choose a coqdoc to use

HUMAN CONVENIENCE
-----------------

CoRN now has a few facilities for the convenience of the human beings
using it. Enable with "make human", or "make ide" for coqide support
(this needs a coqide-enabled Coq).

This will create Makefiles in every directory scanned for .v files
(but will not overwrite the Makefile if any is present) so that all
make commands work from anywhere in the CoRN hierarchy.

It also populates the "bin" directory with CoRNc, CoRNtop and (with
coqide support) CoRNide. These are CoRN versions of coqc, coqtop and
coqide, respectively. We suggest you add the "bin" directory of CoRN
to your PATH.

DEPENDENCIES
------------

The distribution includes a (gzip'ed) postscript file tree.ps.gz
with the dependency tree of all the files in the standard, full,
version of C-CoRN.

OTHERS
------

More information can be found at the C-CoRN page,
http://www.cs.kun.nl/fnds/ccorn.
For any questions, comments, bug reports or other feel free to e-mail
lcf@cs.kun.nl.

$Id$
                 
 LocalWords:  Nijmegen CoRN Coq CVS