From debbugs-submit-bounces@debbugs.gnu.org Sun Aug 06 11:54:52 2017 Received: (at submit) by debbugs.gnu.org; 6 Aug 2017 15:54:52 +0000 Received: from localhost ([127.0.0.1]:44893 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1deNtA-0001L2-5d for submit@debbugs.gnu.org; Sun, 06 Aug 2017 11:54:52 -0400 Received: from eggs.gnu.org ([208.118.235.92]:54984) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1deNt8-0001Kn-I5 for submit@debbugs.gnu.org; Sun, 06 Aug 2017 11:54:47 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1deNt1-0008Mz-1A for submit@debbugs.gnu.org; Sun, 06 Aug 2017 11:54:41 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: * X-Spam-Status: No, score=1.1 required=5.0 tests=BAYES_50, FREEMAIL_ENVFROM_END_DIGIT,FREEMAIL_FROM,T_DKIM_INVALID autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:42869) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1deNt0-0008Mr-Rs for submit@debbugs.gnu.org; Sun, 06 Aug 2017 11:54:38 -0400 Received: from eggs.gnu.org ([2001:4830:134:3::10]:45940) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1deNsy-00081S-HD for guix-patches@gnu.org; Sun, 06 Aug 2017 11:54:38 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1deNsu-0008J2-IH for guix-patches@gnu.org; Sun, 06 Aug 2017 11:54:36 -0400 Received: from mail-pg0-x22b.google.com ([2607:f8b0:400e:c05::22b]:36645) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1deNsu-0008I2-4h for guix-patches@gnu.org; Sun, 06 Aug 2017 11:54:32 -0400 Received: by mail-pg0-x22b.google.com with SMTP id v77so24934134pgb.3 for ; Sun, 06 Aug 2017 08:54:30 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:subject:date:message-id:mime-version; bh=s9/vPiAXgQFg44+/z9E314kOYUceT4SIL1kdeaZiSPA=; b=eyCFgd/vlWXxXsSOKrUxfKMzDXdI8zEYnayo0I68SVhnZwRIRXQODhkwMbi+F1hVsg Mdn1b8XCWqg1GVWpQXOaf/4MbZoBRBVUvXyVqJ7q7XdNOitjiCB84lBLscpsjK2uMCeR KOvLbrCh7mJcaJMjXFw7wIA8VAeirYgg9NHFCLKPHi1fvl5PwANKKfbLiTHJ9Cj17QE/ 7BFP8Yf+et/T0mC5mnQCx8ZJmeDzL6gf0ZpjGjKGUQMKg4PjW7n0/EukN+hgZt0u+v16 40remuOQTapOdrZLe/rwwMwqbOfsUYNWOpb1Rdgq8S0AQR/AwxRDZi7gpzMU7fNaGsCg H2eQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:subject:date:message-id:mime-version; bh=s9/vPiAXgQFg44+/z9E314kOYUceT4SIL1kdeaZiSPA=; b=liY3oXyQ75D9sfj0OYCpd551bBuWG4+ybZ52wwMdbXgXL+3yr83PaCNPgc3VfCsJEZ b0tYOIwZE4EDX7kdQ1N0HevJZVzF77hXgp7BbA0nDPD85Kk70SDXh+ZTMk/faz4MBUZZ jvpGwvyq/HgB7p7bwwb1KRadTKqbhq0rFGWQ4SeUtAWCtnRK9ZVdqkDCxn9Ruv6JC0DL EwsOpPRF/+1uNJMck52/g9JU0q5T7dmR3n+M9/1Hj9D4IOL22WQRUWQTiv2EFmtpu6Jf weFWtMoCZdOGJyR9x9fzb13LLDU1cjgzuxHVnaNxHb8400eAO3dv+D4H6JQa0G9VXzhH 1AwA== X-Gm-Message-State: AHYfb5g2SfJNPrwyqpPTX3mVDICjjZ7raWX/OrhjsJqLLNAfO73u/z5n XfjwvCRPPnbXjIPp X-Received: by 10.98.108.9 with SMTP id h9mr9124843pfc.277.1502034869528; Sun, 06 Aug 2017 08:54:29 -0700 (PDT) Received: from debian (1-64-80-187.static.netvigator.com. [1.64.80.187]) by smtp.gmail.com with ESMTPSA id 64sm9699978pff.168.2017.08.06.08.54.26 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sun, 06 Aug 2017 08:54:27 -0700 (PDT) From: Alex Vong To: guix-patches@gnu.org Subject: Dependencies for Agda - a dependently typed functional language Date: Sun, 06 Aug 2017 23:54:14 +0800 Message-ID: <87efsoofo9.fsf@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="==-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -3.8 (---) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.8 (---) --==-=-= Content-Type: multipart/mixed; boundary="=-=-=" --=-=-= Content-Type: text/plain Hello, I wish to introduce Agda to Guix. The patches below are some dependecies for Agda. There are more to come... --=-=-= Content-Type: text/x-diff; charset=utf-8 Content-Disposition: inline; filename=0001-gnu-cpphs-Update-to-1.20.8.patch Content-Transfer-Encoding: quoted-printable From=20792e06adee38186dc3154b8e5f3f84db3875e019 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Sun, 6 Aug 2017 23:35:06 +0800 Subject: [PATCH 1/6] gnu: cpphs: Update to 1.20.8. * gnu/packages/haskell.scm (cpphs): Update to 1.20.8. =2D-- gnu/packages/haskell.scm | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index a67209234..a42d17d46 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -10,6 +10,7 @@ ;;; Copyright =C2=A9 2016, 2017 David Craven ;;; Copyright =C2=A9 2017 Danny Milosavljevic ;;; Copyright =C2=A9 2017 Peter Mikkelsen +;;; Copyright =C2=A9 2017 Alex Vong ;;; ;;; This file is part of GNU Guix. ;;; @@ -1324,7 +1325,7 @@ various Haskell streaming data libraries, such as @co= de{conduit} and (define-public cpphs (package (name "cpphs") =2D (version "1.19.3") + (version "1.20.8") (source (origin (method url-fetch) @@ -1333,7 +1334,7 @@ various Haskell streaming data libraries, such as @co= de{conduit} and name "-" version ".tar.gz")) (sha256 (base32 =2D "1njpmxgpah5pcqppcl1cxb5xicf6xlqrd162qm12khp9hainlm72")))) + "1bh524asqhk9v1s0wvipl0hgn7l63iy3js867yv0z3h5v2kn8vg5")))) (build-system haskell-build-system) (inputs `(("ghc-polyparse" ,ghc-polyparse) =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0002-gnu-Add-ghc-strict.patch Content-Transfer-Encoding: quoted-printable From=2097d360bb46d727a5129416cd4bfaea54cd0adede Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Sun, 6 Aug 2017 23:37:15 +0800 Subject: [PATCH 2/6] gnu: Add ghc-strict. * gnu/packages/haskell.scm (ghc-strict): New variable. =2D-- gnu/packages/haskell.scm | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index a42d17d46..d0e6a64ce 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -1808,6 +1808,25 @@ capabilities that are optimized for performance crit= ical use, both in terms of large data quantities and high speed.") (license license:bsd-3))) =20 +(define-public ghc-strict + (package + (name "ghc-strict") + (version "0.3.2") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/strict/str= ict-" + version ".tar.gz")) + (sha256 + (base32 "08cjajqz9h47fkq98mlf3rc8n5ghbmnmgn8pfsl3bdldjdkmmlrc")))) + (build-system haskell-build-system) + (home-page "https://hackage.haskell.org/package/strict") + (synopsis "Strict data types and String IO") + (description + "This package provides strict versions of some standard Haskell data = types +(pairs, Maybe and Either). It also contains strict IO operations.") + (license license:bsd-3))) + (define-public ghc-hashable (package (name "ghc-hashable") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0003-gnu-Add-ghc-stmonadtrans.patch Content-Transfer-Encoding: quoted-printable From=2048566e3dd705cbd2f8ad34b38e03e639e9e6e5a7 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Sun, 6 Aug 2017 23:39:55 +0800 Subject: [PATCH 3/6] gnu: Add ghc-stmonadtrans. * gnu/packages/haskell.scm (ghc-stmonadtrans): New variable. =2D-- gnu/packages/haskell.scm | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index d0e6a64ce..44797a226 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -7076,6 +7076,31 @@ other transformers.") (base32 "0a364zfcm17mhpy0c4ms2j88sys4yvgd6071qsgk93la2wjm8mkr"))))= )) =20 +(define-public ghc-stmonadtrans + (package + (name "ghc-stmonadtrans") + (version "0.4.3") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/STMonadTra= ns" + "/STMonadTrans-" version ".tar.gz")) + (sha256 + (base32 "1nr26fnmi5fdjc6d00w13kjhmfyvb5b837d0006w4dj0yxndaksp")))) + (build-system haskell-build-system) + (inputs + `(("ghc-mtl" ,ghc-mtl))) + (home-page "https://hackage.haskell.org/package/STMonadTrans") + (synopsis "Monad transformer version of the ST monad") + (description + "A monad transformer version of the ST monad Warning! This monad +transformer should not be used with monads that can contain multiple answe= rs, +like the list monad. The reason is that the state token will be duplicated +across the different answers and this causes Bad Things to happen (such as= loss +of referential transparency). Safe monads include the monads State, Reade= r, +Writer, Maybe and combinations of their corresponding monad transformers.") + (license license:bsd-3))) + (define-public ghc-findbin (package (name "ghc-findbin") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0004-gnu-Add-ghc-edit-distance.patch Content-Transfer-Encoding: quoted-printable From=202c47df61ed829417127916a44877809eb934640b Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Sun, 6 Aug 2017 23:41:38 +0800 Subject: [PATCH 4/6] gnu: Add ghc-edit-distance. * gnu/packages/haskell.scm (ghc-edit-distance): New variable. =2D-- gnu/packages/haskell.scm | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 44797a226..8726977f1 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -6098,6 +6098,30 @@ supports for high level forms of ASN1 (BER, and DER)= .") when ASN1 pattern matching is not convenient.") (license license:bsd-3))) =20 +(define-public ghc-edit-distance + (package + (name "ghc-edit-distance") + (version "0.2.2.1") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/edit-dista= nce" + "/edit-distance-" version ".tar.gz")) + (sha256 + (base32 "0jkca97zyv23yyilp3jydcrzxqhyk27swhzh82llvban5zp8b21y")))) + (build-system haskell-build-system) + (inputs + `(("ghc-random" ,ghc-random) + ("ghc-test-framework" ,ghc-test-framework) + ("ghc-quickcheck" ,ghc-quickcheck) + ("ghc-test-framework-quickcheck2" ,ghc-test-framework-quickcheck2))) + (home-page "https://github.com/phadej/edit-distance") + (synopsis "Levenshtein and restricted Damerau-Levenshtein edit distanc= es") + (description + "Optimized edit distances for fuzzy matching, including Levenshtein a= nd +restricted Damerau-Levenshtein algorithms.") + (license license:bsd-3))) + (define-public ghc-tasty-kat (package (name "ghc-tasty-kat") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0005-gnu-Add-ghc-boxes.patch Content-Transfer-Encoding: quoted-printable From=2028ebe7e4b96d61f5f55c3af517a871127baf5dfd Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Sun, 6 Aug 2017 23:42:32 +0800 Subject: [PATCH 5/6] gnu: Add ghc-boxes. * gnu/packages/haskell.scm (ghc-boxes): New variable. =2D-- gnu/packages/haskell.scm | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 8726977f1..33e7af969 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -5101,6 +5101,28 @@ prettified JSON to stdout. It also offers a complem= entary \"compact\"-mode, essentially the opposite of pretty-printing.") (license license:bsd-3))) =20 +(define-public ghc-boxes + (package + (name "ghc-boxes") + (version "0.1.4") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/boxes/boxe= s-" + version ".tar.gz")) + (sha256 + (base32 "1n7xiplzd3s1a39nizwjcgsh3wi2348mp21c3fk19v98ialfjgjf")))) + (build-system haskell-build-system) + (inputs + `(("ghc-split" ,ghc-split) + ("ghc-quickcheck" ,ghc-quickcheck))) + (home-page "https://hackage.haskell.org/package/boxes") + (synopsis "2D text pretty-printing library") + (description + "A pretty-printing library for laying out text in two dimensions, +using a simple box model.") + (license license:bsd-3))) + (define-public ghc-wai (package (name "ghc-wai") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0006-gnu-Add-ghc-equivalence.patch Content-Transfer-Encoding: quoted-printable From=20a4c668273df8e726625bf4c8aa828d13bca946f2 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Sun, 6 Aug 2017 23:43:53 +0800 Subject: [PATCH 6/6] gnu: Add ghc-equivalence. * gnu/packages/haskell.scm (ghc-equivalence): New variable. =2D-- gnu/packages/haskell.scm | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 33e7af969..60ded9651 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -4714,6 +4714,36 @@ definition of @code{Monad}.") for Haskell.") (license license:bsd-3))) =20 +(define-public ghc-equivalence + (package + (name "ghc-equivalence") + (version "0.3.2") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/equivalenc= e" + "/equivalence-" version ".tar.gz")) + (sha256 + (base32 "0a85bdyyvjqs5z4kfhhf758210k9gi9dv42ik66a3jl0z7aix8kx")))) + (build-system haskell-build-system) + (inputs + `(("ghc-mtl" ,ghc-mtl) + ("ghc-stmonadtrans" ,ghc-stmonadtrans) + ("ghc-transformers-compat" ,ghc-transformers-compat) + ("ghc-quickcheck" ,ghc-quickcheck) + ("ghc-test-framework" ,ghc-test-framework) + ("ghc-test-framework-quickcheck2" ,ghc-test-framework-quickcheck2))) + (home-page "https://github.com/pa-ba/equivalence") + (synopsis + "Maintaining an equivalence relation implemented as union-find using = STT") + (description + "This is an implementation of Tarjan's Union-Find algorithm +(Robert E.@: Tarjan. \"Efficiency of a Good But Not Linear Set Union + Algorithm\",JACM 22(2), 1975) in order to maintain an equivalence = relation. +This implementation is a port of the @code{union-find} package using the ST +monad transformer (instead of the IO monad).") + (license license:bsd-3))) + (define-public ghc-fast-logger (package (name "ghc-fast-logger") =2D-=20 2.13.4 --=-=-= Content-Type: text/plain Cheers, Alex --=-=-=-- --==-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdZDkzSn0Cycogr9IxYq4eRf1Ea4FAlmHO6YACgkQxYq4eRf1 Ea5FHg//QxW5F6ysoF1o788P5B8SHsf2ytcjHjpx/DS4rj8AessbPfexz0G2b+vH MRYVb92yYgPRABMUH2zhmiIvZxcAxFdJcNzu1iU8jol4FCnIQEDzhQLEZvkxHwUh eQvYhub4SlbIoVs4tjLCAls0mEk7k0VEQ323S1JpCthw1rJNPaZDRkPWe8dd49vf ex9ixGDGKCOWjUd2F3oroQBBFWasFGWM2/nCSbQLfH9E0sYxsTi50idfeo1bI5J3 IDKQJbadAGlFWFNilJTVh6XoC9XxaR7l/f3cwbiCIadM3OQI8wNTd426PbvkLEtD SuWsl7129UWPKHxK4xJiblRxL52t/m/hMW9PMc76FWdlFQjvO0ov69GCFstVq5+N TyG+Qw22nsDeFfccBaef7Vi5agSPYyvvnm4XaX5QlVCKBEOtuk4h7B2wm/mHj1SC 1LDkXydHHnXpDnsGZmCww6mDho9pRcvd6temhh9S+Sifd5C3NJWgdSZEgyQ9F2lZ 4fSjKzykyG5OzlaoTOKDEQ0gjdsfVbY7If3YUEdtcCMtVLg48BrNcPJZ+YTbDYcw 5Z309pXErqdOGWyJQ12X3EaihbA/fU90fcMtDCofDmrj2YLh988Bba7FTzealWpF f36srmuBwbdHd/I8O2xRGQ189D57kugc2F2d46+xPhB1VjqTD8A= =P4z5 -----END PGP SIGNATURE----- --==-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Mon Aug 07 03:34:55 2017 Received: (at 27987) by debbugs.gnu.org; 7 Aug 2017 07:34:55 +0000 Received: from localhost ([127.0.0.1]:45221 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1decYw-000685-R6 for submit@debbugs.gnu.org; Mon, 07 Aug 2017 03:34:55 -0400 Received: from mail-pg0-f48.google.com ([74.125.83.48]:34455) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1decYu-00067s-QT for 27987@debbugs.gnu.org; Mon, 07 Aug 2017 03:34:53 -0400 Received: by mail-pg0-f48.google.com with SMTP id u185so30910688pgb.1 for <27987@debbugs.gnu.org>; Mon, 07 Aug 2017 00:34:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:subject:date:message-id:user-agent:mime-version; bh=07tkQ+MaxmcOedQ85xNC7n/Du9CDd4IrXQoHFwhQi8g=; b=Z+Wvqp4jAeFCNfC33Qt6kRRrcKWmQOIbanw21Nr+F8Jpco8Sa+zSrNiwdj1uLmNMtU 7bcY3XWsms1EWJ2M9Xetcwg76VVaaRLMtM1XcqstE9pIjC66VQr/nvHysKiL532D3ONM ISej4JqzPqmP1BTCHCF2Z1cLaxESgKVgAwY+dnFcM/gIjogJ0OHfl3K42PVANJyvadSX JuTcrH7DnwNtmRtK50ApTQkKOwzQXClpFrjeiZJOLnzRXUS0I2xQ6T23LFGywUWWkMn8 LEx1JmyZx7lWCCHCuOgf7TWEHzaP2T843h/ZZLt+TPm6dRmekRfVMz9s15zqpTpNa+N2 eSlQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:subject:date:message-id:user-agent :mime-version; bh=07tkQ+MaxmcOedQ85xNC7n/Du9CDd4IrXQoHFwhQi8g=; b=XpztgTKd9R0Z114L4erqOKAX0/diES7apBhXUbB7G6y0+RhgSbKC9H0HRH+ICZ1njP YjbPK4V1ho19sRriIV0C4oSv6MjDcdzy1j2yM1r2/9yWK5j1Yw91YP/LLPr7ceFsLQ+f TQb7LdPUC/fFvL1BvJEwjoSieAvGjZ4qs7Rh36D9gjKO0YQZMfld6xvSADrf0SFEjT// FllFbAm7RQ7xvXHnonm+T4ZD7teCtCnldgcfjSVaR/HGjvaG2t5n5kIF0Q8C1nyor3+q NT4/sLMfuzgfoUMICvmm5BN6TB7pkcuZvQz8z099BCzOvkrpcA7QwryY24uHPDQw2r6P dgGA== X-Gm-Message-State: AIVw1127slVBq4QNPF+tflG4dcPS1S3GtKkKCtgj/CmMoiE470zf12So l6smMhKBzMwIug== X-Received: by 10.98.72.90 with SMTP id v87mr11223996pfa.337.1502091286733; Mon, 07 Aug 2017 00:34:46 -0700 (PDT) Received: from debian (pcd372105.netvigator.com. [203.218.162.105]) by smtp.gmail.com with ESMTPSA id d4sm13552700pfj.59.2017.08.07.00.34.39 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Mon, 07 Aug 2017 00:34:40 -0700 (PDT) From: Alex Vong To: 27987@debbugs.gnu.org Subject: Re: Dependencies for Agda - a dependently typed functional language Date: Mon, 07 Aug 2017 15:34:26 +0800 Message-ID: <87valzde65.fsf@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: multipart/signed; boundary="==-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-Spam-Score: -2.0 (--) X-Debbugs-Envelope-To: 27987 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.0 (--) --==-=-= Content-Type: multipart/mixed; boundary="=-=-=" --=-=-= Content-Type: text/plain Hello, Here is the remaining dependencies for Agda. Actually I have already managed to get Agda to build, but I still need to figure out how to build the standard library. --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0001-gnu-Add-ghc-data-hash.patch Content-Transfer-Encoding: quoted-printable From=208c38d3e533717c67ab91cfa72c8d8553798987d6 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Mon, 7 Aug 2017 15:02:41 +0800 Subject: [PATCH 1/8] gnu: Add ghc-data-hash. * gnu/packages/haskell.scm (ghc-data-hash): New variable. =2D-- gnu/packages/haskell.scm | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 60ded9651..d054753b3 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -1857,6 +1857,29 @@ data structures. The package provides instances for= basic types and a way to combine hash values.") (license license:bsd-3))) =20 +(define-public ghc-data-hash + (package + (name "ghc-data-hash") + (version "0.2.0.1") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/data-hash" + "/data-hash-" version ".tar.gz")) + (sha256 + (base32 "1ghbqvc48gf9p8wiy71hdpaj7by3b9cw6wgwi3qqz8iw054xs5wi")))) + (build-system haskell-build-system) + (inputs + `(("ghc-quickcheck" ,ghc-quickcheck) + ("ghc-test-framework" ,ghc-test-framework) + ("ghc-test-framework-quickcheck2" ,ghc-test-framework-quickcheck2))) + (home-page "https://hackage.haskell.org/package/data-hash") + (synopsis "Combinators for building fast hashing functions") + (description + "Combinators for building fast hashing functions. Includes hashing +functions for all basic Haskell98 types.") + (license license:bsd-3))) + (define-public ghc-hunit (package (name "ghc-hunit") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0002-gnu-Add-ghc-murmur-hash.patch Content-Transfer-Encoding: quoted-printable From=205cdf99afbd92e9181e9213979de7e7bbc02c41f9 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Mon, 7 Aug 2017 15:05:36 +0800 Subject: [PATCH 2/8] gnu: Add ghc-murmur-hash. * gnu/packages/haskell.scm (ghc-murmur-hash): New variable. =2D-- gnu/packages/haskell.scm | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index d054753b3..4b1543233 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -1880,6 +1880,27 @@ combine hash values.") functions for all basic Haskell98 types.") (license license:bsd-3))) =20 +(define-public ghc-murmur-hash + (package + (name "ghc-murmur-hash") + (version "0.1.0.9") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/murmur-has= h" + "/murmur-hash-" version ".tar.gz")) + (sha256 + (base32 "1bb58kfnzvx3mpc0rc0dhqc1fk36nm8prd6gvf20gk6lxaadpfc9")))) + (build-system haskell-build-system) + (home-page "https://github.com/nominolo/murmur-hash") + (synopsis "MurmurHash2 implementation for Haskell") + (description + "Implements MurmurHash2, a good, fast, general-purpose, non-cryptogra= phic +hashing function. See @url{https://sites.google.com/site/murmurhash/} for +details. This implementation is pure Haskell, so it might be a bit slower= than +a C FFI binding.") + (license license:bsd-3))) + (define-public ghc-hunit (package (name "ghc-hunit") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0003-gnu-Add-ghc-edisonapi.patch Content-Transfer-Encoding: quoted-printable From=20abc98c9c108aac8591c002426dabc4b10e267647 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Mon, 7 Aug 2017 15:09:03 +0800 Subject: [PATCH 3/8] gnu: Add ghc-edisonapi. * gnu/packages/haskell.scm (ghc-edisonapi): New variable. =2D-- gnu/packages/haskell.scm | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 4b1543233..e2fa7aace 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -3870,6 +3870,31 @@ different keys; hence the name. Also provided is a = @code{locker} type, representing a store for a single element.") (license license:bsd-3))) =20 +(define-public ghc-edisonapi + (package + (name "ghc-edisonapi") + (version "1.3.1") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/EdisonAPI" + "/EdisonAPI-" version ".tar.gz")) + (sha256 + (base32 "0vmmlsj8ggbpwx6fkf5fvb6jp0zpx6iba6b28m80lllr2p8bi8wm")))) + (build-system haskell-build-system) + (inputs `(("ghc-mtl" ,ghc-mtl))) + (home-page "http://rwd.rdockins.name/edison/home/") + (synopsis "Library of efficient, purely-functional data structures (AP= I)") + (description + "Edison is a library of purely functional data structures written by +Chris Okasaki. It is named after Thomas Alva Edison and for the mnemonic = value +EDiSon (Efficient Data Structures). Edison provides several families of +abstractions, each with multiple implementations. The main abstractions +provided by Edison are: Sequences such as stacks, queues, and dequeues; +Collections such as sets, bags and heaps; and Associative Collections such= as +finite maps and priority queues where the priority and element are distinc= t.") + (license license:expat))) + (define-public ghc-mmorph (package (name "ghc-mmorph") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0004-gnu-Add-ghc-edisoncore.patch Content-Transfer-Encoding: quoted-printable From=200dd3f97e1764a0fad07859895c683b64cfa6e6de Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Mon, 7 Aug 2017 15:10:39 +0800 Subject: [PATCH 4/8] gnu: Add ghc-edisoncore. * gnu/packages/haskell.scm (ghc-edisoncore): New variable. =2D-- gnu/packages/haskell.scm | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index e2fa7aace..8a08ad906 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -3895,6 +3895,34 @@ Collections such as sets, bags and heaps; and Associ= ative Collections such as finite maps and priority queues where the priority and element are distinc= t.") (license license:expat))) =20 +(define-public ghc-edisoncore + (package + (name "ghc-edisoncore") + (version "1.3.1.1") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/EdisonCore" + "/EdisonCore-" version ".tar.gz")) + (sha256 + (base32 "06shxmcqxcahcn6zgl64vlqix4fnq53d97drcgsh94qp7gp201ry")))) + (build-system haskell-build-system) + (inputs + `(("ghc-mtl" ,ghc-mtl) + ("ghc-quickcheck" ,ghc-quickcheck) + ("ghc-edisonapi" ,ghc-edisonapi))) + (home-page "http://rwd.rdockins.name/edison/home/") + (synopsis + "Library of efficent, purely-functional data structures +(Core Implementations)") + (description + "This package provides the core Edison data structure implementations, +including multiple sequence, set, bag, and finite map concrete implementat= ions +with various performance characteristics. The implementations in this pac= kage +have no dependencies other than those commonly bundled with Haskell +compilers.") + (license license:expat))) + (define-public ghc-mmorph (package (name "ghc-mmorph") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0005-gnu-Add-ghc-fail.patch Content-Transfer-Encoding: quoted-printable From=20e43cfe603c08d70423af42f35173294a15145a05 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Mon, 7 Aug 2017 15:13:42 +0800 Subject: [PATCH 5/8] gnu: Add ghc-fail. * gnu/packages/haskell.scm (ghc-fail): New variable. =2D-- gnu/packages/haskell.scm | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 8a08ad906..4a322ca4b 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -3972,6 +3972,30 @@ a subset of @code{MonadBase} into which generic cont= rol operations such as @code{catch} can be lifted from @code{IO} or any other base monad.") (license license:bsd-3))) =20 +(define-public ghc-fail + (package + (name "ghc-fail") + (version "4.9.0.0") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/fail/fail-" + version ".tar.gz")) + (sha256 + (base32 "18nlj6xvnggy61gwbyrpmvbdkq928wv0wx2zcsljb52kbhddnp3d")))) + (build-system haskell-build-system) + (home-page "https://prime.haskell.org/wiki/Libraries/Proposals/MonadFa= il") + (synopsis "Forward-compatible MonadFail class") + (description + "This package contains the \"Control.Monad.Fail\" module providing the +@uref{https://prime.haskell.org/wiki/Libraries/Proposals/MonadFail, MonadF= ail} +class that became available in +@uref{https://hackage.haskell.org/package/base-4.9.0.0, base-4.9.0.0} for = older +@code{base} package versions. This package turns into an empty package wh= en +used with GHC versions which already provide the \"Control.Monad.Fail\" mo= dule +to make way for GHC's own \"Control.Monad.Fail\" module.") + (license license:bsd-3))) + (define-public ghc-byteorder (package (name "ghc-byteorder") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0006-gnu-Add-ghc-monadplus.patch Content-Transfer-Encoding: quoted-printable From=20d21b1af8916ae507400a9a8e2cb51c9bdb72586b Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Mon, 7 Aug 2017 15:15:12 +0800 Subject: [PATCH 6/8] gnu: Add ghc-monadplus. * gnu/packages/haskell.scm (ghc-monadplus): New variable. =2D-- gnu/packages/haskell.scm | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 4a322ca4b..6ad6f7799 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -3996,6 +3996,26 @@ used with GHC versions which already provide the \"C= ontrol.Monad.Fail\" module to make way for GHC's own \"Control.Monad.Fail\" module.") (license license:bsd-3))) =20 +(define-public ghc-monadplus + (package + (name "ghc-monadplus") + (version "1.4.2") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/monadplus" + "/monadplus-" version ".tar.gz")) + (sha256 + (base32 "15b5320wdpmdp5slpphnc1x4rhjch3igw245dp2jxbqyvchdavin")))) + (build-system haskell-build-system) + (home-page "https://hackage.haskell.org/package/monadplus") + (synopsis + "Filtering and folding over arbitrary @code{MonadPlus} instances") + (description + "This package generalizes many common stream operations such as +@code{filter}, @code{catMaybes} etc.") + (license license:bsd-3))) + (define-public ghc-byteorder (package (name "ghc-byteorder") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0007-gnu-Add-ghc-geniplate-mirror.patch Content-Transfer-Encoding: quoted-printable From=20857831b8908aa6d8732be76878b2dba3fed93f07 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Mon, 7 Aug 2017 15:20:37 +0800 Subject: [PATCH 7/8] gnu: Add ghc-geniplate-mirror. * gnu/packages/haskell.scm (ghc-geniplate-mirror): New variable. =2D-- gnu/packages/haskell.scm | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 6ad6f7799..7ecbccacb 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -5778,6 +5778,28 @@ and @code{Eq} instances. These instances used to li= ve in the haskell-src-meta package, and that's where the version number started.") (license license:bsd-3))) =20 +(define-public ghc-geniplate-mirror + (package + (name "ghc-geniplate-mirror") + (version "0.7.5") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package" + "/geniplate-mirror" + "/geniplate-mirror-" version ".tar.gz")) + (sha256 + (base32 "17vjps2118s5z3k39ij00lkmkxv3mqf8h59wv6qdamlgmhyr36si")))) + (build-system haskell-build-system) + (inputs `(("ghc-mtl" ,ghc-mtl))) + (home-page "https://github.com/danr/geniplate") + (synopsis "Use Template Haskell to generate Uniplate-like functions") + (description + "Use Template Haskell to generate Uniplate-like functions. This is a +maintained mirror of the @uref{https://hackage.haskell.org/package/genipla= te, +geniplate} package, written by Lennart Augustsson.") + (license license:bsd-3))) + (define-public ghc-haskell-src-meta (package (name "ghc-haskell-src-meta") =2D-=20 2.13.4 --=-=-= Content-Type: text/x-diff Content-Disposition: inline; filename=0008-gnu-Add-ghc-gitrev.patch Content-Transfer-Encoding: quoted-printable From=2077f25bfeaec40a4cdb08a053bc41527b2dd6e738 Mon Sep 17 00:00:00 2001 From: Alex Vong Date: Mon, 7 Aug 2017 15:22:00 +0800 Subject: [PATCH 8/8] gnu: Add ghc-gitrev. * gnu/packages/haskell.scm (ghc-gitrev): New variable. =2D-- gnu/packages/haskell.scm | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm index 7ecbccacb..14bc1dddb 100644 =2D-- a/gnu/packages/haskell.scm +++ b/gnu/packages/haskell.scm @@ -5800,6 +5800,28 @@ maintained mirror of the @uref{https://hackage.haske= ll.org/package/geniplate, geniplate} package, written by Lennart Augustsson.") (license license:bsd-3))) =20 +(define-public ghc-gitrev + (package + (name "ghc-gitrev") + (version "1.3.1") + (source + (origin + (method url-fetch) + (uri (string-append "https://hackage.haskell.org/package/gitrev/git= rev-" + version ".tar.gz")) + (sha256 + (base32 "0cl3lfm6k1h8fxp2vxa6ihfp4v8igkz9h35iwyq2frzm4kdn96d8")))) + (build-system haskell-build-system) + (inputs `(("ghc-base-compat" ,ghc-base-compat))) + (home-page "https://github.com/acfoltzer/gitrev") + (synopsis "Compile git revision info into Haskell projects") + (description + "Some handy Template Haskell splices for including the current git ha= sh +and branch in the code of your project. Useful for including in panic +messages, @command{--version} output, or diagnostic info for more informat= ive +bug reports.") + (license license:bsd-3))) + (define-public ghc-haskell-src-meta (package (name "ghc-haskell-src-meta") =2D-=20 2.13.4 --=-=-= Content-Type: text/plain Cheers, Alex --=-=-=-- --==-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdZDkzSn0Cycogr9IxYq4eRf1Ea4FAlmIGAIACgkQxYq4eRf1 Ea7cKhAAtbMmbtXSj4P/zx7hQUlr3cUnNVVUBEw6MFGqb98rhRC+COjl0Btx+Vc6 BoqLXsMmXhDTvCVoHEQL7tfUoWKOTHhDH7TKO+7PEYQ1+cRlllra3O6l4WKVf/re UUHPTBdfCDOz+w53kTTo20IoO1MMfgrkAA34h0uh66X4af/4q46D45CBel6tRnnF i4lw6spWbHpjsiI9pUTcDbsiaBG6f337v0gYbQNqOc4RdjIhOKcNWrHlYx1AIwGU a3+KF/1SjgHfTafbzZ0ME033mic8XBw3oud3shsAXu6dGNSsBobepIFxutUaVoBM TKKAPQcVmfuOSziouefe9BtkVBXrn/SSixMyLXDFjTZxqnvUI/YiDxPd6ouNU5gc nWnvwcblviqv2hfETUM8YFrcohMXYr3NqDaey4E0JE9A2OCZIVcYLVTR4CsXQPl5 N8cxCpIgT8p3o+dmFgO8x7OSpzHx+w/haSDJ+arDwXeb9cXGAzKvWYPh0tnSBlV4 BC34IGNY1aSSqpqY7hMEBdaanLTltDr8B+CYokv0uM8meyTLTZ8E5WDUrqqwA7mc PyG+UtgJYOhJ2tX8J6XHOol55jxP6adTGi22N3Cgqdrr3swRxeyNZEMRj2wfK2NX Qe9XhIkWd1G2GKxh8iBOXjkvNgNcgV4tIrzTc4mSQwgUjhiRVio= =hs4r -----END PGP SIGNATURE----- --==-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Sun Aug 13 10:57:47 2017 Received: (at control) by debbugs.gnu.org; 13 Aug 2017 14:57:47 +0000 Received: from localhost ([127.0.0.1]:59589 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dguKp-0004Ag-HX for submit@debbugs.gnu.org; Sun, 13 Aug 2017 10:57:47 -0400 Received: from mail-pf0-f174.google.com ([209.85.192.174]:34151) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dguKo-0004Aa-8a for control@debbugs.gnu.org; Sun, 13 Aug 2017 10:57:46 -0400 Received: by mail-pf0-f174.google.com with SMTP id o86so32786689pfj.1 for ; Sun, 13 Aug 2017 07:57:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:subject:date:message-id:user-agent:mime-version; bh=AJ1iTo2hzqA8UFPIlEtvsH9YPJOZNoem8TvnZ4MO/dg=; b=KMewv+lC+P1sWSgLcgNX/NBFCZz/NfbW/rlAO992W9zGiVMbQCImJ6HaoFNPDFT3o9 zGP8Q/9VUK11LiGbiHUNR4ekAgWKdP+9QdIamoM/V0vViReFnCgpahOzRkhVJMGVbdCz BGWBTAu393iCn4gUaaJ6TZxRlcn7kGzYUmXxfjdRR6b4Sw3XuYNycBkyiwd090IDdCO9 zoLSj/NOScx2zfvPgS0NN/1wUuQhMNt82Ud1jQTATwVuDEgUaBeXTq3VVawPEfq1XbCQ OJIjEOqo6tf/phDT22f40JbuBsHv4YxuWXMT/2K5hMtUT7m+6yGOffHOQadiRGtBZngq PY3Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:subject:date:message-id:user-agent :mime-version; bh=AJ1iTo2hzqA8UFPIlEtvsH9YPJOZNoem8TvnZ4MO/dg=; b=mvx2x5Y1QEvp35tS3upXEJpk+jHljDP0rPBT6JZpxbom8s6ySbQLOhsU2VMCT0IDGO gFqWsk/YUOpmwxgLhfMa5Wy0elzAVm/X2QEQdIrdhoU+KKM7mvW0nBB3Zlqp6l/JSg3N 1PsDxJujrch246f8BX2GWLe0xH/pKzP1KeJFMMAyem1Az8FAibbEHB48ySu5bvPtiPhu nkEI5PL3nshacEKIip0Lo4tRV2RZZLCZYtAiwAsY2lpImfAGn2qRKfYAM9j7uzSB486u GKuh19sPl7QRJ69kW2vYo8fn6V6hUQ8AKW3E1WK8H+gTrzHeFGZzf/6FcuOW/d/F+Zb3 C1/Q== X-Gm-Message-State: AHYfb5hvMhYqh6CQiLcwnCjqRTaqS/y1t8nbA5XSpphbXckq6YFqw4fd 1yqrRPT3bU+/Bw== X-Received: by 10.98.60.23 with SMTP id j23mr22005977pfa.189.1502636260381; Sun, 13 Aug 2017 07:57:40 -0700 (PDT) Received: from debian (1-36-201-133.static.netvigator.com. [1.36.201.133]) by smtp.gmail.com with ESMTPSA id 67sm9267635pfa.75.2017.08.13.07.57.38 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sun, 13 Aug 2017 07:57:39 -0700 (PDT) From: Alex Vong To: control@debbugs.gnu.org Subject: Add 'patch' tag. Date: Sun, 13 Aug 2017 22:57:28 +0800 Message-ID: <87lgmn1pnr.fsf@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-Spam-Score: -2.5 (--) X-Debbugs-Envelope-To: control X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.5 (--) --=-=-= Content-Type: text/plain package guix-patches tags 27987 patch tags 28077 patch thanks --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdZDkzSn0Cycogr9IxYq4eRf1Ea4FAlmQaNoACgkQxYq4eRf1 Ea7ivxAAm6MbUd8RN4VEK5MMEy/O2O16WHBQs9tEnPUTSOutYNbDDYPTCxi3wMMo DX04Tv5E7hqJs4t1sefZ2PFHzB/yyB2J3q+MBJCgioSwlgRlCnvHh7I/VvUwcLew OvdwUdKCB8DbZWia1z+FqWJhMqzSQhUIeEabq2yVALFeW/KsxDKMf/fP2wXY7h6t gJqubJRE3spl/jKzmba4QyrEw/Ci8Ywt0VtZ2rhlxqQnk5WcZ6nFTX+iM63Y49IE HACaBxUDGB2JxkdJd66N078sHigc8v+8ZYd4eqXNXa6nmC9S20K4b5ONvT8mfZat KTL1VF/m878ntFP15Aey0z0oyaxheq9WYRM0M6DK84WeAUdsD4I6KHvTpCsKm4aI t9YIIiUzY2bG8eqK2b4hzYGMR/JNYxstaUQLKkNzgO1O+QUJHFy16unFG46j/cSI fj6OwFdIUrDHkYHHNrP4TInuh3YM4sbmGOqX2Ksy66oRqZUUmUdeDUX66k4KO9k9 ob7ANlTJxf5AYdOOypFd6waQAwVBhJaH4/Hh2jtQk/qApeXTrobiEJqnuac1QENd yPdJpM++KDTkUyn8ENDUj670k+XbZ87J6nupbpUgoPGdOuei9uRECR2oa744WbuE SjnVR+TgYGZvEkKoLLxC5l2QCEWFpjmZpDvZZ0bFAiBKhacPQek= =vvH+ -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Wed Aug 16 10:55:05 2017 Received: (at 27987) by debbugs.gnu.org; 16 Aug 2017 14:55:05 +0000 Received: from localhost ([127.0.0.1]:41289 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dhziq-00030C-Oa for submit@debbugs.gnu.org; Wed, 16 Aug 2017 10:55:05 -0400 Received: from sender-of-o51.zoho.com ([135.84.80.216]:21019) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dhzio-000304-L3 for 27987@debbugs.gnu.org; Wed, 16 Aug 2017 10:55:03 -0400 Received: from localhost (141.80.247.215 [141.80.247.215]) by mx.zohomail.com with SMTPS id 150289529871094.57927452308616; Wed, 16 Aug 2017 07:54:58 -0700 (PDT) References: <87efsoofo9.fsf@gmail.com> User-agent: mu4e 0.9.18; emacs 25.2.1 From: Ricardo Wurmus To: Alex Vong Subject: Re: [bug#27987] Dependencies for Agda - a dependently typed functional language In-reply-to: <87efsoofo9.fsf@gmail.com> X-URL: https://elephly.net X-PGP-Key: https://elephly.net/rekado.pubkey X-PGP-Fingerprint: BCA6 89B6 3655 3801 C3C6 2150 197A 5888 235F ACAC Date: Wed, 16 Aug 2017 16:54:56 +0200 Message-ID: <87efsbk1fj.fsf@elephly.net> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-ZohoMailClient: External X-Spam-Score: 1.0 (+) X-Debbugs-Envelope-To: 27987 Cc: 27987@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 1.0 (+) Hi Alex, > I wish to introduce Agda to Guix. The patches below are some dependecies > for Agda. There are more to come... Thank you. I have changed the descriptions, ran “guix lint” and pushed the patches from this email with commit 96f23b62e to master. -- Ricardo GPG: BCA6 89B6 3655 3801 C3C6 2150 197A 5888 235F ACAC https://elephly.net From debbugs-submit-bounces@debbugs.gnu.org Wed Aug 16 11:08:42 2017 Received: (at 27987-done) by debbugs.gnu.org; 16 Aug 2017 15:08:42 +0000 Received: from localhost ([127.0.0.1]:41309 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dhzw2-0003Lj-Dd for submit@debbugs.gnu.org; Wed, 16 Aug 2017 11:08:42 -0400 Received: from sender-of-o51.zoho.com ([135.84.80.216]:21045) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dhzw0-0003LZ-Ek for 27987-done@debbugs.gnu.org; Wed, 16 Aug 2017 11:08:40 -0400 Received: from localhost (141.80.247.215 [141.80.247.215]) by mx.zohomail.com with SMTPS id 1502896116146154.38044421615484; Wed, 16 Aug 2017 08:08:36 -0700 (PDT) References: <87efsoofo9.fsf@gmail.com> <87valzde65.fsf@gmail.com> User-agent: mu4e 0.9.18; emacs 25.2.1 From: Ricardo Wurmus To: Alex Vong Subject: Re: [bug#27987] Dependencies for Agda - a dependently typed functional language In-reply-to: <87valzde65.fsf@gmail.com> X-URL: https://elephly.net X-PGP-Key: https://elephly.net/rekado.pubkey X-PGP-Fingerprint: BCA6 89B6 3655 3801 C3C6 2150 197A 5888 235F ACAC Date: Wed, 16 Aug 2017 17:08:33 +0200 Message-ID: <87d17vk0su.fsf@elephly.net> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-ZohoMailClient: External X-Spam-Score: 1.0 (+) X-Debbugs-Envelope-To: 27987-done Cc: 27987-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 1.0 (+) Hi Alex, > Here is the remaining dependencies for Agda. Actually I have already > managed to get Agda to build, but I still need to figure out how to > build the standard library. Thank you. I’ve pushed the patches to master af4db693d after slight changes to the descriptions. -- Ricardo GPG: BCA6 89B6 3655 3801 C3C6 2150 197A 5888 235F ACAC https://elephly.net From debbugs-submit-bounces@debbugs.gnu.org Wed Aug 16 20:40:54 2017 Received: (at 27987-done) by debbugs.gnu.org; 17 Aug 2017 00:40:54 +0000 Received: from localhost ([127.0.0.1]:41737 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1di8rl-0000n5-Ps for submit@debbugs.gnu.org; Wed, 16 Aug 2017 20:40:53 -0400 Received: from mail-pg0-f53.google.com ([74.125.83.53]:36612) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1di8rj-0000ms-Sz for 27987-done@debbugs.gnu.org; Wed, 16 Aug 2017 20:40:52 -0400 Received: by mail-pg0-f53.google.com with SMTP id i12so31484884pgr.3 for <27987-done@debbugs.gnu.org>; Wed, 16 Aug 2017 17:40:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=LrqQfUpAWXDjHlI2QCjOug1Mp8MHGaDu0ar4TDagMEc=; b=rMq9yYKchUPH2t60cSkwq7/EV4oe/30fGCb7zRbzDoOdytUdYZPsCkho5coUHbH8Vc glNSGFZIy23iqUUnvwradH8CGc7UsCTwMuEmmZv0sRk5Xob3E448K20T4pH9A+adWWuP OIwRBlaeuQkE0eG00rlw4mqo4EfsVFoSOAE/SPht9lNb29uioMKEMoTQ5MHnjsdM7kW8 3ui70+LMqaElg8HWPhxOyMwebIs9KurF7LL/+RWlFKQA8pME4/8gnzoT181nJGhthgQk IP1qufsLYKznoTFzjw4dQoA9kD939doa29z7qcDKQ88IFay679v7uZwpPvRzMLHy2Y5l +kQA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=LrqQfUpAWXDjHlI2QCjOug1Mp8MHGaDu0ar4TDagMEc=; b=RJl2dDo2RbyASv6KMqoPzp31beaAFKv3KF7kT0w0h/YhXBbzNgxFdQIArfLgz6GnDk adlX/6R/IBOQbjzNo/YOYJFRkSqBIEon8E0yLwSuFsJBnMc4tnADKuLKOC+m5akW/vgn 3CF7CjzU8sbMARDdU8wpBPy59Wwhiqjk9wzTvllbqa9+UrV7g7UgzzkrAdm8x6kSr3b5 ekKZKv2BZX8GUD7SSq70XHvU+h5zR7BTjzQ5kUzfcSHKktI8t5Bwux1027qB5bn61yua PaKSN6HscqBlc0nGIopnvi1d34s+liYKDdUI23cIFMXtDE8tpP0jLiwwhsJjdT2kKqXz uJfg== X-Gm-Message-State: AHYfb5htvJ+KrZaGgqfjbm7yYHURFS/xIsUOZ8xUnCp1zhn6XA5DWeXZ WBVeqGligKIz5w== X-Received: by 10.84.176.195 with SMTP id v61mr3687264plb.271.1502930446068; Wed, 16 Aug 2017 17:40:46 -0700 (PDT) Received: from debian (1-64-80-130.static.netvigator.com. [1.64.80.130]) by smtp.gmail.com with ESMTPSA id r13sm4066239pfg.14.2017.08.16.17.40.43 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Wed, 16 Aug 2017 17:40:44 -0700 (PDT) From: Alex Vong To: Ricardo Wurmus Subject: Re: [bug#27987] Dependencies for Agda - a dependently typed functional language References: <87efsoofo9.fsf@gmail.com> <87valzde65.fsf@gmail.com> <87d17vk0su.fsf@elephly.net> Date: Thu, 17 Aug 2017 08:40:42 +0800 In-Reply-To: <87d17vk0su.fsf@elephly.net> (Ricardo Wurmus's message of "Wed, 16 Aug 2017 17:08:33 +0200") Message-ID: <87pobvowl1.fsf@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-Spam-Score: 0.7 (/) X-Debbugs-Envelope-To: 27987-done Cc: 27987-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.7 (/) --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Ricardo Wurmus writes: > Hi Alex, > >> Here is the remaining dependencies for Agda. Actually I have already >> managed to get Agda to build, but I still need to figure out how to >> build the standard library. > > Thank you. I=E2=80=99ve pushed the patches to master af4db693d after sli= ght > changes to the descriptions. Thanks of taking care of it. I tried to change some haddock markup to texinfo notation, but I am new to both :) --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdZDkzSn0Cycogr9IxYq4eRf1Ea4FAlmU5goACgkQxYq4eRf1 Ea4DSQ//UMVm544N2BaQUs89piS2V3gaDZWO50f89g+2OEMgSmxPLjx6sdDY8Xwg Uh/EzIEeObJ7SSkjr17mT/NZA1VnDBPFSvrhEljmKEe5rgw/exNk/gUST+38AR8Q 7oJi3Owt0lVXKBfcBkQkNhQmmODRBJpZEqqAglnpvmlSCtdDbb5ujLdVPEaIffs3 5tRLubNF1OJpy702ybdDmJPevu3ZEIFRLjztvF8xm1Q8Qey8DYIJUWTMCPbolNM5 R9LwaoQVCfYfNgENvyBT6qTTvkDpg8JWAaOKvlfeYWeCkVoEzn7G1t0Ie4rhqHGJ W+oJCuUUGwX6+n4UavF+syfQkBfiworXvmRhNHCnVEgSskQngPns+AoRR4nYmneJ GAfRUtD5evv5YiEDL4Totw84SZW58gVLqrovMRVbvdjoRfTNFdm43BKEKlAUoTc/ +4VE2rybPQZo1WzzDrXQChbZkFkIp5S4Gsho8czTU0E/67L0EyWknJt+5vGtHa7l uPskKQxJLg19I8Y0MDQ4FUW4NYKgFiWFsdycTOJwiOjjG+9Jhd8uP1sgZWka6SwV tQraAG94oPKlRlAQJRfwNq9hyniPlvNywNtc4t6a9rFcYBQiLAetbtkIXQNqm8k9 siBc0tqbbIHkI6I+Mbc4AXdmf2lzYTBXQbNAqT0RF5tysDzGCf4= =sSpB -----END PGP SIGNATURE----- --=-=-=-- From unknown Mon Jun 23 07:49:45 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Thu, 14 Sep 2017 11:24:06 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator