mirror of
https://github.com/Ponce/slackbuilds
synced 2024-11-18 22:06:04 +01:00
143991a46e
This field used to make sense in our pre-git days, but the Signed-Off-By: line serves the same purpose (and even more) now, so APPROVED has been rejected. ;-) Signed-off-by: Robby Workman <rworkman@slackbuilds.org> |
||
|---|---|---|
| .. | ||
| coq.info | ||
| coq.SlackBuild | ||
| gpl.txt.gz | ||
| README | ||
| slack-desc | ||
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.