This script is for Slackware 13.37 and may be outdated.

SlackBuilds Repository

13.37 > 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.

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.

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 13.37

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-2018 Project. All rights reserved.
Slackware® is a registered trademark of Patrick Volkerding
Linux® is a registered trademark of Linus Torvalds
Web Design by WebSight Designs |  Managed Hosting by OnyxLight Communications