7 files changed, 142 insertions, 0 deletions
diff --git a/sci-mathematics/agda/ChangeLog b/sci-mathematics/agda/ChangeLog
new file mode 100644
index 000000000000..bc8fc3f0868a
--- /dev/null
+++ b/sci-mathematics/agda/ChangeLog
@@ -0,0 +1,12 @@
+# ChangeLog for sci-mathematics/agda
+# Copyright 1999-2006 Gentoo Foundation; Distributed under the GPL v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/agda/ChangeLog,v 1.1 2006/07/12 13:21:35 nattfodd Exp $
+
+*agda-20050601 (12 Jul 2006)
+
+  12 Jul 2006; Alexandre Buisse <nattfodd@gentoo.org>
+  +files/50agda-gentoo.el, +files/agda-make_install.patch, +metadata.xml,
+  +agda-20050601.ebuild:
+  Initial commit. The doc generation is broken for now due to unsupported
+  haddock stuff.
+
diff --git a/sci-mathematics/agda/Manifest b/sci-mathematics/agda/Manifest
new file mode 100644
index 000000000000..8476c47603e1
--- /dev/null
+++ b/sci-mathematics/agda/Manifest
@@ -0,0 +1,34 @@
+-----BEGIN PGP SIGNED MESSAGE-----
+Hash: SHA1
+
+AUX 50agda-gentoo.el 318 RMD160 8562741e1705eb87f9409a4b25d19d5c11ed42a2 SHA1 68d46099ad58b0d6617b3479aeece4e618040f5c SHA256 64f767d1fb3bef2e0b31f13f8ed5764dd3c5ede563c543694946a26ef16e22ee
+MD5 950bd40b72871ca9230771bc5f01ec40 files/50agda-gentoo.el 318
+RMD160 8562741e1705eb87f9409a4b25d19d5c11ed42a2 files/50agda-gentoo.el 318
+SHA256 64f767d1fb3bef2e0b31f13f8ed5764dd3c5ede563c543694946a26ef16e22ee files/50agda-gentoo.el 318
+AUX agda-make_install.patch 549 RMD160 323539535e17244e979f0fd14684f4375e0de4ef SHA1 f7e9a2b633b7c03f305db1210f954f34e5dc4037 SHA256 f23e6fa062ca5ef3c6b1e6b7e9133a19bcf3846e12fdd1659d23d44d252946fc
+MD5 2295b9b9d83dd185900ab3b215f2fc6f files/agda-make_install.patch 549
+RMD160 323539535e17244e979f0fd14684f4375e0de4ef files/agda-make_install.patch 549
+SHA256 f23e6fa062ca5ef3c6b1e6b7e9133a19bcf3846e12fdd1659d23d44d252946fc files/agda-make_install.patch 549
+DIST Agda-1.1-cvs20050601.tar.gz 411993 RMD160 562cd4314f22f8763caa6b1ff025f96924a7fce6 SHA1 a3e19b11bcb43c6e1103ce36d1479d30a4826672 SHA256 75f7efc479f664e0cd12680af40082e93410fc130f9a2881663d54c2853b5814
+EBUILD agda-20050601.ebuild 1364 RMD160 4d5dd63caab61746d09a085ba54b8556bfc1fb5c SHA1 6b22aa8c785f88f3846cbc9a3f7d619a257093f6 SHA256 663b3592154b6056852f6b0cd37e5adb1128529a7fbc94a0875499258bb6775d
+MD5 5c9832edb82f734d8662257470b938f3 agda-20050601.ebuild 1364
+RMD160 4d5dd63caab61746d09a085ba54b8556bfc1fb5c agda-20050601.ebuild 1364
+SHA256 663b3592154b6056852f6b0cd37e5adb1128529a7fbc94a0875499258bb6775d agda-20050601.ebuild 1364
+MISC ChangeLog 490 RMD160 8d257d1ba051d351a31000229828762651d916ec SHA1 070aea7a36e7b63e46af859f5de4c15d10e103b8 SHA256 eb83893f55caef45fce59647a8373b0b760efee9b4abb180fcf87f8a64a5cbc8
+MD5 a66bf9889d42cd94498d5e4b45f278e4 ChangeLog 490
+RMD160 8d257d1ba051d351a31000229828762651d916ec ChangeLog 490
+SHA256 eb83893f55caef45fce59647a8373b0b760efee9b4abb180fcf87f8a64a5cbc8 ChangeLog 490
+MISC metadata.xml 262 RMD160 40a79c7a47bf41357031ea3505d676c48f1f1292 SHA1 84fc35c85f916614b3648fbd909dbbbd1c2471a5 SHA256 123f078e162fb42574af32faee9ded61a0986c3eef35a4ce5989953e464e8c0f
+MD5 dcf379a33cdc813d247f606073b36244 metadata.xml 262
+RMD160 40a79c7a47bf41357031ea3505d676c48f1f1292 metadata.xml 262
+SHA256 123f078e162fb42574af32faee9ded61a0986c3eef35a4ce5989953e464e8c0f metadata.xml 262
+MD5 377344cb60e6d766fe2bdb430ec8713d files/digest-agda-20050601 262
+RMD160 859ba2a4a74df4afcb9d3870ab69d1820117c953 files/digest-agda-20050601 262
+SHA256 444762b6fc59669cd052cc962fc45deb9e3c85f60fcb11942b8d4c99e10ee342 files/digest-agda-20050601 262
+-----BEGIN PGP SIGNATURE-----
+Version: GnuPG v1.4.4 (GNU/Linux)
+
+iD8DBQFEtPfGwx9vvAARv2sRAr6bAKDJLdMd11osQzHnUL0eOzJcZVc5MwCgydQq
+wJ9hw0VxhbrUfiiAwukzZk8=
+=1xE8
+-----END PGP SIGNATURE-----
diff --git a/sci-mathematics/agda/agda-20050601.ebuild b/sci-mathematics/agda/agda-20050601.ebuild
new file mode 100644
index 000000000000..d2157cd689aa
--- /dev/null
+++ b/sci-mathematics/agda/agda-20050601.ebuild
@@ -0,0 +1,60 @@
+# Copyright 1999-2006 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/agda/agda-20050601.ebuild,v 1.1 2006/07/12 13:21:35 nattfodd Exp $
+
+inherit autotools elisp-common
+
+DESCRIPTION="Agda is a proof assistant in Haskell."
+HOMEPAGE="http://www.cs.chalmers.se/~catarina/agda"
+SRC_URI="http://www.coverproject.org/Agda/Agda-1.1-cvs${PV}.tar.gz"
+S="${WORKDIR}/Agda-1.1-cvs${PV}"
+
+
+LICENSE="MIT"
+SLOT="0"
+KEYWORDS="~x86"
+# make html is currently broken
+#IUSE="doc emacs"
+IUSE="emacs"
+
+DEPEND="virtual/ghc
+		emacs? ( virtual/emacs )"
+	#doc? ( dev-haskell/haddock) "
+RDEPEND=""
+
+SITEFILE="50${PN}-gentoo.el"
+
+src_unpack() {
+	unpack ${A}
+	cd "${S}"
+	epatch ${FILESDIR}/${PN}-make_install.patch
+	eaclocal -I macros || die "aclocal failed"
+	eautoconf || die "autoconf failed"
+}
+
+src_compile() {
+	cd "${S}"
+	econf || die "./configure failed"
+	emake || die "make failed"
+	#if use doc ; then
+	#	emake html
+	#fi
+}
+
+src_install() {
+	if use emacs; then
+		cd "${S}/elisp"
+		elisp-install ${PN} *.el
+		elisp-site-file-install ${FILESDIR}/${SITEFILE}
+	fi
+	cd "${S}/src"
+	make prefix="${D}/usr" install || die "make install failed"
+	dosym /usr/lib/EmacsAgda/bin/emacsagda /usr/bin/emacsagda
+	dosym /usr/bin/emacsagda /usr/bin/agda
+}
+
+pkg_postinst() {
+	if use emacs; then
+		elisp-site-regen
+	fi
+}
diff --git a/sci-mathematics/agda/files/50agda-gentoo.el b/sci-mathematics/agda/files/50agda-gentoo.el
new file mode 100644
index 000000000000..dfafe7ed765c
--- /dev/null
+++ b/sci-mathematics/agda/files/50agda-gentoo.el
@@ -0,0 +1,10 @@
+;;; agda site-lisp configuration
+
+(add-to-list 'load-path "@SITELISP@")
+(autoload 'agda-mode "agda-mode.el"
+          "Major mode for Agda files" t)
+(unless (assoc "\\.agda" auto-mode-alist)
+  (setq auto-mode-alist
+        (nconc '(("\\.agda" . agda-mode)
+                 ("\\.alfa" . agda-mode)) auto-mode-alist)))
+
diff --git a/sci-mathematics/agda/files/agda-make_install.patch b/sci-mathematics/agda/files/agda-make_install.patch
new file mode 100644
index 000000000000..0d008acd436b
--- /dev/null
+++ b/sci-mathematics/agda/files/agda-make_install.patch
@@ -0,0 +1,14 @@
+--- Agda-1.1-cvs20050601/src/Makefile.in.old	2006-07-12 14:47:06.000000000 +0200
++++ Agda-1.1-cvs20050601/src/Makefile.in	2006-07-12 14:47:25.000000000 +0200
+@@ -74,10 +74,9 @@
+ 
+ install_bin: emacsagda agdachecker
+ 	${INSTALL} -d ${destdir}/bin/
++	${INSTALL} -d ${bindir}
+ 	cp emacsagda ${destdir}/bin/emacsagda-${VERSION}
+-	-rm ${destdir}/bin/emacsagda
+ 	(cd ${destdir}/bin; ln -s emacsagda-${VERSION} emacsagda)
+-	-(cd ${bindir}; ln -s ${destdir}/bin/emacsagda emacsagda)
+ # No more energy to create variants
+ 	${INSTALL} agdachecker ${bindir}
+ 
diff --git a/sci-mathematics/agda/files/digest-agda-20050601 b/sci-mathematics/agda/files/digest-agda-20050601
new file mode 100644
index 000000000000..afb2a5c03880
--- /dev/null
+++ b/sci-mathematics/agda/files/digest-agda-20050601
@@ -0,0 +1,3 @@
+MD5 0fad57e47dd4bd608fe1152b27c497c6 Agda-1.1-cvs20050601.tar.gz 411993
+RMD160 562cd4314f22f8763caa6b1ff025f96924a7fce6 Agda-1.1-cvs20050601.tar.gz 411993
+SHA256 75f7efc479f664e0cd12680af40082e93410fc130f9a2881663d54c2853b5814 Agda-1.1-cvs20050601.tar.gz 411993
diff --git a/sci-mathematics/agda/metadata.xml b/sci-mathematics/agda/metadata.xml
new file mode 100644
index 000000000000..8d4153f1aea0
--- /dev/null
+++ b/sci-mathematics/agda/metadata.xml
@@ -0,0 +1,9 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+	<herd>math-proof</herd>
+	<maintainer>
+		<email>nattfodd@gentoo.org</email>
+		<name>Alexandre Buisse</name>
+	</maintainer>
+</pkgmetadata>