Date: Thursday, December 28, 2017 @ 09:32:23 Author: felixonmars Revision: 276389
upgpkg: agda 2.5.3-6 avoid building twice - use a better way! Modified: agda/trunk/PKGBUILD Deleted: agda/trunk/unordered-containers-0.2.6.patch ----------------------------------+ PKGBUILD | 24 +++++++--------------- unordered-containers-0.2.6.patch | 40 ------------------------------------- 2 files changed, 8 insertions(+), 56 deletions(-) Modified: PKGBUILD =================================================================== --- PKGBUILD 2017-12-28 08:46:36 UTC (rev 276388) +++ PKGBUILD 2017-12-28 09:32:23 UTC (rev 276389) @@ -5,7 +5,7 @@ _hkgname=Agda pkgname=agda pkgver=2.5.3 -pkgrel=5 +pkgrel=6 pkgdesc="A dependently typed functional programming language and proof assistant" url="http://wiki.portal.chalmers.se/agda/"; license=("custom") @@ -23,9 +23,11 @@ sha512sums=('89cf67d095cb3694a8f266445092620746a04aa866ab3af277f73b304d8c0f54dc7880a6093336f0c4893ee3861fc853bcf7ca48c430f2c8c83b2c24bf6cb97a') prepare() { - # TODO: Find a better way! - # Build it twice to compile the agdai file. - cp -a ${pkgname}-${pkgver}{,-tmp} + mkdir -p lib-target + cp -a $pkgname-$pkgver/src/data/lib lib-target/lib + sed -e "s|rawSystem agda \\[|rawSystem \"env\" [\"Agda_datadir=$PWD/lib-target\", \"LD_LIBRARY_PATH=$PWD/$pkgname-$pkgver/dist/build\", agda,|" \ + -e "s|(ms, datadir dirs|(ms, \"$PWD/lib-target\"|" \ + -i $pkgname-$pkgver/Setup.hs } build() { @@ -40,16 +42,6 @@ runhaskell Setup unregister --gen-script sed -i -r -e "s|ghc-pkg.*update[^ ]* |&'--force' |" register.sh sed -i -r -e "s|ghc-pkg.*unregister[^ ]* |&'--force' |" unregister.sh - - cd "${srcdir}/${pkgname}-${pkgver}-tmp" - runhaskell Setup configure --prefix="$PWD/target" --enable-executable-dynamic --disable-library-vanilla --datasubdir="$pkgname" - LC_CTYPE=en_US.UTF-8 runhaskell Setup build - runhaskell Setup copy - - LD_PRELOAD=(dist/build/libHSAgda-*-ghc*.so) dist/build/agda/agda target/share/agda/lib/prim/Agda/Primitive.agda - for _file in target/share/agda/lib/prim/Agda/Builtin/*.agda; do - LD_PRELOAD=(dist/build/libHSAgda-*-ghc*.so) dist/build/agda/agda "$_file" - done } package() { @@ -61,6 +53,6 @@ install -D -m644 "LICENSE" "${pkgdir}/usr/share/licenses/${pkgname}/LICENSE" rm -f "${pkgdir}/usr/share/doc/${pkgname}/LICENSE" - install -m644 "${srcdir}/${pkgname}-${pkgver}-tmp"/target/share/agda/lib/prim/Agda/Primitive.agdai "$pkgdir"/usr/share/agda/lib/prim/Agda/Primitive.agdai - install -m644 "${srcdir}/${pkgname}-${pkgver}-tmp"/target/share/agda/lib/prim/Agda/Builtin/*.agdai "$pkgdir"/usr/share/agda/lib/prim/Agda/Builtin/ + install -m644 "$srcdir"/lib-target/lib/prim/Agda/Primitive.agdai "$pkgdir"/usr/share/agda/lib/prim/Agda/Primitive.agdai + install -m644 "$srcdir"/lib-target/lib/prim/Agda/Builtin/*.agdai "$pkgdir"/usr/share/agda/lib/prim/Agda/Builtin/ } Deleted: unordered-containers-0.2.6.patch =================================================================== --- unordered-containers-0.2.6.patch 2017-12-28 08:46:36 UTC (rev 276388) +++ unordered-containers-0.2.6.patch 2017-12-28 09:32:23 UTC (rev 276389) @@ -1,40 +0,0 @@ -diff --git a/src/full/Agda/Utils/HashMap.hs b/src/full/Agda/Utils/HashMap.hs -index 5e1da8b..bd14fac 100644 ---- a/src/full/Agda/Utils/HashMap.hs -+++ b/src/full/Agda/Utils/HashMap.hs -@@ -1,29 +1,14 @@ - module Agda.Utils.HashMap - ( module HashMap -- , mapMaybe -- , alter - ) where - --import Data.Hashable - import Data.HashMap.Strict as HashMap --import qualified Data.Maybe as Maybe - ---- | Like 'Data.Map.Strict.mapMaybe'. -+-- ASR (20 January 2016) Issue 1779: I removed the @mapMaybe@ and -+-- @alter@ functions because them currently aren't used and -+-- them were added in unordered-containers 0.2.6.0. - ---- This code has not been benchmarked. Other implementations may be ---- more efficient. -+-- mapMaybe :: (a -> Maybe b) -> HashMap k a -> HashMap k b - --mapMaybe :: (a -> Maybe b) -> HashMap k a -> HashMap k b --mapMaybe f = fmap Maybe.fromJust . HashMap.filter Maybe.isJust . fmap f -- ---- | Like 'Data.Map.Strict.alter'. -- --alter :: (Eq k, Hashable k) => -- (Maybe a -> Maybe a) -> k -> HashMap k a -> HashMap k a --alter f k m = case HashMap.lookup k m of -- Nothing -> case f Nothing of -- Nothing -> m -- Just v -> HashMap.insert k v m -- Just v -> case f (Just v) of -- Nothing -> HashMap.delete k m -- Just v -> HashMap.insert k v m -+-- alter :: (Eq k, Hashable k) => -+-- (Maybe a -> Maybe a) -> k -> HashMap k a -> HashMap k a
