GNU bug report logs - #30563
[PATCH] add Agda.

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 30563 in the body.
You can then email your comments to 30563 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Alex ter Weele <alex.ter.weele <at> gmail.com>
To: guix-patches <at> gnu.org
Subject: [PATCH] add Agda.
Date: Tue, 20 Feb 2018 19:23:06 -0600

Hello,

The following patch series fixes a few ghc- packages, adds another, and
finally adds Agda. Following the example of Idris, I've placed it in its
own file.

I have not yet packaged the Emacs mode for Agda. That's next!

Message #8 received at 30563 <at> debbugs.gnu.org (full text, mbox):

From: Alex ter Weele <alex.ter.weele <at> gmail.com>
To: bug#30563 <30563 <at> debbugs.gnu.org>
Subject: Re: Status: [PATCH] add Agda.
Date: Tue, 20 Feb 2018 19:36:41 -0600

[0001-gnu-ghc-edit-distance-Allow-newer-version-of-QuickCh.patch (text/x-patch, inline)]

From b107451e58413a1a86fc4fb7a5a9b650f234f73c Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele <at> gmail.com>
Date: Tue, 20 Feb 2018 18:49:41 -0600
Subject: [PATCH 1/4] gnu: ghc-edit-distance: Allow newer version of
 QuickCheck.

* gnu/packages/haskell.scm (ghc-edit-distance)[arguments]: Allow running tests
  with newer version of QuickCheck.
---
 gnu/packages/haskell.scm | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm
index e62c405ab..737b7a4cd 100644
--- a/gnu/packages/haskell.scm
+++ b/gnu/packages/haskell.scm
@@ -5755,6 +5755,8 @@ representations of current time.")
        (sha256
         (base32 "0jkca97zyv23yyilp3jydcrzxqhyk27swhzh82llvban5zp8b21y"))))
     (build-system haskell-build-system)
+    (arguments
+     `(#:configure-flags (list "--allow-newer=QuickCheck")))
     (inputs
      `(("ghc-random" ,ghc-random)
        ("ghc-test-framework" ,ghc-test-framework)
-- 
2.16.1

Message #11 received at 30563 <at> debbugs.gnu.org (full text, mbox):

From: Alex ter Weele <alex.ter.weele <at> gmail.com>
To: bug#30563 <30563 <at> debbugs.gnu.org>
Subject: Re: Status: [PATCH] add Agda.
Date: Tue, 20 Feb 2018 19:44:00 -0600

[0002-gnu-ghc-hashtables-Allow-newer-version-of-vector.patch (text/x-patch, inline)]

From 4e20edfb690f8d2f7d0652058d8fcff5927102a2 Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele <at> gmail.com>
Date: Tue, 20 Feb 2018 18:51:16 -0600
Subject: [PATCH 2/4] gnu: ghc-hashtables: Allow newer version of vector.

* gnu/packages/haskell.scm (ghc-hashtables)[arguments]: Allow newer version of
  vector.
---
 gnu/packages/haskell.scm | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/gnu/packages/haskell.scm b/gnu/packages/haskell.scm
index 737b7a4cd..dbb9ebc80 100644
--- a/gnu/packages/haskell.scm
+++ b/gnu/packages/haskell.scm
@@ -7360,6 +7360,8 @@ Haskell, using gnuplot for rendering.")
        (sha256
         (base32 "1b6w9xznk42732vpd8ili60k12yq190xnajgga0iwbdpyg424lgg"))))
     (build-system haskell-build-system)
+    (arguments
+     `(#:configure-flags (list "--allow-newer=vector")))
     (inputs
      `(("ghc-hashable" ,ghc-hashable)
        ("ghc-primitive" ,ghc-primitive)
-- 
2.16.1

Message #14 received at 30563 <at> debbugs.gnu.org (full text, mbox):

From: Alex ter Weele <alex.ter.weele <at> gmail.com>
To: bug#30563 <30563 <at> debbugs.gnu.org>
Subject: Re: Status: [PATCH] add Agda.
Date: Tue, 20 Feb 2018 19:44:26 -0600

[0003-gnu-Add-ghc-uri-encode.patch (text/x-patch, inline)]

From 33a25f9a810b791099b89811a65590c62d6167be Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele <at> gmail.com>
Date: Tue, 20 Feb 2018 18:53:26 -0600
Subject: [PATCH 3/4] gnu: Add ghc-uri-encode.

* gnu/packages/haskell-web.scm (ghc-uri-encode): New variable.
---
 gnu/packages/haskell-web.scm | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/gnu/packages/haskell-web.scm b/gnu/packages/haskell-web.scm
index a24ee4b7c..aec69deb1 100644
--- a/gnu/packages/haskell-web.scm
+++ b/gnu/packages/haskell-web.scm
@@ -866,3 +866,28 @@ of a JSON value into a @code{Data.Aeson.Value}.")
     (description
      "HTTP multipart split out of the cgi package, for Haskell.")
     (license license:bsd-3)))
+
+(define-public ghc-uri-encode
+  (package
+    (name "ghc-uri-encode")
+    (version "1.5.0.5")
+    (source
+     (origin
+       (method url-fetch)
+       (uri (string-append
+             "https://hackage.haskell.org/package/uri-encode/uri-encode-"
+             version
+             ".tar.gz"))
+       (sha256
+        (base32
+         "11miwb5vvnn17m92ykz1pzg9x6s8fbpz3mmsyqs2s4b3mn55haz8"))))
+    (build-system haskell-build-system)
+    (inputs
+     `(("ghc-text" ,ghc-text)
+       ("ghc-utf8-string" ,ghc-utf8-string)
+       ("ghc-network-uri" ,ghc-network-uri)))
+    (home-page
+     "http://hackage.haskell.org/package/uri-encode")
+    (synopsis "Unicode aware uri-encoding")
+    (description "Unicode aware uri-encoding.")
+    (license license:bsd-3)))
-- 
2.16.1

Message #17 received at 30563 <at> debbugs.gnu.org (full text, mbox):

From: Alex ter Weele <alex.ter.weele <at> gmail.com>
To: bug#30563 <30563 <at> debbugs.gnu.org>
Subject: Re: Status: [PATCH] add Agda.
Date: Tue, 20 Feb 2018 19:44:39 -0600

[0004-gnu-Add-agda.patch (text/x-patch, inline)]

From 4d0f3020ee8c9430272fd78dbb970ec38978c4a8 Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele <at> gmail.com>
Date: Tue, 20 Feb 2018 18:55:06 -0600
Subject: [PATCH 4/4] gnu: Add agda.

* gnu/packages/agda.scm: New file.
* gnu/local.mk (GNU_SYSTEM_MODULES): Add adga.scm.
---
 gnu/local.mk          |  1 +
 gnu/packages/agda.scm | 86 +++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 87 insertions(+)
 create mode 100644 gnu/packages/agda.scm

diff --git a/gnu/local.mk b/gnu/local.mk
index e61cb9f44..eb044989e 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -52,6 +52,7 @@ GNU_SYSTEM_MODULES =				\
   %D%/packages/acl.scm				\
   %D%/packages/admin.scm			\
   %D%/packages/adns.scm				\
+  %D%/packages/agda.scm				\
   %D%/packages/algebra.scm			\
   %D%/packages/aidc.scm				\
   %D%/packages/android.scm			\
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
new file mode 100644
index 000000000..42a7d56db
--- /dev/null
+++ b/gnu/packages/agda.scm
@@ -0,0 +1,86 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2018 Alex ter Weele <alex.ter.weele <at> gmail.com>
+;;;
+;;; This file is part of GNU Guix.
+;;;
+;;; GNU Guix is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or (at
+;;; your option) any later version.
+;;;
+;;; GNU Guix is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;;; GNU General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (gnu packages agda)
+  #:use-module (gnu packages haskell)
+  #:use-module (gnu packages haskell-check)
+  #:use-module (gnu packages haskell-web)
+  #:use-module (guix build-system haskell)
+  #:use-module (guix build-system trivial)
+  #:use-module (guix download)
+  #:use-module ((guix licenses) #:prefix license:)
+  #:use-module (guix packages))
+
+(define-public agda
+  (package
+    (name "agda")
+    (version "2.5.3")
+    (source
+     (origin
+       (method url-fetch)
+       (uri (string-append
+             "https://hackage.haskell.org/package/Agda/Agda-"
+             version
+             ".tar.gz"))
+       (sha256
+        (base32
+         "0r80vw7vnvbgq47y50v050malv7zvv2p2kg6f47i04r0b2ix855a"))))
+    (build-system haskell-build-system)
+    (inputs
+     `(("cpphs" ,cpphs)
+       ("ghc-alex" ,ghc-alex)
+       ("ghc-async" ,ghc-async)
+       ("ghc-blaze-html" ,ghc-blaze-html)
+       ("ghc-boxes" ,ghc-boxes)
+       ("ghc-data-hash" ,ghc-data-hash)
+       ("ghc-edisoncore" ,ghc-edisoncore)
+       ("ghc-edit-distance" ,ghc-edit-distance)
+       ("ghc-equivalence" ,ghc-equivalence)
+       ("ghc-geniplate-mirror" ,ghc-geniplate-mirror)
+       ("ghc-gitrev" ,ghc-gitrev)
+       ("ghc-happy" ,ghc-happy)
+       ("ghc-hashable" ,ghc-hashable)
+       ("ghc-hashtables" ,ghc-hashtables)
+       ("ghc-ieee754" ,ghc-ieee754)
+       ("ghc-monadplus" ,ghc-monadplus)
+       ("ghc-mtl" ,ghc-mtl)
+       ("ghc-murmur-hash" ,ghc-murmur-hash)
+       ("ghc-uri-encode" ,ghc-uri-encode)
+       ("ghc-parallel" ,ghc-parallel)
+       ("ghc-regex-tdfa" ,ghc-regex-tdfa)
+       ("ghc-stm" ,ghc-stm)
+       ("ghc-strict" ,ghc-strict)
+       ("ghc-text" ,ghc-text)
+       ("ghc-unordered-containers" ,ghc-unordered-containers)
+       ("ghc-zlib" ,ghc-zlib)))
+    (home-page
+     "http://wiki.portal.chalmers.se/agda/")
+    (synopsis
+     "Dependently typed functional programming language and proof assistant")
+    (description
+     "Agda is a dependently typed functional programming language: It has
+inductive families, which are similar to Haskell's GADTs, but they can be
+indexed by values and not just types.  It also has parameterised modules,
+mixfix operators, Unicode characters, and an interactive Emacs interface (the
+type checker can assist in the development of your code).  Agda is also a
+proof assistant: It is an interactive system for writing and checking proofs.
+Agda is based on intuitionistic type theory, a foundational system for
+constructive mathematics developed by the Swedish logician Per Martin-Löf.  It
+has many similarities with other proof assistants based on dependent types,
+such as Coq, Epigram and NuPRL.")
+    (license (list license:expat license:bsd-3))))
-- 
2.16.1

Message #22 received at 30563-done <at> debbugs.gnu.org (full text, mbox):

From: Marius Bakke <mbakke <at> fastmail.com>
To: Alex ter Weele <alex.ter.weele <at> gmail.com>, 30563-done <at> debbugs.gnu.org
Subject: Re: [bug#30563] [PATCH] add Agda.
Date: Mon, 26 Feb 2018 01:46:52 +0100

[Message part 1 (text/plain, inline)]

Alex ter Weele <alex.ter.weele <at> gmail.com> writes:

> Hello,
>
> The following patch series fixes a few ghc- packages, adds another, and
> finally adds Agda. Following the example of Idris, I've placed it in its
> own file.

Thank you!  I added a comment about the Agda licenses and pushed the
series as acc55e836..f61682e7e.

> I have not yet packaged the Emacs mode for Agda. That's next!

:-)

[signature.asc (application/pgp-signature, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.