Skip to Content.
Sympa Menu

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

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 (81e9ff38539b39f3717d0cf983f74a3de0fd977c)
  • Date: Fri, 2 Mar 2012 09:31:06 -0600

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



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

Archive powered by MHonArc 2.6.24.

Top of Page