;;; 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, 2022 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 gexp)
#: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.6.2.2")
(source
(origin
(method url-fetch)
"https://hackage.haskell.org/package/Agda/Agda-"
version ".tar.gz"))
(sha256
- (base32
- "0bxpibsk98n9xp42d92ma5vj2fam8rsnl61fbhr3askfjdvalnbp"))))
+ (base32 "0yjjbhc593ylrm4mq4j01nkdvh7xqsg5in30wxj4y53vf5hkggp5"))))
(build-system haskell-build-system)
(inputs
- `(("cpphs" ,cpphs)
- ("ghc-alex" ,ghc-alex)
- ("ghc-async" ,ghc-async)
- ("ghc-blaze-html" ,ghc-blaze-html)
- ("ghc-boxes" ,ghc-boxes)
- ("ghc-data-hash" ,ghc-data-hash)
- ("ghc-edisoncore" ,ghc-edisoncore)
- ("ghc-edit-distance" ,ghc-edit-distance)
- ("ghc-equivalence" ,ghc-equivalence)
- ("ghc-filemanip" ,ghc-filemanip)
- ("ghc-geniplate-mirror" ,ghc-geniplate-mirror)
- ("ghc-gitrev" ,ghc-gitrev)
- ("ghc-happy" ,ghc-happy)
- ("ghc-hashable" ,ghc-hashable)
- ("ghc-hashtables" ,ghc-hashtables)
- ("ghc-ieee754" ,ghc-ieee754)
- ("ghc-murmur-hash" ,ghc-murmur-hash)
- ("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)))
+ (list ghc-aeson
+ ghc-alex
+ ghc-async
+ ghc-blaze-html
+ ghc-boxes
+ ghc-case-insensitive
+ ghc-data-hash
+ ghc-edit-distance
+ ghc-equivalence
+ ghc-gitrev
+ ghc-happy
+ ghc-hashable
+ ghc-hashtables
+ ghc-monad-control
+ ghc-murmur-hash
+ ghc-parallel
+ ghc-regex-tdfa
+ ghc-split
+ ghc-strict
+ ghc-unordered-containers
+ ghc-uri-encode
+ ghc-zlib))
(arguments
- `(#:modules ((guix build haskell-build-system)
- (guix build utils)
- (srfi srfi-26)
- (ice-9 match))
- #:phases
- (modify-phases %standard-phases
- ;; FIXME: This is a copy of the standard configure phase with a tiny
- ;; difference: this package needs the -package-db flag to be passed
- ;; to "runhaskell" in addition to the "configure" action, because
- ;; Setup.hs depends on filemanip. Without this option the Setup.hs
- ;; file cannot be evaluated. The haskell-build-system should be
- ;; changed to pass "-package-db" to "runhaskell" in any case.
- (replace 'configure
- (lambda* (#:key outputs inputs tests? (configure-flags '())
- #:allow-other-keys)
- (let* ((out (assoc-ref outputs "out"))
- (name-version (strip-store-file-name out))
- (input-dirs (match inputs
- (((_ . dir) ...)
- dir)
- (_ '())))
- (ghc-path (getenv "GHC_PACKAGE_PATH"))
- (params (append `(,(string-append "--prefix=" out))
- `(,(string-append "--libdir=" out "/lib"))
- `(,(string-append "--bindir=" out "/bin"))
- `(,(string-append
- "--docdir=" out
- "/share/doc/" name-version))
- '("--libsubdir=$compiler/$pkg-$version")
- '("--package-db=../package.conf.d")
- '("--global")
- `(,@(map
- (cut string-append "--extra-include-dirs=" <>)
- (search-path-as-list '("include") input-dirs)))
- `(,@(map
- (cut string-append "--extra-lib-dirs=" <>)
- (search-path-as-list '("lib") input-dirs)))
- (if tests?
- '("--enable-tests")
- '())
- configure-flags)))
- (unsetenv "GHC_PACKAGE_PATH")
- (apply invoke "runhaskell" "-package-db=../package.conf.d"
- "Setup.hs" "configure" params)
- (setenv "GHC_PACKAGE_PATH" ghc-path)
- #t)))
- (add-after 'compile 'agda-compile
- (lambda* (#:key outputs #:allow-other-keys)
- (let* ((out (assoc-ref outputs "out"))
- (agda-compiler (string-append out "/bin/agda")))
- (for-each (cut invoke agda-compiler <>)
- (find-files (string-append out "/share") "\\.agda$"))
- #t))))))
- (home-page "http://wiki.portal.chalmers.se/agda/")
+ (list #:modules `((guix build haskell-build-system)
+ (guix build utils)
+ (srfi srfi-26)
+ (ice-9 match))
+ #:phases
+ #~(modify-phases %standard-phases
+ ;; This allows us to call the 'agda' binary before installing.
+ (add-after 'unpack 'set-ld-library-path
+ (lambda _
+ (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build"))))
+ (add-after 'compile 'agda-compile
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((agda-compiler (string-append #$output "/bin/agda")))
+ (for-each (cut invoke agda-compiler <>)
+ (find-files (string-append #$output "/share")
+ "\\.agda$"))))))))
+ (home-page "https://wiki.portal.chalmers.se/agda/")
(synopsis
"Dependently typed functional programming language and proof assistant")
(description
(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
+ (list 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)))
HCoop / jackhill / guix / guix.git / blobdiff