summaryrefslogtreecommitdiff
path: root/gnu/packages/agda.scm
diff options
context:
space:
mode:
authorJosselin Poiret <dev@jpoiret.xyz>2023-06-04 10:46:26 +0200
committerJosselin Poiret <dev@jpoiret.xyz>2023-06-04 11:04:54 +0200
commite198fe4e942c58136dd4cb8ebf49cade58a8f5e3 (patch)
treef3a9ad383660e987c225685f4d899e2bbf5965d4 /gnu/packages/agda.scm
parent067e75e17a7f2c278eb6273824e33454d8e00566 (diff)
gnu: agda-ial: Update to ded30c410d5d40142249686572aa1acd1b2f8cc7.
* gnu/packages/agda.scm (agda-ial): Update to ded30c410d5d40142249686572aa1acd1b2f8cc7, use agda-build-system, switch to G-Exps, reorder fields.
Diffstat (limited to 'gnu/packages/agda.scm')
-rw-r--r--gnu/packages/agda.scm65
1 files changed, 30 insertions, 35 deletions
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index bd7fe29f1e..88626b823c 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -155,46 +155,41 @@ Agda. It also aids the input of Unicode characters.")
(license (package-license agda))))
(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
+ (let ((revision "1")
+ ;; There hasn't been a release in a long time, and the last one
+ ;; doesn't build with Agda 2.6.
+ (commit "ded30c410d5d40142249686572aa1acd1b2f8cc7"))
+ (package
+ (name "agda-ial")
+ (version (git-version "1.5.0" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference (url "https://github.com/cedille/ial")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0xn6zvp1wnm0i84pz1rfbzfmayd15ch4i5s11ycd88d22pxd55dc"))))
+ (build-system agda-build-system)
+ (arguments
+ (list
+ #:gnu-and-haskell? #t
#: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
+ #~(modify-phases %standard-phases
+ (add-before 'build 'patch-dependencies
+ (lambda _ (patch-shebang "find-deps.sh")))
+ (replace 'build
+ (lambda _
+ (invoke "make"))))))
+ (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)))
+ (license license:expat))))
(define-public agda-stdlib
(package