13 files changed, 371 insertions, 0 deletions
diff --git a/dev-ml/getarg/Manifest b/dev-ml/getarg/Manifest
new file mode 100644
index 0000000..712561b
--- /dev/null
+++ b/dev-ml/getarg/Manifest
@@ -0,0 +1,2 @@
+DIST getarg-0.1-p1.tbz 23650 SHA256 6d0f592b82354d5204c374148e7fb700b1a21cd32e7f5f9953753e59122dc83b SHA512 b10016fc3479c0b968ff030df79f7f8fd1152460e9c6f79ebd0b347e5998c37df7b4c3795f28cfb7247c4c1414024d7e7aa09f45651c22e7c268b27cdaff71c3 WHIRLPOOL 14a01199344752da48bf78ba45ebc8634a90f54249b32bed2c6c1cf1cead39451d8433a0b9d535c68ff442e6707ee0814ecf41777c6f238ae9b60844944b4d64
+EBUILD getarg-0.1_p1.ebuild 1004 SHA256 ad54b63c6dffff46adeb33d78d641c2042952d3d284e9597b527c3fe08e4a6c1 SHA512 90563fa2952fc2053b7943c8335cddf3d67c50b74230d1198d7fd1936f1621cf794e1c1eda6e66bbd3ad8df148229903c3ba82fe46bfd95c518663aaf61449e9 WHIRLPOOL f698cb44a77756d4ac64f04dcc9b59eb2ed14ee0830eb2959fa32eb2b92dc00bc04c267f02e2ac753052865502fef9cc9d5daa6733e6698ef60b66c1d08e09b6
diff --git a/dev-ml/getarg/getarg-0.1_p1.ebuild b/dev-ml/getarg/getarg-0.1_p1.ebuild
new file mode 100644
index 0000000..8885738
--- /dev/null
+++ b/dev-ml/getarg/getarg-0.1_p1.ebuild
@@ -0,0 +1,65 @@
+# Copyright 2013 Quentin Heath
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI=4
+
+inherit eutils autotools
+
+SLOT="0"
+MY_PV="${PV/_/-}"
+TARBALL_NAME="${PN}-${MY_PV}"
+
+DESCRIPTION="OCaml command-line option parser"
+HOMEPAGE="http://gitorious.org/hippomail/getarg/"
+SRC_URI="http://www.lix.polytechnique.fr/~heath/releases/tarballs/${TARBALL_NAME}.tbz"
+
+LICENSE="GPL-3"
+KEYWORDS="~amd64 ~x86"
+IUSE="+ocamlopt debug doc"
+
+DEPEND=">=dev-lang/ocaml-3.11.0[ocamlopt?]
+>=sys-devel/autoconf-2.60"
+RDEPEND="${DEPEND}"
+
+S="${WORKDIR}/${TARBALL_NAME}"
+
+
+#pkg_setup()
+
+#src_unpack()
+
+src_prepare() {
+	eautoconf
+}
+
+src_configure() {
+	local myconf="--no-create"
+	econf $myconf \
+		$(use_enable ocamlopt nativecode) \
+		$(use_enable debug) \
+		$(use_enable doc)
+}
+
+src_compile() {
+	emake -j1
+	use doc && emake -j1 doc
+}
+
+src_test() {
+	emake -j1 test
+}
+
+src_install() {
+	emake -j1 DESTDIR="${D}" install
+}
+
+#pkg_preinst()
+
+#pkg_postinst()
+
+#pkg_prerm()
+
+#pkg_postrm()
+
+#pkg_config()
diff --git a/dev-ml/ocaml-getopt/Manifest b/dev-ml/ocaml-getopt/Manifest
new file mode 100644
index 0000000..cb54427
--- /dev/null
+++ b/dev-ml/ocaml-getopt/Manifest
@@ -0,0 +1,2 @@
+DIST getopt-20040811.tar.gz 4759 SHA256 cb53317e026867e732276feff392031831d7cbed1d4b49a764971d6bab1fff2a SHA512 0c8c9e4efc277db6b39ee12c074c31b053609a60c9af4b83aa3ac1a1b07b2c62ef7c22836fb6d0ce4e2102be52a024ae7fc411d5fdb29ba64a58290835e7ee67 WHIRLPOOL 865932133628408abc2ad7906e115f95937c59b42a3f8034a1adfbe8ffe5eb3241d8f0dfd9fd72ff6b24e7d5f7a2efa9823f96f73d44efb852a03dd0dbb5bd90
+EBUILD ocaml-getopt-20040811.ebuild 709 SHA256 3cad5fe49bda5269153694f7099687516a8683ccb89d9810df61fdf510ff3439 SHA512 4461fe03977e2f2c87c93eb5f220f3c37de757494477091291e410b6c20e8b6766eaca5600c4d2b6664b40e2d9be216cb083a2a2746ee1c19cae76b3e4f35a35 WHIRLPOOL 2d07f7a5fb342646496ca2061817477b8f2ed0937210a22b22c12a93ca67c71662768a1cc2e6a40c29fb5de4f672b40314ac282aa0a75e69c0174fad021f0eff
diff --git a/dev-ml/ocaml-getopt/ocaml-getopt-20040811.ebuild b/dev-ml/ocaml-getopt/ocaml-getopt-20040811.ebuild
new file mode 100644
index 0000000..9cd39ac
--- /dev/null
+++ b/dev-ml/ocaml-getopt/ocaml-getopt-20040811.ebuild
@@ -0,0 +1,40 @@
+# Copyright 1999-2012 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI=4
+
+inherit findlib
+
+DESCRIPTION="Ocaml command line parser (à la GNU GetOpt)"
+HOMEPAGE="http://forge.ocamlcore.org/projects/ocaml-getopt/"
+SRC_URI="http://forge.ocamlcore.org/frs/download.php/756/getopt-20040811.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~x86 ~amd64"
+IUSE="doc"
+
+DEPEND=">=dev-lang/ocaml-3.06"
+RDEPEND="${DEPEND}"
+
+S=${WORKDIR}/getopt
+RESTRICT="nomirror"
+
+
+
+src_compile()
+{
+	make all allopt || die "make failed"
+}
+
+src_install()
+{
+	findlib_src_preinst
+	make install || die
+
+	use doc && dohtml -r doc/*
+	use doc && dodoc sample.ml
+	dodoc COPYING Changes README
+}
+
diff --git a/dev-tex/mathpartir/Manifest b/dev-tex/mathpartir/Manifest
new file mode 100644
index 0000000..94c9f7d
--- /dev/null
+++ b/dev-tex/mathpartir/Manifest
@@ -0,0 +1,3 @@
+DIST mathpartir.tgz 325049 SHA256 2697072b6615ced3601e9596f45507a199565078c67eff465e21e2d3c5b91bfe SHA512 fec136cf9acc211ea2c8e90bd458a1e316db9a8a62357e7cafbe9a321ca4800136a009adba10ed9fb5275f7af6bfefc1cd8ca85b848e22c0aa540892df753970 WHIRLPOOL 4ee5a4858cb49f966f34bbd7e0cfc1af5e0d94f417fabec4e1f8d5a433e4f3cd0e1f167ecf420c7380e0c75656ba2325dd5ea1daafcbe4ed3d53cf46f7efe1f7
+EBUILD mathpartir-1.2.0-r1.ebuild 909 SHA256 9495e4bdc532845663add3825720d82b8cf9f9a5a1105ab1eb8869ba8c49b343 SHA512 d6b1894f63ffd86e7535c2ed181d51b55fd4860bcf6e82c86bdda90977f3b7f74939ac027f4805b37879b60a45eb9ce9450834645124660fb29fbe6f5c0ecf3f WHIRLPOOL a5df0b073c80b62d23c53aa47b212aa1ca396876c433e73b4dde494f768c8693f888caa4f103f2b0e6f81b65d4a6073cd1617007255a73cd4611f16d611189a3
+MISC metadata.xml 1254 SHA256 6b2bb55730c2bf38199324089eea2e4c030a184df3e42dc6345864d53a1315ac SHA512 549565fee446f857d79fa79d881b8fb0141808047131bb5de86eb5db88d3200cafbccb5082f778362da7f59451fac940c21674f90a42754819f9880ebe218ca4 WHIRLPOOL 5e2bbfa1fc16f9f77ba2c9393ea10642dbaacd071498821c612ea69ace1b9550ed5b081f8f3e48d1a202ad82e378720cfe411bb5588ea3c6f0d7a22bfdf8703d
diff --git a/dev-tex/mathpartir/mathpartir-1.2.0-r1.ebuild b/dev-tex/mathpartir/mathpartir-1.2.0-r1.ebuild
new file mode 100644
index 0000000..fd0e91e
--- /dev/null
+++ b/dev-tex/mathpartir/mathpartir-1.2.0-r1.ebuild
@@ -0,0 +1,59 @@
+# Copyright 2013 Quentin Heath
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI=4
+
+inherit eutils
+
+SLOT="0"
+
+DESCRIPTION="LaTeX macros for typesetting inference rules"
+HOMEPAGE="http://cristal.inria.fr/~remy/latex/"
+SRC_URI="http://cristal.inria.fr/~remy/latex/${PN}.tgz"
+
+LICENSE="GPL-2"
+KEYWORDS="~amd64 ~x86"
+IUSE="doc"
+
+DEPEND="doc? ( app-text/texlive[extra] dev-tex/hevea )"
+RDEPEND="${DEPEND}"
+
+S="${WORKDIR}"
+
+
+#pkg_setup()
+
+#src_unpack()
+
+#src_prepare()
+
+#src_configure()
+
+#src_compile()
+
+src_test() {
+	true
+}
+
+src_install() {
+	dodoc mathpartir.ps.gz mathpartir.pdf mathpartir.html
+	insinto /usr/share/texmf/tex/latex/${PN}
+	doins mathpartir.sty
+	insinto /usr/share/doc/texmf/latex/${PN}
+	doins mathpartir.tex mathpartir.dvi
+}
+
+#pkg_preinst()
+
+pkg_postinst() {
+	mktexlsr /usr/share/texmf
+}
+
+#pkg_prerm()
+
+pkg_postrm() {
+	mktexlsr /usr/share/texmf
+}
+
+#pkg_config()
diff --git a/dev-tex/mathpartir/metadata.xml b/dev-tex/mathpartir/metadata.xml
new file mode 100644
index 0000000..a193c4e
--- /dev/null
+++ b/dev-tex/mathpartir/metadata.xml
@@ -0,0 +1,26 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+	<herd>no-herd</herd>
+	<longdescription>
+		This package provides macros for displaying lists of formulas
+		that are typeset in mixed horizontal and vertical modes.
+		The package is two-folded.
+
+		The first part is an environment mathpar that generalizes the math
+		display mode to allow several formulas on the same line, and several
+		lines in the same display. The arrangement of the sequence of formulas
+		into lines is automatic depending on the line width and on a minimum
+		inter-formula space and line width alike words in a paragraphs (in
+		centerline mode). A typical application is displaying a set of type
+		inference rules.
+
+		The second par is a macro inferrule to typeset inference rules
+		themselves. Here again, both premises and conclusions are presented as
+		list of formulas that should be displayed in almost the same way, except
+		that the width is not fixed in advance; and the inference rule should
+		use no more width than necessary so that other inference rules are given
+		a chance to appear on the same line.
+	</longdescription>
+	<upstream>http://cristal.inria.fr/~remy/latex/</upstream>
+</pkgmetadata>
diff --git a/metadata/layout.conf b/metadata/layout.conf
new file mode 100644
index 0000000..d43e61c
--- /dev/null
+++ b/metadata/layout.conf
@@ -0,0 +1 @@
+masters = gentoo
diff --git a/profiles/repo_name b/profiles/repo_name
new file mode 100644
index 0000000..2182eeb
--- /dev/null
+++ b/profiles/repo_name
@@ -0,0 +1 @@
+dawan
diff --git a/sci-mathematics/bedwyr/ChangeLog b/sci-mathematics/bedwyr/ChangeLog
new file mode 100644
index 0000000..dfb8722
--- /dev/null
+++ b/sci-mathematics/bedwyr/ChangeLog
@@ -0,0 +1,48 @@
+# ChangeLog for sci-mathematics/bedwyr
+# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2
+# $Header: $
+
+*bedwyr-1.4_alpha9 (15 Aug 2013)
+
+  15 Aug 2013; Quentin Heath <dawan@melix.net> -bedwyr-1.4_alpha1.ebuild,
+  +bedwyr-1.4_alpha9.ebuild:
+  - version bump
+  - fix man symlinks
+
+*bedwyr-1.4_alpha1 (13 Jul 2012)
+
+  13 Jul 2012; Quentin Heath <dawan@melix.net> -bedwyr-1.3_rc2.ebuild,
+  +bedwyr-1.4_alpha1.ebuild:
+  - version bump
+  - no more parallel build (because of ocamlbuild)
+  - sci-mathematics/ndcore and sci-mathematics/bedwyr merged
+  - better package layout but empty documentation
+
+*bedwyr-1.3_rc2 (29 Feb 2012)
+
+  29 Feb 2012; Quentin Heath <dawan@melix.net> +bedwyr-1.3_rc2.ebuild:
+  version bump
+
+*bedwyr-1.3_beta10 (24 Feb 2012)
+
+  24 Feb 2012; Quentin Heath <dawan@melix.net> -bedwyr-1.3_beta8-r2.ebuild,
+  +bedwyr-1.3_beta10.ebuild:
+  version bump
+
+*bedwyr-1.3_beta8-r2 (15 Feb 2012)
+
+  15 Feb 2012; Quentin Heath <dawan@melix.net> -bedwyr-1.3_beta6.ebuild,
+  -bedwyr-1.3_beta8.ebuild, +bedwyr-1.3_beta8-r2.ebuild,
+  +files/bedwyr-1.3-beta8-src-Makefile.in.patch:
+  - version bump
+  - parallel make allowed
+  - doc built during compilation
+  - patch for broken makefile dependencies
+
+*bedwyr-1.3_beta8 (14 Feb 2012)
+*bedwyr-1.3_beta6 (14 Feb 2012)
+
+  14 Feb 2012; Quentin Heath <dawan@melix.net> +bedwyr-1.3_beta6.ebuild,
+  +bedwyr-1.3_beta8.ebuild, +metadata.xml:
+  initial ebuild
+
diff --git a/sci-mathematics/bedwyr/Manifest b/sci-mathematics/bedwyr/Manifest
new file mode 100644
index 0000000..0b9b3db
--- /dev/null
+++ b/sci-mathematics/bedwyr/Manifest
@@ -0,0 +1,4 @@
+DIST bedwyr-1.4-alpha9.tbz 205169 SHA256 416603c231a3cfe0f7b79135425845ce6a7824c4d1a414d411c870f03139fb8e SHA512 ba8d14df1c05826ce97018546bf93fc2972d52a3cde17b2177d1f06351d214d38dac74a4235eb984beb8d69b591e393b2fc53f7816e009b01023448b523d38cd WHIRLPOOL 4463412874550e73bd7e086b361c71ac44f15766954cb5c3c7b3eaad881b28d268ac768cf91d628a80cb08d694e4e94f5626690a29462f847b9ad51e52ece8ec
+EBUILD bedwyr-1.4_alpha9.ebuild 1953 SHA256 859aa0b6fff6e4fa72f4bc38a577c62651003b3f615199d2f617eb62c9a0ee55 SHA512 4ce8418c19d01e2ef7c2acf1d16b2e9ef9b87dea3f403851a7c318e517f577d9198d58ba3d8a33448fcefc94e1cc1c7afc23222a57d214fbd65de1ccd5898c10 WHIRLPOOL ac8a327fe20778b04a2ca53c60cc183586e5817ae5fd55dc3d568317f23973b7afc869e0efeca6be1d125eca7a858d2f47841eb2c4df5a50041ff5151d584645
+MISC ChangeLog 1420 SHA256 4d4d29cc68ef961e74578fe160b764fc813f03c51018377764b4aa2751d575a5 SHA512 d9ce3156294a0ed6506fb0d5cc9d4373f112e8c01397c8ae045a404c4d2f6234cfa78a4c965e5bf7547be076040f44fcaea0b58682bbb31ad92c4e713229bfd1 WHIRLPOOL f842f21709a9c9268fbb3b1e6aa638a09122908e0fe1ce930d8c84ca70c7bd40f60727da6830c18c85c222e260bb1daab5892e713a0669c5902f93d06b9d3f86
+MISC metadata.xml 1386 SHA256 68531530ddae77f43095e13ddeede6a3eb3b1a0b95e7d112758a7dca9e2f4889 SHA512 8ff18ef060d150c744bfc563d84da266c8b6ee92f1d798ced9303d2b5830fa8cb08028776e40f2f3cbc912a9fdaa569fea194ad2f5e83f3e5e9b5f9fe4c2b33a WHIRLPOOL a65aa613ae738bd0611311444fa2b1df8cf1f19435f949fa335c9dd7bd581d7493c0d2b3aad56faf3824518b5b0cf17f70743b45f8eb925f3a577f94b24bdcc5
diff --git a/sci-mathematics/bedwyr/bedwyr-1.4_alpha9.ebuild b/sci-mathematics/bedwyr/bedwyr-1.4_alpha9.ebuild
new file mode 100644
index 0000000..93628db
--- /dev/null
+++ b/sci-mathematics/bedwyr/bedwyr-1.4_alpha9.ebuild
@@ -0,0 +1,88 @@
+# Copyright 1999-2013 Quentin Heath
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI=4
+
+inherit eutils autotools
+
+SLOT="1"
+MY_PV="${PV/_/-}"
+TARBALL_NAME="${PN}-${MY_PV}"
+
+DESCRIPTION="Bedwyr, the not-so-sound logician"
+HOMEPAGE="http://slimmer.gforge.inria.fr/bedwyr/"
+SRC_URI="https://gforge.inria.fr/frs/download.php/32337/${TARBALL_NAME}.tbz"
+
+LICENSE="GPL-2"
+KEYWORDS="~amd64 ~x86"
+IUSE="+ocamlopt vim-syntax +rlwrap ledit debug doc"
+
+DEPEND=">=dev-lang/ocaml-3.11.0[ocamlopt?]
+doc? ( app-text/texlive[extra] dev-tex/hevea dev-tex/mathpartir )
+>=sys-devel/autoconf-2.60
+!sci-mathematics/ndcore"
+RDEPEND="${DEPEND}
+rlwrap? ( app-misc/rlwrap )
+ledit? ( app-misc/ledit )
+vim-syntax? ( >=app-editors/vim-7 )"
+
+S="${WORKDIR}/${TARBALL_NAME}"
+
+
+#pkg_setup()
+
+#src_unpack()
+
+src_prepare() {
+	epatch "${FILESDIR}/${TARBALL_NAME}-handle-empty-wildcard-lists.patch"
+	eautoconf
+}
+
+src_configure() {
+	# TODO at some point, use the emacs, tac and spec flags
+	local myconf="--no-create"
+	econf $myconf \
+		$(use_enable ocamlopt nativecode) \
+		$(use_enable debug) \
+		$(use_enable doc) \
+		$(use_with vim-syntax vimfiles)
+}
+
+src_compile() {
+	emake -j1
+	use doc && emake -j1 doc
+}
+
+src_test() {
+	emake -j1 test
+}
+
+src_install() {
+	emake -j1 DESTDIR="${D}" install
+
+	# fix manpage renaming
+	rm "${D}/usr/share/man/man1/bedwyr.byte.1.gz"
+	ln -s "${D}/usr/share/man/man1/bedwyr.1.bz2" bedwyr.byte.1.bz2
+	rm "${D}/usr/share/man/man1/bedwyr.native.1.gz"
+	ln -s "${D}/usr/share/man/man1/bedwyr.1.bz2" bedwyr.native1.bz2
+}
+
+#pkg_preinst()
+
+pkg_postinst() {
+	einfo "Refer to quickstart.html and refman/index.html."
+	einfo "Any feedack is welcome."
+
+	use rlwrap && einfo \
+		"Add \"alias bedwyr='rlwrap -c -Cbedwyr -D2 -g'\\''^(n|y)$'\\'' -m \
+-pgreen -q'\\''\\\"'\\'' bedwyr'\" to ~/.alias."
+	use ledit && einfo \
+		"Add \"alias bedwyr='ledit -h ~/.bedwyr_history bedwyr'\" to ~/.alias."
+}
+
+#pkg_prerm()
+
+#pkg_postrm()
+
+#pkg_config()
diff --git a/sci-mathematics/bedwyr/metadata.xml b/sci-mathematics/bedwyr/metadata.xml
new file mode 100644
index 0000000..096ffd7
--- /dev/null
+++ b/sci-mathematics/bedwyr/metadata.xml
@@ -0,0 +1,32 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+	<herd>no-herd</herd>
+	<maintainer>
+		<email>quentin.heath@inria.fr</email>
+		<name>Quentin Heath</name>
+		<description>Upstream developer</description>
+	</maintainer>
+	<longdescription>
+		Bedwyr is a generalization of logic programming
+		that allows model checking directly on syntactic expression
+		possibly containing bindings.
+		
+		This system, written in OCaml, is a direct implementation of
+		two recent advances in the theory of proof search:
+		a symmetric treatment of finite success and finite failure
+		(which allows capturing both aspects of may and must behavior
+		in operational semantics and mixing model checking and logic programming),
+		and direct support for lambda-tree syntax, as in lambdaProlog,
+		via term-level lambda-binders, higher-order pattern unification,
+		and the nabla-quantifier.
+	</longdescription>
+	<use>
+		<flag name="tac">Install <pkg>sci-mathematics/tac</pkg></flag>
+		<flag name="spec">Install Spec, a fork of Bedwyr</flag>
+		<flag name="rlwrap">Install support for <pkg>app-misc/rlwrap</pkg></flag>
+		<flag name="ledit">Install support for <pkg>app-misc/ledit</pkg></flag>
+	</use>
+	<upstream>http://slimmer.gforge.inria.fr/bedwyr/</upstream>
+	<bugs-to>https://gforge.inria.fr/tracker/?group_id=367</bugs-to>
+</pkgmetadata>