Downloads

Tarballs

You can download the total formalization or just specific parts of it.

• Full System
• Core
• Algebraic Hierarchy
• Model of the Real Numbers
• Fundamental Theorem of Algebra
• Real Calculus
• Metric Spaces
• Effective Real Numbers

To download the full system, just click on the first link. The partial distributions should be self-contained, e.g. you do not need to download Core in order to use Algebraic Hierarchy. After you untar the files (which will create a CoRN/ directory at the place of installation) you will find a.o. a README file which contains more detailed instructions on how to proceed. It is (unfortunately) quite likely that all will not go well, especially if you only download parts of C-CoRN; if this happens, please contact me.

Bleeding Edge and Contributors

You can also use Git to get the latest development of CoRN and its recent development history by cloning our repository:

git clone http://www.fnds.cs.ru.nl/git/CoRN.git

This is particularly recommended if

• You want to contribute back improvements to CoRN. (In this case, you will probably want to fork CoRN into your own repository and ask us to merge from you when your contribution is mature.)
• You are in a tremendous hurry and don't want to wait for the above tarballs to be regenerated.

• coq-8.1
  This version should be compatible with the Coq 8.1 (the latest stable release of Coq).
• coq-8.2
  This version should be compatible with the latest coq-8.2 development branch, and will become compatible with the next release of Coq.
• coq-trunk
  This version should be compatible with the latest svn version of Coq.

• coq-8.0
  This is the last version of CoRN that was compatible coq 8.0.