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.2.

Before installing C-CoRN, please check that you have:
 - Coq version 8.2
 - at least 128MiB RAM memory available (and preferably more) 
 - GNU make version 3.80 or later
 - a POSIX-compliant operating system. This means Unix, a clone
   thereof or a good emulation layer on top of another OS. In
   particular, *hard* links must be supported by the file system.
 - the GNU Bourne Again SHell (we use some bashisms)
 - At least one of:
   * The "realpath" utility in your PATH (Debian package realpath).
   * A C compiler.
 - camlp4
 - Compile Ssreflect in the root directory of its sources:

   <your path to coq sources directory>/bin/coq_makefile -f Make > Makefile
   Add a custom target to the Makefile:
   ----
   bin/ssrcoqide: src/ssreflect.cmx
        $(COQBIN)coqmktop -ide -opt -o "$@" src/ssreflect.cmx
   ----
   COQBIN=<your path to coq sources directory>/bin/ make

   If you have ocaml version > 3.11 then  you can directly use standard coq tools if you use
   ssreflect as a plugin Declare ML Module "ssreflect".
   at the beginning of ssreflect.v, and installing ssreflect.cmxs next to ssreflect.vo
   Or put the Declare line in either a .coqrc file, or in a Coq compile option, rather than modifying ssreflect.v.

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 Coq installation prefix (e.g. /usr/ or
   /usr/local/) or the location of a compiled Coq source tree (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/.
 - SSRDIR should be set to the directory where Ssreflect can
   be found.

FILES
-----

Any distribution of C-CoRN should include the following files at root
level:
 - Makefile
 - Makefile.{realpath,common}
 - README
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
 - coq_reals
 - examples
 - fta
 - ftc
 - logic
 - metric2
 - metrics
 - model
 - order
 - raster
 - reals
 - transc

COMPILING
---------

C-CoRN 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
                 VCS checkout.
 doc          -> produces both postscript and html documentation and
                 and SVG dependency graph.
 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 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
                 (Obsolete, as CoRN does not use OCaml anymore.)
 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".

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
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 can build a dependency graph.  run

 make tree.pdf

or 

 make tree.svg

to build it.
This requires graphviz and a haskell interpreter.

OTHERS
------

More information can be found at the C-CoRN page,
http://c-corn.cs.ru.nl/
For any questions, comments, bug reports or other feel free to contact
us; contact information is in the doc/www/info.html file.

 LocalWords:  Nijmegen CoRN Coq VCS