---
fullname: C-CoRN
shortname: corn
organization: coq-community
community: true
action: true

synopsis: The Coq Constructive Repository at Nijmegen.

description: |
  CoRN includes the following parts:

  - Algebraic Hierarchy

    An axiomatic formalization of the most common algebraic
    structures, including setoids, monoids, groups, rings,
    fields, ordered fields, rings of polynomials, real and
    complex numbers

  - Model of the Real Numbers

    Construction of a concrete real number structure
    satisfying the previously defined axioms

  - Fundamental Theorem of Algebra

    A proof that every non-constant polynomial on the complex
    plane has at least one root

  - Real Calculus

    A collection of elementary results on real analysis,
    including continuity, differentiability, integration,
    Taylor's theorem and the Fundamental Theorem of Calculus

  - Exact Real Computation

    Fast verified computation inside Coq. This includes: real numbers, functions,
    integrals, graphs of functions, differential equations.

authors:
- name: Evgeny Makarov
- name: Robbert Krebbers
- name: Eelis van der Weegen
- name: Bas Spitters
- name: Jelle Herold
- name: Russell O'Connor
- name: Cezary Kaliszyk
- name: Dan Synek
- name: Luís Cruz-Filipe
- name: Milad Niqui
- name: Iris Loeb
- name: Herman Geuvers
- name: Randy Pollack
- name: Freek Wiedijk
- name: Jan Zwanenburg
- name: Dimitri Hendriks
- name: Henk Barendregt
- name: Mariusz Giero
- name: Rik van Ginneken
- name: Dimitri Hendriks
- name: Sébastien Hinderer
- name: Bart Kirkels
- name: Pierre Letouzey
- name: Lionel Mamane
- name: Nickolay Shmyrev
- name: Vincent Semeria

maintainers:
- name: Bas Spitters
  nickname: spitters
- name: Vincent Semeria
  nickname: vincentse

opam-file-maintainer: b.a.w.spitters@gmail.com

license:
  fullname: GNU General Public License v2
  identifier: GPL-2.0

supported_coq_versions:
  text: Coq 8.7 or greater
  opam: '{(>= "8.7" & < "8.13~") | (= "dev")}'

tested_coq_opam_versions:
- version: dev
- version: "8.12"
- version: "8.11"
- version: "8.10"
- version: "8.9"
- version: "8.8"
- version: "8.7"

dependencies:
- opam:
    name: coq-math-classes
    version: '{(>= "8.8.1") | (= "dev")}'
  nix: math-classes
  description: |
    [Math-Classes](https://github.com/coq-community/math-classes) 8.8.1 or
    greater, which is a library of abstract interfaces for mathematical
    structures that is heavily based on Coq's type classes.
- opam:
    name: coq-bignums
  nix: bignums
  description: "[Bignums](https://github/com/coq/bignums)"

namespace: CoRN

keywords:
- name: constructive mathematics
- name: algebra
- name: real calculus
- name: real numbers
- name: Fundamental Theorem of Algebra

categories:
- name: Mathematics/Algebra
- name: Mathematics/Real Calculus and Topology
- name: Mathematics/Exact Real computation

publications:
- pub_title: See this page for the list of publications
  pub_url: http://corn.cs.ru.nl/pub.html

build: |
  ## Building and installation instructions

  The easiest way to install the latest released version of C-CoRN
  is via [OPAM](https://opam.ocaml.org/doc/Install.html):

  ```shell
  opam repo add coq-released https://coq.inria.fr/opam/released
  opam install coq-corn
  ```

  To instead build and install manually, you have to start with
  the `bignums` dependency:

  ``` shell
  git clone https://github.com/coq/bignums
  cd bignums
  make   # or make -j <number-of-cores-on-your-machine>
  make install
  ```

  The last `make install` is necessary, it copies `bignums` to
  a common folder, which is usually `coq/user-contrib`. Afterwards
  the similar commands for `math-classes` will find `bignums` there.
  Finally build `corn` itself:

  ``` shell
  git clone https://github.com/coq-community/corn
  cd corn
  ./configure.sh
  make   # or make -j <number-of-cores-on-your-machine>
  make install
  ```

  ### Building C-CoRN with SCons

  C-CoRN supports building with [SCons](http://www.scons.org/). SCons is a modern
  Python-based Make-replacement.

  To build C-CoRN with SCons run `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](http://www.scons.org/).

  ### Building documentation

  To build CoqDoc documentation, say `scons coqdoc`.
---