Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Tree: 6f9a857142
Fetching contributors…

Cannot retrieve contributors at this time

71 lines (44 sloc) 2.034 kB
C-CoRN, the Coq Constructive Repository at Nijmegen
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/
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.
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
If you have already cloned the CoRN repository without --recursive, you can
still get the submodules with
git submodule update --init --recursive
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
To build CoqDoc documentation, say "scons coqdoc".
A dependency graph in DOT format can be created with "scons".
If you want high resolution plots in examples/Circle.v, follow the instructions
in dump/INSTALL
Jump to Line
Something went wrong with that request. Please try again.