diff options
Diffstat (limited to 'gnu/packages')
| -rw-r--r-- | gnu/packages/agda.scm | 48 |
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))) |