summaryrefslogtreecommitdiff
path: root/gnu/packages/agda.scm
diff options
context:
space:
mode:
authorJohn Soo <jsoo1@asu.edu>2019-08-12 08:33:36 -0700
committerLudovic Courtès <ludo@gnu.org>2019-08-28 00:27:14 +0200
commit276f598abc12eaae01fbea0c0bbba577a93bcbdb (patch)
tree069a58be3ed10b09ab0b7fa801966a50a8ca3149 /gnu/packages/agda.scm
parent58d5f280a36e1cfddfa999d320c285726d8a8bc1 (diff)
gnu: Add agda-ial.
* gnu/packages/agda.scm (agda-ial): new variable. Signed-off-by: Ludovic Courtès <ludo@gnu.org>
Diffstat (limited to 'gnu/packages/agda.scm')
-rw-r--r--gnu/packages/agda.scm48
1 files changed, 48 insertions, 0 deletions
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 0f9b4299c3..8840790058 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -3,6 +3,7 @@
;;; Copyright © 2018 Ricardo Wurmus <rekado@elephly.net>
;;; Copyright © 2018 Alex Vong <alexvong1995@gmail.com>
;;; Copyright © 2018 Tobias Geerinckx-Rice <me@tobias.gr>
+;;; Copyright © 2018 John Soo <jsoo1@asu.edu>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -24,6 +25,7 @@
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (guix build-system emacs)
+ #:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix build-system trivial)
#:use-module (guix download)
@@ -154,3 +156,49 @@ such as Coq, Epigram and NuPRL.")
(synopsis "Emacs mode for Agda")
(description "This Emacs mode enables interactive development with
Agda. It also aids the input of Unicode characters.")))
+
+(define-public agda-ial
+ (package
+ (name "agda-ial")
+ (version "1.5.0")
+ (source
+ (origin
+ (method url-fetch)
+ (uri (string-append
+ "https://github.com/cedille/ial/archive/v"
+ version ".tar.gz"))
+ (file-name (string-append name "-" version))
+ (sha256
+ (base32
+ "0ilgalmx3kljy6j9i8d7w6r7ky4bq0xzxanwfr6kyx56mf2sf0zh"))))
+ (build-system gnu-build-system)
+ (inputs
+ `(("agda" ,agda)))
+ (arguments
+ `(#:parallel-build? #f
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'configure)
+ (add-before 'build 'patch-dependencies
+ (lambda _ (patch-shebang "find-deps.sh") #t))
+ (delete 'check)
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (for-each
+ (lambda (file)
+ (install-file
+ file
+ (string-append
+ (assoc-ref outputs "out") "/include/agda/ial")))
+ (find-files "." ".*agda.*"))
+ #t)))))
+ (home-page "https://github.com/cedille/ial")
+ (synopsis
+ "The Iowa Agda Library")
+ (description
+ "The goal is to provide a concrete library focused on verification
+examples, as opposed to mathematics. The library has a good number
+of theorems for booleans, natural numbers, and lists. It also has
+trees, tries, vectors, and rudimentary IO. A number of good ideas
+come from Agda's standard library.")
+ (license license:expat)))