;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
;;; 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>
+;;; Copyright © 2019 Ludovic Courtès <ludo@gnu.org>
;;;
;;; This file is part of GNU Guix.
;;;
;;; 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 (gnu packages haskell-xyz)
#: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)
+ #:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
#:use-module (guix packages))
(define-public agda
(package
(name "agda")
- (version "2.5.4.1")
+ (version "2.5.4.2")
(source
(origin
(method url-fetch)
version ".tar.gz"))
(sha256
(base32
- "0bxpibsk98n9xp42d92ma5vj2fam8rsnl61fbhr3askfjdvalnbp"))))
+ "07wvawpfjhx3gw2w53v27ncv1bl0kkx08wkm6wzxldbslkcasign"))))
(build-system haskell-build-system)
(inputs
- `(("cpphs" ,cpphs)
- ("ghc-alex" ,ghc-alex)
+ `(("ghc-alex" ,ghc-alex)
("ghc-async" ,ghc-async)
("ghc-blaze-html" ,ghc-blaze-html)
("ghc-boxes" ,ghc-boxes)
("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)))
(arguments
(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")
+ (home-page "https://github.com/cedille/ial")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference (url home-page)
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0dlis6v6nzbscf713cmwlx8h9n2gxghci8y21qak3hp18gkxdp0g"))))
+ (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)
+ (let* ((out (assoc-ref outputs "out"))
+ (include (string-append out "/include/agda/ial")))
+ (for-each (lambda (file)
+ (make-file-writable file)
+ (install-file file include))
+ (find-files "." "\\.agdai?(-lib)?$"))
+ #t))))))
+ (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)))