Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Verilog Other
branch: master
Failed to load latest commit information.
algebra Move broken and incomplete stuff to the broken directory.
broken Make compile with 8.4 beta.
classes Replaced meet/join by their unicode notation ⊔ / ⊓
complex Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
coq_reals Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
doc Build PDF from documentation
dump Plot pgm s works again
examples Update examples.
fta Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
ftc Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
logic Make compile with recent version of math-classes.
math-classes @ 9b9625e Make compile with 8.4 beta.
metric2 Make compile with 8.4 beta.
metrics Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
model Make compile with 8.4 beta.
old Started replacing of the rational tactic by ring.
order CoRN no longer depends on Ssreflect.
raster CoRN no longer depends on Ssreflect.
reals Make compile with 8.4 beta.
site_scons/site_tools Merge math-classes, and make joint compilation work.
stdlib_omissions Merge branch 'master' of /home/robbert/formath/math-classes
tactics Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
tools Merge branch 'master' of /home/robbert/formath/math-classes
transc Make compile with 8.4 beta.
util Make compile with 8.4 beta.
.gitignore changing .gitignore, so that we can commit the plotting function
.gitmodules Make compile with 8.4 beta.
LICENSE Merge with Nijmegen:
README Update README
SConstruct Removed old folder, modified build paths
description r786: Mise � jour des fichiers description (principalement des mots c…

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

Something went wrong with that request. Please try again.