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                |    4 ++++
 devel/alt-ergo/DEPENDS   |    2 ++
 devel/alt-ergo/DETAILS   |   17 +++++++++++++++++
 devel/alt-ergo/HISTORY   |    3 +++
 devel/ocamlgraph/DEPENDS |    1 +
 devel/ocamlgraph/DETAILS |   35 +++++++++++++++++++++++++++++++++++
 devel/ocamlgraph/HISTORY |    3 +++
 7 files changed, 65 insertions(+)

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

    devel/alt-ergo: new spell, a theorem prover

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

    devel/ocamlgraph: new spell, a graph library for ocaml

diff --git a/ChangeLog b/ChangeLog
index 4741abb..d3b4014 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,7 @@
+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
+
 2012-03-01 Ladislav Hagara <hgr AT vabo.cz>
        * libs/libftdi: new spell, library to talk to FTDI chips
        * devel/openocd: new spell, Open On-Chip Debugging
diff --git a/devel/alt-ergo/DEPENDS b/devel/alt-ergo/DEPENDS
new file mode 100755
index 0000000..4e9dffe
--- /dev/null
+++ b/devel/alt-ergo/DEPENDS
@@ -0,0 +1,2 @@
+depends ocaml &&
+depends ocamlgraph
diff --git a/devel/alt-ergo/DETAILS b/devel/alt-ergo/DETAILS
new file mode 100755
index 0000000..5a089ba
--- /dev/null
+++ b/devel/alt-ergo/DETAILS
@@ -0,0 +1,17 @@
+           SPELL=alt-ergo
+         VERSION=0.94
+          SOURCE="${SPELL}-${VERSION}.tar.gz"
+   SOURCE_URL[0]=http://${SPELL}.lri.fr/http/${SOURCE}
+     
SOURCE_HASH=sha512:7bd5f725f9861b764dcc1a71cf89e8abe9398a0138d1f137094a9d1b089938ef3a3933bb5d55677f50b197a443c66bbbbf0a57e07da32e592f741a7aab527bdf
+SOURCE_DIRECTORY="${BUILD_DIRECTORY}/${SPELL}-${VERSION}"
+        WEB_SITE="http://alt-ergo.lri.fr";
+      LICENSE[0]=CeCILL-C
+         ENTERED=20120302
+           SHORT="an automatic theorem prover"
+cat << EOF
+Alt-Ergo is an automatic theorem prover dedicated to program verification.
+Alt-Ergo is based on CC(X) a congruence closure algorithm parameterized by
+an equational theory X. Currently, CC(X) can be instantiated by the empty
+equational theory and by the linear arithmetics. Alt-Ergo contains also a
+home made SAT-solver and an instantiation mechanism.
+EOF
diff --git a/devel/alt-ergo/HISTORY b/devel/alt-ergo/HISTORY
new file mode 100644
index 0000000..5404b63
--- /dev/null
+++ b/devel/alt-ergo/HISTORY
@@ -0,0 +1,3 @@
+2012-03-02 Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
+       * DEPENDS, DETAILS: spell created
+
diff --git a/devel/ocamlgraph/DEPENDS b/devel/ocamlgraph/DEPENDS
new file mode 100755
index 0000000..1a31e9f
--- /dev/null
+++ b/devel/ocamlgraph/DEPENDS
@@ -0,0 +1 @@
+depends ocaml 
diff --git a/devel/ocamlgraph/DETAILS b/devel/ocamlgraph/DETAILS
new file mode 100755
index 0000000..bc0c7a3
--- /dev/null
+++ b/devel/ocamlgraph/DETAILS
@@ -0,0 +1,35 @@
+           SPELL=ocamlgraph
+         VERSION=1.8.1
+          SOURCE="${SPELL}-${VERSION}.tar.gz"
+   SOURCE_URL[0]=http://${SPELL}.lri.fr/download/${SOURCE}
+     
SOURCE_HASH=sha512:8e2aab51afd096979e3e062a86eaa1445c4cd84baf7f45bff01897ef03a9d154eacf51f494212c1a5859f83f8521584679069f9bf604f2eccb4714ebf71ab6a8
+SOURCE_DIRECTORY="${BUILD_DIRECTORY}/${SPELL}-${VERSION}"
+        WEB_SITE="http://ocamlgraph.lri.fr";
+      LICENSE[0]=GPL
+         ENTERED=20120302
+           SHORT="a graph library for Objective Caml"
+cat << EOF
+ocamlgraph is a graph library for Objective Caml. Its contribution is
+three-fold:
+
+* It provides an easy-to-use graph data structure together with several
+  operations and algorithms over graphs. It is a reasonably efficient
+  imperative data structure for directed graphs with vertices and edges
+  labeled with integers.
+
+* Ocamlgraph provides several other graph implementations for those not
+  satisfied with the one above. Some are persistent (imutable) and other
+  imperative (mutable). Some are directed and other are not. Some have labels
+  for vertices, or labels for edges, or both. Some have abstract types for
+  vertices. etc.
+
+  These implementations are written as functors: you give the types of 
vertices
+  labels, edge labels, etc. and you get the data structure as a result.
+
+* Finally, ocamlgraph provides several classic operations and algorithms over
+  graphs. They are also written as functors i.e. independently of the data
+  structure for graphs. One consequence is that you can define your own data
+  structure for graphs and yet re-use all the algorithms from this library
+  -- you only need to provide a few operations such as iterating over all
+  vertices, over the successors of a vertex, etc.
+EOF
diff --git a/devel/ocamlgraph/HISTORY b/devel/ocamlgraph/HISTORY
new file mode 100644
index 0000000..5404b63
--- /dev/null
+++ b/devel/ocamlgraph/HISTORY
@@ -0,0 +1,3 @@
+2012-03-02 Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
+       * DEPENDS, DETAILS: spell created
+