[Lunar-commits] <moonbase> coq: introduction to moonbase

[Michael 'v4hn' Goerner]

commit bc73f30999319aae35fd7f01768c649a6a837386
Author: Michael 'v4hn' Goerner <v4hn at lunar-linux.org>
Date:   Mon Aug 29 14:04:10 2011 +0200

    coq: introduction to moonbase
---
 compilers/coq/BUILD   |    8 ++++++++
 compilers/coq/DEPENDS |    4 ++++
 compilers/coq/DETAILS |   15 +++++++++++++++
 3 files changed, 27 insertions(+), 0 deletions(-)

diff --git a/compilers/coq/BUILD b/compilers/coq/BUILD
new file mode 100644
index 0000000..6d95049
--- /dev/null
+++ b/compilers/coq/BUILD
@@ -0,0 +1,8 @@
+(
+
+ ./configure -prefix /usr $OPTS &&
+ make world      &&
+ prepare_install &&
+ make install
+
+) > $C_FIFO 2>&1
diff --git a/compilers/coq/DEPENDS b/compilers/coq/DEPENDS
new file mode 100644
index 0000000..19aacde
--- /dev/null
+++ b/compilers/coq/DEPENDS
@@ -0,0 +1,4 @@
+depends ocaml
+depends camlp5
+
+optional_depends lablgtk "-coqide opt" "-coqide no" "to build a GTK IDE"
diff --git a/compilers/coq/DETAILS b/compilers/coq/DETAILS
new file mode 100644
index 0000000..8ba1242
--- /dev/null
+++ b/compilers/coq/DETAILS
@@ -0,0 +1,15 @@
+          MODULE=coq
+         VERSION=8.3pl2
+          SOURCE=$MODULE-$VERSION.tar.gz
+      SOURCE_URL=http://coq.inria.fr/distrib/V${VERSION}/files/
+      SOURCE_VFY=sha1:8506761e4755739cc728aff790dd778db8217f3f
+        WEB_SITE=http://coq.inria.fr/
+         ENTERED=20110829
+         UPDATED=20110829
+           SHORT="COQ is an interactive proof assistant"
+cat << EOF
+COQ is a Proof Assistant for a Logical Framework known as the Calculus of
+Inductive Constructions. It allows the interactive construction of formal
+proofs, and also the manipulation of functional programs consistently
+with their specifications.
+EOF