SlackBuilds Repository

14.2 > Academic > coq (8.5pl1)

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.5pl1.tar.gz (1faa8a237c3e81905dc938b6b727b807)

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

(the SlackBuild does not include the source)

Individual Files:

Validated for Slackware 14.2

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