Source Mage code commit list

[Florian Franzmann <scm AT sourcemage.org>]

GIT changes to master grimoire by Florian Franzmann 
<siflfran AT hawo.stw.uni-erlangen.de>:

 ChangeLog            |    2 ++
 devel/camlp5/BUILD   |    4 ++++
 devel/camlp5/DEPENDS |    1 +
 devel/camlp5/DETAILS |   13 +++++++++++++
 devel/camlp5/HISTORY |    4 ++++
 devel/coq/BUILD      |    8 ++++++++
 devel/coq/DEPENDS    |    6 ++++++
 devel/coq/DETAILS    |   20 ++++++++++++++++++++
 devel/coq/HISTORY    |    3 +++
 devel/coq/PRE_BUILD  |    3 +++
 10 files changed, 64 insertions(+)

New commits:
commit 81e9ff38539b39f3717d0cf983f74a3de0fd977c
Author: Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
Commit: Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>

    devel/coq: new spell, a formal proof management system

commit dd0d57f780d674f2a333aa6f5efae822359edfe4
Author: Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
Commit: Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>

    devel/camlp5: fixed libdir

commit f2e768c07cdd4ce05f09ef0f161d3f66044dd5ce
Author: Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
Commit: Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>

    devel/camlp5: new spell, a preprocessor-pretty-printer for ocaml

diff --git a/ChangeLog b/ChangeLog
index d3b4014..6715fe8 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,6 +1,8 @@
 2012-03-02 Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
        * devel/ocamlgraph: new spell, a graph library for ocaml
        * devel/alt-ergo: new spell, a theorem prover
+       * devel/camlp5: new spell, a preprocessor-pretty-printer for ocaml
+       * devel/coq: new spell, a formal proof management system
 
 2012-03-01 Ladislav Hagara <hgr AT vabo.cz>
        * libs/libftdi: new spell, library to talk to FTDI chips
diff --git a/devel/camlp5/BUILD b/devel/camlp5/BUILD
new file mode 100755
index 0000000..01abadf
--- /dev/null
+++ b/devel/camlp5/BUILD
@@ -0,0 +1,4 @@
+./configure --mandir ${INSTALL_ROOT}/usr/share/man \
+            --prefix ${INSTALL_ROOT}/usr \
+            ${OPTS} &&
+default_build_make
diff --git a/devel/camlp5/DEPENDS b/devel/camlp5/DEPENDS
new file mode 100755
index 0000000..1a31e9f
--- /dev/null
+++ b/devel/camlp5/DEPENDS
@@ -0,0 +1 @@
+depends ocaml 
diff --git a/devel/camlp5/DETAILS b/devel/camlp5/DETAILS
new file mode 100755
index 0000000..5ec3a73
--- /dev/null
+++ b/devel/camlp5/DETAILS
@@ -0,0 +1,13 @@
+           SPELL=camlp5
+         VERSION=6.04
+          SOURCE="${SPELL}-${VERSION}.tgz"
+   SOURCE_URL[0]=http://pauillac.inria.fr/~ddr/${SPELL}/distrib/src/${SOURCE}
+     
SOURCE_HASH=sha512:b1c6f5bc7ee662837b533bada68ec85f646ff372c7b8e68a2cf8503d65afd1b7710c1bc4279f85e29cb3a36fcfdef38cb261c3fe8da7037c2b5881b809a072b0
+SOURCE_DIRECTORY="${BUILD_DIRECTORY}/${SPELL}-${VERSION}"
+        WEB_SITE="http://pauillac.inria.fr/~ddr/camlp5";
+      LICENSE[0]=BSD
+         ENTERED=20120302
+           SHORT="a preprocessor-pretty-printer of OCaml"
+cat << EOF
+Camlp5 is a preprocessor-pretty-printer of ocaml.
+EOF
diff --git a/devel/camlp5/HISTORY b/devel/camlp5/HISTORY
new file mode 100644
index 0000000..f10411d
--- /dev/null
+++ b/devel/camlp5/HISTORY
@@ -0,0 +1,4 @@
+2012-03-02 Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
+       * BUILD, DEPENDS, DETAILS: spell created
+       * BUILD: fixed libdir
+
diff --git a/devel/coq/BUILD b/devel/coq/BUILD
new file mode 100755
index 0000000..14de3bf
--- /dev/null
+++ b/devel/coq/BUILD
@@ -0,0 +1,8 @@
+./configure -prefix ${INSTALL_ROOT}/usr \
+            -mandir ${INSTALL_ROOT}/usr/share/man \
+            -coqrunbyteflags "-dllib -lcoqrun" \
+            -libdir /usr/lib/coq \
+            ${OPTS} &&
+make_single         &&
+CAML_LD_LIBRARY_PATH=$(pwd)/kernel/byterun default_build_make  &&
+make_normal
diff --git a/devel/coq/DEPENDS b/devel/coq/DEPENDS
new file mode 100755
index 0000000..bd27fc7
--- /dev/null
+++ b/devel/coq/DEPENDS
@@ -0,0 +1,6 @@
+depends ocaml  &&
+depends camlp5 &&
+optional_depends lablgtk2 \
+                 "" \
+                 "" \
+                 "to build the IDE" 
diff --git a/devel/coq/DETAILS b/devel/coq/DETAILS
new file mode 100755
index 0000000..931ecf5
--- /dev/null
+++ b/devel/coq/DETAILS
@@ -0,0 +1,20 @@
+           SPELL=coq
+         VERSION=8.3pl3
+          SOURCE="${SPELL}-${VERSION}.tar.gz"
+   SOURCE_URL[0]=http://${SPELL}.inria.fr/distrib/V${VERSION}/files/${SOURCE}
+     
SOURCE_HASH=sha512:c80d9dd13fdeba632e8db3e49fb210546ddfc665b7a7dedbdaad1a1e2533e2e526871d8995837c4806f322eb7c4b86a7ac0762167bcec54ac90a06b3eb246b50
+SOURCE_DIRECTORY="${BUILD_DIRECTORY}/${SPELL}-${VERSION}"
+        WEB_SITE="http://coq.inria.fr";
+      LICENSE[0]=GPL
+         ENTERED=20120302
+           SHORT="a formal proof management system"
+cat << EOF
+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. 
Typical
+applications include the formalization of programming languages semantics 
(e.g.
+the CompCert compiler certification project or Java Card EAL7 certification
+in industrial context), the formalization of mathematics (e.g. the full
+formalization of the 4 color theorem or constructive mathematics at Nijmegen)
+and teaching.
+EOF
diff --git a/devel/coq/HISTORY b/devel/coq/HISTORY
new file mode 100644
index 0000000..c5380fe
--- /dev/null
+++ b/devel/coq/HISTORY
@@ -0,0 +1,3 @@
+2012-03-02 Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
+       * BUILD, DEPENDS, DETAILS, PRE_BUILD: spell created
+
diff --git a/devel/coq/PRE_BUILD b/devel/coq/PRE_BUILD
new file mode 100755
index 0000000..61835c9
--- /dev/null
+++ b/devel/coq/PRE_BUILD
@@ -0,0 +1,3 @@
+default_pre_build      &&
+cd ${SOURCE_DIRECTORY} &&
+sed -i "s/\\\\\"\\\$LABLGTKLIB\\\\\"/\\\$LABLGTKLIB/" configure