diff options
| author | Josselin Poiret <dev@jpoiret.xyz> | 2023-04-29 17:01:14 +0200 |
|---|---|---|
| committer | Josselin Poiret <dev@jpoiret.xyz> | 2023-06-04 10:59:34 +0200 |
| commit | c1f8bcbbda4d90dc98d5e808049f008dffe6b979 (patch) | |
| tree | 78e53df384b040a887a21a7450824f32f66165c6 /gnu/packages/agda.scm | |
| parent | 80d122832135c4b7f1a35d22ae746cc6374a83f5 (diff) | |
| download | guix-c1f8bcbbda4d90dc98d5e808049f008dffe6b979.tar guix-c1f8bcbbda4d90dc98d5e808049f008dffe6b979.tar.gz | |
gnu: Add agda-stdlib.
* gnu/packages/patches/agda-stdlib-use-runhaskell.patch: New patch.
* gnu/local.mk (dist_patch_DATA): Register it.
* gnu/packages/agda.scm: New variable agda-stdlib.
Diffstat (limited to 'gnu/packages/agda.scm')
| -rw-r--r-- | gnu/packages/agda.scm | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index c73c238a35..dd427bff02 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -31,6 +31,7 @@ #:use-module (gnu packages python) #:use-module (gnu packages sphinx) #:use-module (gnu packages texinfo) + #:use-module (guix build-system agda) #:use-module (guix build-system emacs) #:use-module (guix build-system gnu) #:use-module (guix build-system haskell) @@ -194,3 +195,40 @@ 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))) + +(define-public agda-stdlib + (package + (name "agda-stdlib") + (version "1.7.2") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/agda/agda-stdlib") + (commit (string-append "v" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "065hf24xjpciwdrvk4isslgcgi01q0k93ql0y1sjqqvy5ryg5xmy")))) + (build-system agda-build-system) + (arguments + (list + #:plan '(("^\\./README.agda$" "-i.")) + #:gnu-and-haskell? #t + #:phases + #~(modify-phases %standard-phases + (add-before 'build 'generate-everything + (lambda* (#:key inputs native-inputs #:allow-other-keys) + (invoke + (search-input-file (or native-inputs inputs) "/bin/runhaskell") + "GenerateEverything.hs")))))) + (native-inputs (list ghc-filemanip)) + (synopsis "The Agda Standard Library") + (description + "The standard library aims to contain all the tools needed to write +both programs and proofs easily. While we always try and write efficient +code, we prioritize ease of proof over type-checking and normalization +performance. If computational performance is important to you, then perhaps +try agda-prelude instead.") + (home-page "https://wiki.portal.chalmers.se/agda/pmwiki.php") + (license license:expat))) + |