Arch Linux

I was unable to get agda 2.6.0 to compile with the official PKGBUILD due to large changes in Setup.hs breaking the sed scripts. I made some patches for agda-git on the AUR: <https://aur.archlinux.org/packages/agda-git/#comment-691011>. I have also ported them to the official agda package. The second patch in this series also bumps the version because the required functionality was added in v2.5.4.2.20190310. I have included the patches in this bug report, but you can also find them at <http://ix.io/1GUx> and <http://ix.io/1GUy>.

From 43e4c935ad6666ed97ce66bbb8fa7c7dd4b8e4ff Mon Sep 17 00:00:00 2001
From: Sean Anderson <seanga2@gmail.com>
Date: Mon, 22 Apr 2019 15:37:56 -0400
Subject: [PATCH 1/2] Fix compilation for 2.6.0

`Setup.hs` has changed considerably since the sed scripts were first
created. This patch updates them. In addition, we need to disable
copying `agdai` files by the script, since we will do it manually.
---
repos/community-x86_64/PKGBUILD | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/repos/community-x86_64/PKGBUILD b/repos/community-x86_64/PKGBUILD
index cb3ea20..cd83f3f 100644
--- a/repos/community-x86_64/PKGBUILD
+++ b/repos/community-x86_64/PKGBUILD
@@ -28,9 +28,9 @@ prepare() {
cp -a $pkgname-$pkgver/src/data/lib lib-target/lib

cd $pkgname-$pkgver
- sed -e "s|rawSystem agda \\[|rawSystem \"env\" [\"Agda_datadir=$PWD/../lib-target\", \"LD_LIBRARY_PATH=$PWD/dist/build\", agda,|" \
- -e "s|datadir dirs|\"$PWD/../lib-target\"|" \
- -e 's|"Builtins"|"Builtin"|' \
+ sed -e "s|(\"Agda_datadir\", agda_datadir) : e|[(\"Agda_datadir\",\"$PWD/../lib-target\"), (\"LD_LIBRARY_PATH\", \"$PWD/dist/build\")] ++ e|" \
+ -e "s|ddir <- .*|let ddir = \"$PWD/lib-target\"|" \
+ -e "s|pd' = pd .*|pd' = pd|" \
-i Setup.hs

sed -i 's/== 0.5/>= 0.5/' Agda.cabal
--
2.21.0

From 7d56c6a39443db5a5b7a160b50e0769d5a7c2c9a Mon Sep 17 00:00:00 2001
From: Sean Anderson <seanga2@gmail.com>
Date: Mon, 22 Apr 2019 15:51:28 -0400
Subject: [PATCH 2/2] Don't use a separate lib-target

There is no longer any need to use a separate lib-target directory to
generate agdai files for the builtin library, since `Setup.hs` can do it
for us now.
---
repos/community-x86_64/PKGBUILD | 15 ++++-----------
1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/repos/community-x86_64/PKGBUILD b/repos/community-x86_64/PKGBUILD
index cd83f3f..f6fcc16 100644
--- a/repos/community-x86_64/PKGBUILD
+++ b/repos/community-x86_64/PKGBUILD
@@ -3,8 +3,8 @@

_hkgname=Agda
pkgname=agda
-pkgver=2.5.99.20190207
-_commit=3048fdaa1840c352fc00aa7222c50bcd622580d8
+pkgver=2.6.0
+_commit=16eb89fb0c20b02bfa667c2bf1234ecca3028022
pkgrel=13
pkgdesc="A dependently typed functional programming language and proof assistant"
url="https://wiki.portal.chalmers.se/agda/"
@@ -19,7 +19,7 @@ depends=('ghc-libs' 'haskell-aeson' 'haskell-async' 'haskell-blaze-html' 'haskel
optdepends=('agda-stdlib: for standard library')
makedepends=('alex' 'happy' 'ghc' 'haskell-filemanip')
source=("$_hkgname-$_commit.tar.gz::https://github.com/agda/agda/archive/$_commit.tar.gz")
-sha512sums=('21b061fada9b3ddfb1348366f270990192eefe49e79943a061d843d6fe78c049b87fde73ff3cf70c586e955c8aa5007365723b380686931a55547deae87e0043')
+sha512sums=('b32d4806895a681722afb606e169643f1a7f25bb87776b1e16808365ce340584e1c0e739de58f646d08349cc744896f7eb313539dd45cdaac2f733cb204e3a6a')

prepare() {
mv $pkgname-{$_commit,$pkgver}
@@ -28,9 +28,7 @@ prepare() {
cp -a $pkgname-$pkgver/src/data/lib lib-target/lib

cd $pkgname-$pkgver
- sed -e "s|(\"Agda_datadir\", agda_datadir) : e|[(\"Agda_datadir\",\"$PWD/../lib-target\"), (\"LD_LIBRARY_PATH\", \"$PWD/dist/build\")] ++ e|" \
- -e "s|ddir <- .*|let ddir = \"$PWD/lib-target\"|" \
- -e "s|pd' = pd .*|pd' = pd|" \
+ sed -e "s|(\"Agda_datadir\", agda_datadir) : e|[(\"Agda_datadir\", agda_datadir), (\"LD_LIBRARY_PATH\", \"$PWD/dist/build\")] ++ e|" \
-i Setup.hs

sed -i 's/== 0.5/>= 0.5/' Agda.cabal
@@ -58,9 +56,4 @@ package() {
runhaskell Setup copy --destdir="${pkgdir}"
install -D -m644 "LICENSE" "${pkgdir}/usr/share/licenses/${pkgname}/LICENSE"
rm -f "${pkgdir}/usr/share/doc/${pkgname}/LICENSE"
-
- install -m644 "$srcdir"/lib-target/lib/prim/Agda/*.agdai "$pkgdir"/usr/share/agda/lib/prim/Agda/
- install -m644 "$srcdir"/lib-target/lib/prim/Agda/Builtin/*.agdai "$pkgdir"/usr/share/agda/lib/prim/Agda/Builtin/
- install -m644 "$srcdir"/lib-target/lib/prim/Agda/Builtin/Cubical/*.agdai "$pkgdir"/usr/share/agda/lib/prim/Agda/Builtin/Cubical/
- install -m644 "$srcdir"/lib-target/lib/prim/Agda/Primitive/*.agdai "$pkgdir"/usr/share/agda/lib/prim/Agda/Primitive/
}
--
2.21.0