diff options
| author | Nick Smallbone <nick@smallbone.se> | 2020-01-18 07:49:05 +0700 |
|---|---|---|
| committer | Willy Sudiarto Raharjo <willysr@slackbuilds.org> | 2020-01-18 07:49:05 +0700 |
| commit | 25d036b157ee70a44577dcb95ba365f5d1501491 (patch) | |
| tree | 76ada3e96a291bed0e9a5ded29961fbe543c07f0 /academic/coq/README | |
| parent | a7ac25a4b1424457802304a26696d29d7b6439e9 (diff) | |
| download | slackbuilds-25d036b157ee70a44577dcb95ba365f5d1501491.tar.gz | |
academic/coq: Updated for version 8.9.0.
Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
Diffstat (limited to 'academic/coq/README')
| -rw-r--r-- | academic/coq/README | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/academic/coq/README b/academic/coq/README index 81ec48f0d6..e21de9a5fa 100644 --- a/academic/coq/README +++ b/academic/coq/README @@ -1,14 +1,7 @@ -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. +coq is a formal proof management system. It provides a formal language +to write mathematical definitions, executable algorithms and theorems +together with an environment for semi-interactive development of +machine-checked proofs. -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. - -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. +To build CoqIDE, add COQIDE=yes, e.g.: COQIDE=yes ./coq.SlackBuild. +You will need the lablgtk package built with gtksourceview support. |