;;; 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.2")
+ (version "2.6.0.1")
(source
(origin
(method url-fetch)
version ".tar.gz"))
(sha256
(base32
- "07wvawpfjhx3gw2w53v27ncv1bl0kkx08wkm6wzxldbslkcasign"))))
+ "1s600ry1qwizr3ynyj05rvlx7jdcw9a1viyc0ycjamm5sjf8mf3v"))))
(build-system haskell-build-system)
(inputs
- `(("ghc-alex" ,ghc-alex)
+ `(("ghc-aeson" ,ghc-aeson)
+ ("ghc-alex" ,ghc-alex)
("ghc-async" ,ghc-async)
("ghc-blaze-html" ,ghc-blaze-html)
("ghc-boxes" ,ghc-boxes)
("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-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-strict" ,ghc-strict)
("ghc-unordered-containers" ,ghc-unordered-containers)
(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
#: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)))
+ (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)
(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