;;; GNU Guix --- Functional package management for GNU
;;; 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.3")
+ (version "2.6.0.1")
(source
(origin
(method url-fetch)
version ".tar.gz"))
(sha256
(base32
- "0r80vw7vnvbgq47y50v050malv7zvv2p2kg6f47i04r0b2ix855a"))))
+ "1s600ry1qwizr3ynyj05rvlx7jdcw9a1viyc0ycjamm5sjf8mf3v"))))
(build-system haskell-build-system)
(inputs
- `(("cpphs" ,cpphs)
+ `(("ghc-aeson" ,ghc-aeson)
("ghc-alex" ,ghc-alex)
("ghc-async" ,ghc-async)
("ghc-blaze-html" ,ghc-blaze-html)
("ghc-edisoncore" ,ghc-edisoncore)
("ghc-edit-distance" ,ghc-edit-distance)
("ghc-equivalence" ,ghc-equivalence)
+ ("ghc-exceptions" ,ghc-exceptions)
+ ("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-monadplus" ,ghc-monadplus)
- ("ghc-mtl" ,ghc-mtl)
("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)))
(arguments
`(#:modules ((guix build haskell-build-system)
(guix build utils)
- (srfi srfi-26))
+ (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"))
+ #t))
+ ;; 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))
+ (ghc-path (getenv "GHC_PACKAGE_PATH"))
+ (params
+ `(,(string-append "--prefix=" out)
+ ,(string-append "--libdir=" out "/lib")
+ ,(string-append "--docdir=" out
+ "/share/doc/" name-version)
+ "--libsubdir=$compiler/$pkg-$version"
+ "--package-db=../package.conf.d"
+ "--global"
+ ,@(if tests?
+ '("--enable-tests")
+ '())
+ ;; Build and link with shared libraries
+ "--enable-shared"
+ "--enable-executable-dynamic"
+ "--ghc-option=-fPIC"
+ ,(string-append "--ghc-option=-optl=-Wl,-rpath=" out
+ "/lib/$compiler/$pkg-$version")
+ ,@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"))
(for-each (cut invoke agda-compiler <>)
(find-files (string-append out "/share") "\\.agda$"))
#t))))))
- (home-page "http://wiki.portal.chalmers.se/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
+ `(("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)))
HCoop / jackhill / guix / guix.git / blobdiff