03/04: gnu: Add agda-ial.

[guix-commits]

civodul pushed a commit to branch master
in repository guix.

commit 276f598abc12eaae01fbea0c0bbba577a93bcbdb
Author: John Soo <address@hidden>
Date:   Mon Aug 12 08:33:36 2019 -0700

    gnu: Add agda-ial.
    
    * gnu/packages/agda.scm (agda-ial): new variable.
    
    Signed-off-by: Ludovic Courtès <address@hidden>
---
 gnu/packages/agda.scm | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 0f9b429..8840790 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -3,6 +3,7 @@
 ;;; Copyright © 2018 Ricardo Wurmus <address@hidden>
 ;;; Copyright © 2018 Alex Vong <address@hidden>
 ;;; Copyright © 2018 Tobias Geerinckx-Rice <address@hidden>
+;;; Copyright © 2018 John Soo <address@hidden>
 ;;;
 ;;; 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)))