From 276f598abc12eaae01fbea0c0bbba577a93bcbdb Mon Sep 17 00:00:00 2001
From: John Soo <jsoo1@asu.edu>
Date: Mon, 12 Aug 2019 08:33:36 -0700
Subject: [PATCH] gnu: Add agda-ial.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* gnu/packages/agda.scm (agda-ial): new variable.

Signed-off-by: Ludovic Courtès <ludo@gnu.org>
---
 gnu/packages/agda.scm | 48 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

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)))