mirror of
https://github.com/Ponce/slackbuilds
synced 2024-11-22 19:44:21 +01:00
20 lines
935 B
Text
20 lines
935 B
Text
|
Coq implements a program specification and mathematical higher-level
|
||
|
|
language called Gallina that is based on an expressive formal language
|
||
|
|
called the Calculus of Inductive Constructions that itself combines both
|
||
|
|
a higher-order logic and a richly-typed functional programming language.
|
||
|
|
|
||
|
|
This requires OCaml (>= 3.10.2), camlp5 (with "transitional mode", avoiding
|
||
|
|
version 5.0.0), and GNU Make (>= 3.81). If you have ocamlopt, Coq
|
||
|
|
will be compiled to native code, which runs 4-10 times faster. For best
|
||
|
|
performance, OCaml should have support for pthreads.
|
||
|
|
|
||
|
|
Note: camlp5 6.01 appears to have a bug that prevents Coq from building
|
||
|
|
correctly. This build has been tested with 6.02.3.
|
||
|
|
|
||
|
|
If you want CoqIDE, you need LablGTK2 (>= 2.10.0) with development
|
||
|
|
files, and GTK2+ (>= 2.10.0). This also REQUIRES OCaml to have support
|
||
|
|
for pthreads.
|
||
|
|
|
||
|
|
If you have emacs installed, emacs files for Coq will be installed.
|
||
|
|
Otherwise, they will be omitted.
|