From 276f598abc12eaae01fbea0c0bbba577a93bcbdb Mon Sep 17 00:00:00 2001 From: John Soo Date: Mon, 12 Aug 2019 08:33:36 -0700 Subject: gnu: Add agda-ial. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/agda.scm (agda-ial): new variable. Signed-off-by: Ludovic Courtès --- gnu/packages/agda.scm | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) (limited to 'gnu/packages/agda.scm') diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 0f9b4299c3..8840790058 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -3,6 +3,7 @@ ;;; Copyright © 2018 Ricardo Wurmus ;;; Copyright © 2018 Alex Vong ;;; Copyright © 2018 Tobias Geerinckx-Rice +;;; Copyright © 2018 John Soo ;;; ;;; This file is part of GNU Guix. ;;; @@ -24,6 +25,7 @@ #:use-module (gnu packages haskell-check) #:use-module (gnu packages haskell-web) #: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) @@ -154,3 +156,49 @@ such as Coq, Epigram and NuPRL.") (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") + (source + (origin + (method url-fetch) + (uri (string-append + "https://github.com/cedille/ial/archive/v" + version ".tar.gz")) + (file-name (string-append name "-" version)) + (sha256 + (base32 + "0ilgalmx3kljy6j9i8d7w6r7ky4bq0xzxanwfr6kyx56mf2sf0zh")))) + (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) + (for-each + (lambda (file) + (install-file + file + (string-append + (assoc-ref outputs "out") "/include/agda/ial"))) + (find-files "." ".*agda.*")) + #t))))) + (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))) -- cgit v1.2.3 From 48752f277c589435aab4d80947fa80f01577d55d Mon Sep 17 00:00:00 2001 From: Ludovic Courtès Date: Wed, 28 Aug 2019 00:19:48 +0200 Subject: gnu: agda-ial: Fetch source from Git. This addresses a 'guix lint' warning. * gnu/packages/agda.scm (agda-ial)[source]: Change to use 'git-fetch'. [arguments]: Change 'install phase accordingly; adjust its 'find-files' regexp. --- gnu/packages/agda.scm | 40 +++++++++++++++++++--------------------- 1 file changed, 19 insertions(+), 21 deletions(-) (limited to 'gnu/packages/agda.scm') diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 8840790058..56d4b15940 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -4,6 +4,7 @@ ;;; Copyright © 2018 Alex Vong ;;; Copyright © 2018 Tobias Geerinckx-Rice ;;; Copyright © 2018 John Soo +;;; Copyright © 2019 Ludovic Courtès ;;; ;;; This file is part of GNU Guix. ;;; @@ -29,6 +30,7 @@ #: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)) @@ -161,16 +163,15 @@ Agda. It also aids the input of Unicode characters."))) (package (name "agda-ial") (version "1.5.0") - (source - (origin - (method url-fetch) - (uri (string-append - "https://github.com/cedille/ial/archive/v" - version ".tar.gz")) - (file-name (string-append name "-" version)) - (sha256 - (base32 - "0ilgalmx3kljy6j9i8d7w6r7ky4bq0xzxanwfr6kyx56mf2sf0zh")))) + (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))) @@ -184,17 +185,14 @@ Agda. It also aids the input of Unicode characters."))) (delete 'check) (replace 'install (lambda* (#:key outputs #:allow-other-keys) - (for-each - (lambda (file) - (install-file - file - (string-append - (assoc-ref outputs "out") "/include/agda/ial"))) - (find-files "." ".*agda.*")) - #t))))) - (home-page "https://github.com/cedille/ial") - (synopsis - "The Iowa Agda Library") + (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 "." "\\.agda$")) + #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 -- cgit v1.2.3 From 83ac4c099a4c31840d2ddce9febadfa75c692648 Mon Sep 17 00:00:00 2001 From: John Soo Date: Tue, 27 Aug 2019 21:46:26 -0700 Subject: gnu: agda-ial: Fix install step. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/agda.scm (agda-ial): copy library and agdai files when installing. Signed-off-by: Ludovic Courtès --- gnu/packages/agda.scm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'gnu/packages/agda.scm') diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 56d4b15940..c085bfac2e 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -190,7 +190,7 @@ Agda. It also aids the input of Unicode characters."))) (for-each (lambda (file) (make-file-writable file) (install-file file include)) - (find-files "." "\\.agda$")) + (find-files "." "\\.agdai?(-lib)?$")) #t)))))) (synopsis "The Iowa Agda Library") (description -- cgit v1.2.3