OKlibrary  0.2.1.6
Coq.hpp File Reference

Documentation on how to build Coq. More...

Go to the source code of this file.


Detailed Description

Documentation on how to build Coq.

Installing Coq

On the purpose of Coq

Proof assistant for upper bound proofs (and extraction of related programs).

What the installation yields

  • The coq interpreter
    1. the coqtop program: The interactive console.
  • Documentation

Current state of installation

How to install

  • Only local installation currently.
  • The programming language Ocaml needs to be installed; see the installation page Ocaml installation page.
  • The default is to use the local (OKlib) installation of Ocaml.
  • For Coq version 8.1 the latest version of Ocaml which can be used is 3.09.3 (the successor version 3.10.0 has removed the deprecated usage of "pa_ifdef.cmo" used by Coq).

Make targets

coq Build the recommended version of coq.
coq-x.y.z Build the version x.y.z of coq (for example coq-8.1).

Definition in file Coq.hpp.