README

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

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

This version of C-CoRN is known to compile with:

 - Coq 8.4 beta

   One might also perform the following optimizations:
   * Change size = 6 to size = 12 in theories/Numbers/Natural/BigN/NMake_gen.ml
     to increase performance for big numbers.

 - SCons 1.2

 - In order to build the dependency graph you need a Haskell compiler and the
   Graphviz library for Haskell. The latter can be obtained using the Cabal
   package manager.

GIT CHECKOUT & SUBMODULES
-------------------------

C-CoRN depends on Math Classes, which is a library of abstract interfaces for 
mathematical structures that is heavily based on Coq's new type classes. 
Math Classes is contained in the C-CoRN git repository as a submodule. You can 
obtain math-classes automatically by giving the --recursive option when you 
clone the git repository:

  git clone --recursive https://github.com/c-corn/corn.git

If you have already cloned the CoRN repository without --recursive, you can
still get the submodules with

  git submodule update --init --recursive


BUILDING C-CoRN
---------------

C-CoRN uses SCons for its build infrastructure. SCons is a modern
Python-based Make-replacement.

To build C-CoRN with SCons say "scons" to build the whole library, or 
"scons some/module.vo" to just build some/module.vo (and its dependencies).

In addition to common Make options like -j N and -k, SCons
supports some useful options of its own, such as --debug=time, which
displays the time spent executing individual build commands.

scons -c replaces Make clean

For more information, see the SCons documentation at

  http://www.scons.org/


BUILDING DOCUMENTATION
----------------------

To build CoqDoc documentation, say "scons coqdoc".

A dependency graph in DOT format can be created with "scons deps.dot".

PLOTS
-----

If you want high resolution plots in examples/Circle.v, follow the instructions 
in dump/INSTALL