This script is for Slackware 14.1 only and may be outdated.

SlackBuilds Repository

14.1 > Academic > coq (8.3pl2)

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.

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.

This requires: camlp5

Maintained by: William Bowman
Keywords: coq,theorem prover,proof assistant,proof managment,ocaml
ChangeLog: coq


Source Downloads:
coq-8.3pl2.tar.gz (db415f6c5372f5a443699c62f5affcb4)

Download SlackBuild:
coq.tar.gz.asc (FAQ)

(the SlackBuild does not include the source)

Individual Files:

Validated for Slackware 14.1

See our HOWTO for instructions on how to use the contents of this repository.

Access to the repository is available via:
ftp git cgit http rsync

© 2006-2023 Project. All rights reserved.
Slackware® is a registered trademark of Patrick Volkerding
Linux® is a registered trademark of Linus Torvalds