mirror of
https://git.in.rschanz.org/ryan77627/guix.git
synced 2025-01-12 14:16:55 -05:00
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.
This commit is contained in:
parent
80d1228321
commit
c1f8bcbbda
3 changed files with 67 additions and 0 deletions
|
@ -886,6 +886,7 @@ dist_patch_DATA = \
|
||||||
%D%/packages/patches/aegisub-boost68.patch \
|
%D%/packages/patches/aegisub-boost68.patch \
|
||||||
%D%/packages/patches/aegisub-make43.patch \
|
%D%/packages/patches/aegisub-make43.patch \
|
||||||
%D%/packages/patches/agda-libdirs-env-variable.patch \
|
%D%/packages/patches/agda-libdirs-env-variable.patch \
|
||||||
|
%D%/packages/patches/agda-stdlib-use-runhaskell.patch \
|
||||||
%D%/packages/patches/agg-am_c_prototype.patch \
|
%D%/packages/patches/agg-am_c_prototype.patch \
|
||||||
%D%/packages/patches/agg-2.5-gcc8.patch \
|
%D%/packages/patches/agg-2.5-gcc8.patch \
|
||||||
%D%/packages/patches/akonadi-paths.patch \
|
%D%/packages/patches/akonadi-paths.patch \
|
||||||
|
|
|
@ -31,6 +31,7 @@ (define-module (gnu packages agda)
|
||||||
#:use-module (gnu packages python)
|
#:use-module (gnu packages python)
|
||||||
#:use-module (gnu packages sphinx)
|
#:use-module (gnu packages sphinx)
|
||||||
#:use-module (gnu packages texinfo)
|
#:use-module (gnu packages texinfo)
|
||||||
|
#:use-module (guix build-system agda)
|
||||||
#:use-module (guix build-system emacs)
|
#:use-module (guix build-system emacs)
|
||||||
#:use-module (guix build-system gnu)
|
#:use-module (guix build-system gnu)
|
||||||
#:use-module (guix build-system haskell)
|
#:use-module (guix build-system haskell)
|
||||||
|
@ -194,3 +195,40 @@ (define-public agda-ial
|
||||||
trees, tries, vectors, and rudimentary IO. A number of good ideas
|
trees, tries, vectors, and rudimentary IO. A number of good ideas
|
||||||
come from Agda's standard library.")
|
come from Agda's standard library.")
|
||||||
(license license:expat)))
|
(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)))
|
||||||
|
|
||||||
|
|
28
gnu/packages/patches/agda-stdlib-use-runhaskell.patch
Normal file
28
gnu/packages/patches/agda-stdlib-use-runhaskell.patch
Normal file
|
@ -0,0 +1,28 @@
|
||||||
|
From 3dc3c0856906d25bb697a4480a8457a69637cd51 Mon Sep 17 00:00:00 2001
|
||||||
|
Message-Id: <3dc3c0856906d25bb697a4480a8457a69637cd51.1682798848.git.dev@jpoiret.xyz>
|
||||||
|
From: Josselin Poiret <dev@jpoiret.xyz>
|
||||||
|
Date: Sat, 29 Apr 2023 22:06:55 +0200
|
||||||
|
Subject: [PATCH] Makefile: use runhaskell instead of cabal
|
||||||
|
|
||||||
|
From: Josselin Poiret <dev@jpoiret.xyz>
|
||||||
|
|
||||||
|
---
|
||||||
|
GNUmakefile | 2 +-
|
||||||
|
1 file changed, 1 insertion(+), 1 deletion(-)
|
||||||
|
|
||||||
|
diff --git a/GNUmakefile b/GNUmakefile
|
||||||
|
index c5d886e03..f3cb2a1e7 100644
|
||||||
|
--- a/GNUmakefile
|
||||||
|
+++ b/GNUmakefile
|
||||||
|
@@ -21,7 +21,7 @@ Everything.agda:
|
||||||
|
# command `cabal install` is needed by cabal-install <= 2.4.*. I did
|
||||||
|
# not found any problem running both commands with different versions
|
||||||
|
# of cabal-install. See Issue #1001.
|
||||||
|
- cabal run GenerateEverything
|
||||||
|
+ runhaskell GenerateEverything
|
||||||
|
|
||||||
|
.PHONY: listings
|
||||||
|
listings: Everything.agda
|
||||||
|
--
|
||||||
|
2.39.2
|
||||||
|
|
Loading…
Reference in a new issue