GitHub - wangpengmit/corn: Coq Repository at Nijmegen

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 1,410 Commits
algebra		algebra
broken		broken
classes		classes
complex		complex
coq_reals		coq_reals
doc		doc
dump		dump
examples		examples
fta		fta
ftc		ftc
logic		logic
metric2		metric2
metrics		metrics
model		model
ode		ode
old		old
order		order
raster		raster
reals		reals
site_scons/site_tools		site_scons/site_tools
stdlib_omissions		stdlib_omissions
tactics		tactics
tools		tools
transc		transc
util		util
.gitignore		.gitignore
LICENSE		LICENSE
Make.in		Make.in
README		README
SConstruct		SConstruct
configure.sh		configure.sh
description		description

Repository files navigation

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

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

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

 - Coq 8.4pl4

 - SCons 1.2 or make

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. 

MathClasses can be installed using OPAM.
http://coq-blog.clarus.me/use-opam-for-coq.html

Or directly using from git:
https://github.com/math-classes/math-classes

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/


Make is still supported.


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

To build CoqDoc documentation, say "scons coqdoc".