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

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

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

 - Coq version revision 14023 from the trunk branch
   
   One might also perform the following optimizations:
   * Revert commit 13997 to speed up instance resolution (dependent subgoals 
     are put first since 13997. This sometimes reduces the performance 
     badly). This commit can be reverted using the following command:

       svn diff -r 13997:13996 | patch -p0
       
   * 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.
   
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

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