Skip to Content.
Sympa Menu

sm-commit - [SM-Commit] GIT changes to master grimoire by Florian Franzmann (f010a870d8d3ed1038d14a1585fe7d4b44d1d66a)

sm-commit AT lists.ibiblio.org

Subject: Source Mage code commit list

List archive

Chronological Thread  
  • From: Florian Franzmann <scm AT sourcemage.org>
  • To: sm-commit AT lists.ibiblio.org
  • Subject: [SM-Commit] GIT changes to master grimoire by Florian Franzmann (f010a870d8d3ed1038d14a1585fe7d4b44d1d66a)
  • Date: Fri, 2 Mar 2012 07:57:51 -0600

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
+



  • [SM-Commit] GIT changes to master grimoire by Florian Franzmann (f010a870d8d3ed1038d14a1585fe7d4b44d1d66a), Florian Franzmann, 03/02/2012

Archive powered by MHonArc 2.6.24.

Top of Page