Package: guix-patches;
Reported by: Josselin Poiret <dev <at> jpoiret.xyz>
Date: Thu, 2 Mar 2023 14:11:02 UTC
Severity: normal
Tags: patch
Merged with 61848
Done: Josselin Poiret <dev <at> jpoiret.xyz>
Bug is archived. No further changes may be made.
To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 61915 in the body.
You can then email your comments to 61915 AT debbugs.gnu.org in the normal way.
Toggle the display of automated, internal messages from the tracker.
View this report as an mbox folder, status mbox, maintainer mbox
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Thu, 02 Mar 2023 14:11:02 GMT) Full text and rfc822 format available.Josselin Poiret <dev <at> jpoiret.xyz>:guix-patches <at> gnu.org.
(Thu, 02 Mar 2023 14:11:02 GMT) Full text and rfc822 format available.Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: guix-patches <at> gnu.org Cc: Josselin Poiret <dev <at> jpoiret.xyz> Subject: [PATCH 0/4] Update Agda to 2.6.3 Date: Thu, 2 Mar 2023 15:10:25 +0100
Hi everyone, This should update Agda to the newly released 2.6.3 version. I also thought it would be a good idea to build the user manual as an info manual, since sphinx has a texinfo backend! This means we have to switch to git-fetch, since the manual is not available in the upstream tarballs from hackage. I don't know how problematic it is wrt. updaters and friends though. Best, Josselin Poiret (4): gnu: Add ghc-peano gnu: Add ghc-vector-hashtables gnu: agda: Update to 2.6.3 and switch to git-fetch gnu: agda: Build info manual gnu/packages/agda.scm | 35 ++++++++++++++++++++++++------ gnu/packages/haskell-xyz.scm | 41 ++++++++++++++++++++++++++++++++++++ 2 files changed, 70 insertions(+), 6 deletions(-) base-commit: 307d1b626be86ed21d48d44a131ce8490f370a17 -- 2.39.1
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Thu, 02 Mar 2023 14:14:02 GMT) Full text and rfc822 format available.Message #8 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, 61915 <at> debbugs.gnu.org Subject: [PATCH 1/4] gnu: Add ghc-peano Date: Thu, 2 Mar 2023 15:13:33 +0100
* gnu/packages/haskell-xyz.scm (ghc-peano): New variable.
---
gnu/packages/haskell-xyz.scm | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)
diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index b6c3a71045..e7e566fcfc 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -8579,6 +8579,26 @@ (define-public ghc-pcre-light
syntax and semantics as Perl 5.")
(license license:bsd-3)))
+(define-public ghc-peano
+ (package
+ (name "ghc-peano")
+ (version "0.1.0.1")
+ (source (origin
+ (method url-fetch)
+ (uri (hackage-uri "peano" version))
+ (sha256
+ (base32
+ "0yzcxrl41dacvx2wkyxjj7hgvz56l4qb59r4h9rmaqd7jcwx5z9i"))))
+ (build-system haskell-build-system)
+ (arguments
+ `(#:cabal-revision ("3"
+ "0wl22dnz6ld300cg6id3lw991bp8kdfi8h0nbv37vn79i1zdcj5n")))
+ (home-page "http://hackage.haskell.org/package/peano")
+ (synopsis "Peano numbers")
+ (description "Provides an efficient Haskell implementation of Peano
+numbers")
+ (license license:bsd-3)))
+
(define-public ghc-persistent
(package
(name "ghc-persistent")
--
2.39.1
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Thu, 02 Mar 2023 14:14:02 GMT) Full text and rfc822 format available.Message #11 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, 61915 <at> debbugs.gnu.org Subject: [PATCH 2/4] gnu: Add ghc-vector-hashtables Date: Thu, 2 Mar 2023 15:13:34 +0100
* gnu/packages/haskell-xyz.scm (ghc-vector-hashtables): New variable.
---
gnu/packages/haskell-xyz.scm | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index e7e566fcfc..a98f8adeb0 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -13305,6 +13305,27 @@ (define-public ghc-vector-builder
vector.")
(license license:expat)))
+(define-public ghc-vector-hashtables
+ (package
+ (name "ghc-vector-hashtables")
+ (version "0.1.1.2")
+ (source (origin
+ (method url-fetch)
+ (uri (hackage-uri "vector-hashtables" version))
+ (sha256
+ (base32
+ "0hrjvy9qg1m5g3w91zxy4syqmp8jk7ajjbxbzkhy282dwfigkyd2"))))
+ (build-system haskell-build-system)
+ (inputs (list ghc-primitive ghc-vector ghc-hashable))
+ (native-inputs (list ghc-hspec ghc-quickcheck ghc-quickcheck-instances
+ hspec-discover))
+ (home-page "https://github.com/klapaucius/vector-hashtables#readme")
+ (synopsis "Efficient vector-based mutable hashtables implementation")
+ (description
+ "This package provides efficient vector-based hashtable implementation
+similar to .NET Generic Dictionary implementation (at the time of 2015).")
+ (license license:bsd-3)))
+
(define-public ghc-vector-th-unbox
(package
(name "ghc-vector-th-unbox")
--
2.39.1
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Thu, 02 Mar 2023 14:14:03 GMT) Full text and rfc822 format available.Message #14 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, 61915 <at> debbugs.gnu.org Subject: [PATCH 3/4] gnu: agda: Update to 2.6.3 and switch to git-fetch Date: Thu, 2 Mar 2023 15:13:35 +0100
* gnu/packages/agda.scm (agda): Update to 2.6.3, switch to fetching using git so
that doc files are included, and add new dependencies ghc-peano and
ghc-vector-hashtables.
---
gnu/packages/agda.scm | 14 +++++++++-----
1 file changed, 9 insertions(+), 5 deletions(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 7128a3f108..1595f2cd22 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -37,15 +37,17 @@ (define-module (gnu packages agda)
(define-public agda
(package
(name "agda")
- (version "2.6.2.2")
+ (version "2.6.3")
(source
(origin
- (method url-fetch)
- (uri (hackage-uri "Agda" version))
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/agda/agda.git")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
(sha256
- (base32 "0yjjbhc593ylrm4mq4j01nkdvh7xqsg5in30wxj4y53vf5hkggp5"))))
+ (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q"))))
(build-system haskell-build-system)
- (properties '((upstream-name . "Agda")))
(inputs
(list ghc-aeson
ghc-alex
@@ -63,11 +65,13 @@ (define-public agda
ghc-monad-control
ghc-murmur-hash
ghc-parallel
+ ghc-peano
ghc-regex-tdfa
ghc-split
ghc-strict
ghc-unordered-containers
ghc-uri-encode
+ ghc-vector-hashtables
ghc-zlib))
(arguments
(list #:modules `((guix build haskell-build-system)
--
2.39.1
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Thu, 02 Mar 2023 14:14:03 GMT) Full text and rfc822 format available.Message #17 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, 61915 <at> debbugs.gnu.org Subject: [PATCH 4/4] gnu: agda: Build info manual Date: Thu, 2 Mar 2023 15:13:36 +0100
* gnu/packages/agda.scm (agda): Build the user manual as an info manual.
---
gnu/packages/agda.scm | 21 ++++++++++++++++++++-
1 file changed, 20 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 1595f2cd22..4a157d5c39 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -25,6 +25,10 @@ (define-module (gnu packages agda)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
+ #:use-module (gnu packages imagemagick)
+ #:use-module (gnu packages python)
+ #:use-module (gnu packages texinfo)
+ #:use-module (gnu packages sphinx)
#:use-module (guix build-system emacs)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
@@ -73,6 +77,12 @@ (define-public agda
ghc-uri-encode
ghc-vector-hashtables
ghc-zlib))
+ (native-inputs
+ (list python
+ python-sphinx
+ python-sphinx-rtd-theme
+ texinfo
+ imagemagick))
(arguments
(list #:modules `((guix build haskell-build-system)
(guix build utils)
@@ -89,7 +99,16 @@ (define-public agda
(let ((agda-compiler (string-append #$output "/bin/agda")))
(for-each (cut invoke agda-compiler <>)
(find-files (string-append #$output "/share")
- "\\.agda$"))))))))
+ "\\.agda$")))))
+ (add-after 'agda-compile 'install-info
+ (lambda _
+ (with-directory-excursion "doc/user-manual"
+ (invoke "sphinx-build" "-b" "texinfo"
+ "." "_build_texinfo")
+ (with-directory-excursion "_build_texinfo"
+ (setenv "infodir" (string-append #$output
+ "/share/info"))
+ (invoke "make" "install-info"))))))))
(home-page "https://wiki.portal.chalmers.se/agda/")
(synopsis
"Dependently typed functional programming language and proof assistant")
--
2.39.1
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Fri, 03 Mar 2023 08:53:02 GMT) Full text and rfc822 format available.Message #20 received at submit <at> debbugs.gnu.org (full text, mbox):
From: Simon Tournier <zimon.toutoune <at> gmail.com> To: Josselin Poiret via Guix-patches via <guix-patches <at> gnu.org>, 61915 <at> debbugs.gnu.org Cc: Josselin Poiret <dev <at> jpoiret.xyz> Subject: Re: [bug#61915] [PATCH 0/4] Update Agda to 2.6.3 Date: Fri, 03 Mar 2023 02:30:09 +0100
Hi Josselin,
It seems some duplicate work with #61848 [1] from Monday.
Maybe the two series could be merged. WDYT?
On Thu, 02 Mar 2023 at 15:10, Josselin Poiret via Guix-patches via <guix-patches <at> gnu.org> wrote:
> This should update Agda to the newly released 2.6.3 version. I also thought it
> would be a good idea to build the user manual as an info manual, since sphinx
> has a texinfo backend! This means we have to switch to git-fetch, since the
> manual is not available in the upstream tarballs from hackage. I don't know how
> problematic it is wrt. updaters and friends though.
>
> Best,
>
> Josselin Poiret (4):
> gnu: Add ghc-peano
> gnu: Add ghc-vector-hashtables
> gnu: agda: Update to 2.6.3 and switch to git-fetch
> gnu: agda: Build info manual
>
> gnu/packages/agda.scm | 35 ++++++++++++++++++++++++------
> gnu/packages/haskell-xyz.scm | 41 ++++++++++++++++++++++++++++++++++++
> 2 files changed, 70 insertions(+), 6 deletions(-)
Well, #61848 reads,
Christopher Rodriguez (4):
gnu/packages/haskell-xyz.scm: Add ghc-vector-hashtables.
gnu/packages/agda.scm: Add agda v2.6.3.
gnu/packages/agda.scm: Add emacs-agda2-mode v2.6.3.
gnu/packages/agda.scm: Add agda-stdlib v1.7.2.
gnu/packages/agda.scm | 70 ++++++++++++++++++++++++++++++++++++
gnu/packages/haskell-xyz.scm | 23 ++++++++++++
2 files changed, 93 insertions(+)
1: <http://issues.guix.gnu.org/msgid/20230227181055.21133-1-yewscion <at> gmail.com>
Cheers,
simon
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Fri, 03 Mar 2023 08:53:02 GMT) Full text and rfc822 format available.guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Fri, 03 Mar 2023 16:25:02 GMT) Full text and rfc822 format available.Message #26 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: Re: [bug#61915] [PATCH 0/4] Update Agda to 2.6.3 Date: Fri, 03 Mar 2023 17:24:27 +0100
[Message part 1 (text/plain, inline)]
Hi Simon, Simon Tournier <zimon.toutoune <at> gmail.com> writes: > Hi Josselin, > > It seems some duplicate work with #61848 [1] from Monday. > > Maybe the two series could be merged. WDYT? My bad, completely missed this one. I'm not too familiar with the reasonning behind keeping agda <at> 2.6.2 around in that other patchset, but I'll have a look there soon. Best, -- Josselin Poiret
[signature.asc (application/pgp-signature, inline)]
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:01 GMT) Full text and rfc822 format available.Message #29 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 00/13] Update agda, add build-system and libraries. Date: Sun, 30 Apr 2023 12:53:10 +0200
Hi everyone, Took me quite some time to get back to this, but since I need this for work and I've been using my patches on top of master to get 2.6.3 for a while now I figured I needed to properly finish this. This series does a couple of things: * Update Agda to 2.6.3, and build its manual in the info format. Note that ghc-peano is not yet needed for 2.6.3 but anyone working on HEAD would need it. * Add a search-path to Agda (AGDA_LIBDIRS) that lets agda search for libraries in these directories. This lets Guix manage Agda libraries. * Add an agda-build-system. It should be quite simple to use for simple libraries but also supports using Haskell to generate Everything.agda or similar setups, like in agda-stdlib. * Add common libraries: agda-stdlib, cubical, agda-categories, 1lab. Most of them are off recent commits, because they don't really have a proper release schedule right now (99% of the users just use git checkouts on HEAD). With these, we can just do `guix shell agda agda-categories` and directly use agda-categories, without any setup like modifying `~/.agda/libraries`. Best, Josselin Poiret (13): gnu: Add ghc-peano. gnu: Add ghc-vector-hashtables. gnu: agda: Update to 2.6.3 and switch to git-fetch. gnu: agda: Build info manual. gnu: emacs-agda2-mode: No longer inherit from agda. gnu: emacs-agda2-mode: Switch to G-Exps. gnu: agda: Add AGDA_LIBDIRS search-path. build-system/haskell: Export default-haskell. build-system: New agda-build-system. gnu: Add agda-stdlib. gnu: Add agda-categories. gnu: Add agda-cubical. gnu: Add agda-1lab. Makefile.am | 2 + doc/guix.texi | 21 ++ gnu/local.mk | 5 + gnu/packages/agda.scm | 192 ++++++++++++++++-- gnu/packages/haskell-xyz.scm | 41 ++++ .../agda-categories-bump-stdlib-version.patch | 42 ++++ ...categories-remove-incompatible-flags.patch | 31 +++ .../patches/agda-categories-use-find.patch | 31 +++ .../patches/agda-libdirs-env-variable.patch | 49 +++++ .../patches/agda-stdlib-use-runhaskell.patch | 28 +++ guix/build-system/agda.scm | 105 ++++++++++ guix/build-system/haskell.scm | 1 + guix/build/agda-build-system.scm | 110 ++++++++++ 13 files changed, 645 insertions(+), 13 deletions(-) create mode 100644 gnu/packages/patches/agda-categories-bump-stdlib-version.patch create mode 100644 gnu/packages/patches/agda-categories-remove-incompatible-flags.patch create mode 100644 gnu/packages/patches/agda-categories-use-find.patch create mode 100644 gnu/packages/patches/agda-libdirs-env-variable.patch create mode 100644 gnu/packages/patches/agda-stdlib-use-runhaskell.patch create mode 100644 guix/build-system/agda.scm create mode 100644 guix/build/agda-build-system.scm base-commit: 4884ee6dd4b1694a4a502dd8058d6c61fa0c0199 -- 2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:02 GMT) Full text and rfc822 format available.Message #32 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 02/13] gnu: Add ghc-vector-hashtables. Date: Sun, 30 Apr 2023 12:53:12 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/haskell-xyz.scm (ghc-vector-hashtables): New variable.
---
gnu/packages/haskell-xyz.scm | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index 0c1eb15d79..aaa7255956 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -13328,6 +13328,27 @@ (define-public ghc-vector-builder
vector.")
(license license:expat)))
+(define-public ghc-vector-hashtables
+ (package
+ (name "ghc-vector-hashtables")
+ (version "0.1.1.2")
+ (source (origin
+ (method url-fetch)
+ (uri (hackage-uri "vector-hashtables" version))
+ (sha256
+ (base32
+ "0hrjvy9qg1m5g3w91zxy4syqmp8jk7ajjbxbzkhy282dwfigkyd2"))))
+ (build-system haskell-build-system)
+ (inputs (list ghc-primitive ghc-vector ghc-hashable))
+ (native-inputs (list ghc-hspec ghc-quickcheck ghc-quickcheck-instances
+ hspec-discover))
+ (home-page "https://github.com/klapaucius/vector-hashtables#readme")
+ (synopsis "Efficient vector-based mutable hashtables implementation")
+ (description
+ "This package provides efficient vector-based hashtable implementation
+similar to .NET Generic Dictionary implementation (at the time of 2015).")
+ (license license:bsd-3)))
+
(define-public ghc-vector-th-unbox
(package
(name "ghc-vector-th-unbox")
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:02 GMT) Full text and rfc822 format available.Message #35 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 01/13] gnu: Add ghc-peano. Date: Sun, 30 Apr 2023 12:53:11 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/haskell-xyz.scm (ghc-peano): New variable.
---
gnu/packages/haskell-xyz.scm | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)
diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index a411bfc40a..0c1eb15d79 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -8602,6 +8602,26 @@ (define-public ghc-pcre-light
syntax and semantics as Perl 5.")
(license license:bsd-3)))
+(define-public ghc-peano
+ (package
+ (name "ghc-peano")
+ (version "0.1.0.1")
+ (source (origin
+ (method url-fetch)
+ (uri (hackage-uri "peano" version))
+ (sha256
+ (base32
+ "0yzcxrl41dacvx2wkyxjj7hgvz56l4qb59r4h9rmaqd7jcwx5z9i"))))
+ (build-system haskell-build-system)
+ (arguments
+ `(#:cabal-revision ("3"
+ "0wl22dnz6ld300cg6id3lw991bp8kdfi8h0nbv37vn79i1zdcj5n")))
+ (home-page "http://hackage.haskell.org/package/peano")
+ (synopsis "Peano numbers")
+ (description "Provides an efficient Haskell implementation of Peano
+numbers")
+ (license license:bsd-3)))
+
(define-public ghc-persistent
(package
(name "ghc-persistent")
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:03 GMT) Full text and rfc822 format available.Message #38 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 03/13] gnu: agda: Update to 2.6.3 and switch to git-fetch. Date: Sun, 30 Apr 2023 12:53:13 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/agda.scm (agda): Update to 2.6.3, switch to fetching using git so
that doc files are included, and add new dependency ghc-vector-hashtables.
---
gnu/packages/agda.scm | 13 ++++++++-----
1 file changed, 8 insertions(+), 5 deletions(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 7128a3f108..252193de90 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -37,15 +37,17 @@ (define-module (gnu packages agda)
(define-public agda
(package
(name "agda")
- (version "2.6.2.2")
+ (version "2.6.3")
(source
(origin
- (method url-fetch)
- (uri (hackage-uri "Agda" version))
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/agda/agda.git")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
(sha256
- (base32 "0yjjbhc593ylrm4mq4j01nkdvh7xqsg5in30wxj4y53vf5hkggp5"))))
+ (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q"))))
(build-system haskell-build-system)
- (properties '((upstream-name . "Agda")))
(inputs
(list ghc-aeson
ghc-alex
@@ -68,6 +70,7 @@ (define-public agda
ghc-strict
ghc-unordered-containers
ghc-uri-encode
+ ghc-vector-hashtables
ghc-zlib))
(arguments
(list #:modules `((guix build haskell-build-system)
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:03 GMT) Full text and rfc822 format available.Message #41 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 05/13] gnu: emacs-agda2-mode: No longer inherit from agda. Date: Sun, 30 Apr 2023 12:53:15 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/agda.scm (emacs-agda2-mode): Remove it. Made no sense, as we only
need the source, which we can refer to without inheriting the whole thing.
---
gnu/packages/agda.scm | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index eba48da0ff..69d6d22d32 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -128,10 +128,10 @@ (define-public agda
(define-public emacs-agda2-mode
(package
- (inherit agda)
(name "emacs-agda2-mode")
+ (version (package-version agda))
+ (source (package-source agda))
(build-system emacs-build-system)
- (inputs '())
(arguments
`(#:phases
(modify-phases %standard-phases
@@ -140,7 +140,8 @@ (define-public emacs-agda2-mode
(home-page "https://agda.readthedocs.io/en/latest/tools/emacs-mode.html")
(synopsis "Emacs mode for Agda")
(description "This Emacs mode enables interactive development with
-Agda. It also aids the input of Unicode characters.")))
+Agda. It also aids the input of Unicode characters.")
+ (license (package-license agda))))
(define-public agda-ial
(package
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:03 GMT) Full text and rfc822 format available.Message #44 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 04/13] gnu: agda: Build info manual. Date: Sun, 30 Apr 2023 12:53:14 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/agda.scm (agda): Build the user manual as an info manual.
---
gnu/packages/agda.scm | 21 ++++++++++++++++++++-
1 file changed, 20 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 252193de90..eba48da0ff 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -25,6 +25,10 @@ (define-module (gnu packages agda)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
+ #:use-module (gnu packages imagemagick)
+ #:use-module (gnu packages python)
+ #:use-module (gnu packages sphinx)
+ #:use-module (gnu packages texinfo)
#:use-module (guix build-system emacs)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
@@ -72,6 +76,12 @@ (define-public agda
ghc-uri-encode
ghc-vector-hashtables
ghc-zlib))
+ (native-inputs
+ (list python
+ python-sphinx
+ python-sphinx-rtd-theme
+ texinfo
+ imagemagick))
(arguments
(list #:modules `((guix build haskell-build-system)
(guix build utils)
@@ -88,7 +98,16 @@ (define-public agda
(let ((agda-compiler (string-append #$output "/bin/agda")))
(for-each (cut invoke agda-compiler <>)
(find-files (string-append #$output "/share")
- "\\.agda$"))))))))
+ "\\.agda$")))))
+ (add-after 'agda-compile 'install-info
+ (lambda _
+ (with-directory-excursion "doc/user-manual"
+ (invoke "sphinx-build" "-b" "texinfo"
+ "." "_build_texinfo")
+ (with-directory-excursion "_build_texinfo"
+ (setenv "infodir" (string-append #$output
+ "/share/info"))
+ (invoke "make" "install-info"))))))))
(home-page "https://wiki.portal.chalmers.se/agda/")
(synopsis
"Dependently typed functional programming language and proof assistant")
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:04 GMT) Full text and rfc822 format available.Message #47 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 08/13] build-system/haskell: Export default-haskell. Date: Sun, 30 Apr 2023 12:53:18 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* guix/build-system/haskell.scm: Export default-haskell.
---
guix/build-system/haskell.scm | 1 +
1 file changed, 1 insertion(+)
diff --git a/guix/build-system/haskell.scm b/guix/build-system/haskell.scm
index b8858421c2..f8568e33db 100644
--- a/guix/build-system/haskell.scm
+++ b/guix/build-system/haskell.scm
@@ -33,6 +33,7 @@ (define-module (guix build-system haskell)
#:use-module (ice-9 match)
#:use-module (srfi srfi-1)
#:export (hackage-uri
+ default-haskell
%haskell-build-system-modules
haskell-build
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:04 GMT) Full text and rfc822 format available.Message #50 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 07/13] gnu: agda: Add AGDA_LIBDIRS search-path. Date: Sun, 30 Apr 2023 12:53:17 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/patches/agda-libdirs-env-variable.patch: New patch.
* gnu/local.mk (dist_patch_DATA): Register it.
* gnu/packages/agda.scm (agda): Patch agda, and add search path.
---
gnu/local.mk | 1 +
gnu/packages/agda.scm | 10 +++-
.../patches/agda-libdirs-env-variable.patch | 49 +++++++++++++++++++
3 files changed, 59 insertions(+), 1 deletion(-)
create mode 100644 gnu/packages/patches/agda-libdirs-env-variable.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 1a84e5b499..712649c5fc 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -880,6 +880,7 @@ dist_patch_DATA = \
%D%/packages/patches/aegisub-icu59-include-unistr.patch \
%D%/packages/patches/aegisub-boost68.patch \
%D%/packages/patches/aegisub-make43.patch \
+ %D%/packages/patches/agda-libdirs-env-variable.patch \
%D%/packages/patches/agg-am_c_prototype.patch \
%D%/packages/patches/agg-2.5-gcc8.patch \
%D%/packages/patches/akonadi-paths.patch \
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index d94036939c..17ea5b62be 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -22,6 +22,7 @@
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
(define-module (gnu packages agda)
+ #:use-module (gnu packages)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -50,7 +51,8 @@ (define-public agda
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
- (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q"))))
+ (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q"))
+ (patches (search-patches "agda-libdirs-env-variable.patch"))))
(build-system haskell-build-system)
(inputs
(list ghc-aeson
@@ -108,6 +110,12 @@ (define-public agda
(setenv "infodir" (string-append #$output
"/share/info"))
(invoke "make" "install-info"))))))))
+ (search-paths
+ (list (search-path-specification
+ (variable "AGDA_LIBDIRS")
+ (files (list "lib/agda")))))
+ (native-search-paths
+ search-paths)
(home-page "https://wiki.portal.chalmers.se/agda/")
(synopsis
"Dependently typed functional programming language and proof assistant")
diff --git a/gnu/packages/patches/agda-libdirs-env-variable.patch b/gnu/packages/patches/agda-libdirs-env-variable.patch
new file mode 100644
index 0000000000..3b291358a6
--- /dev/null
+++ b/gnu/packages/patches/agda-libdirs-env-variable.patch
@@ -0,0 +1,49 @@
+From 457bc7438a4f0801dbf332fa2369248bddf5da0c Mon Sep 17 00:00:00 2001
+Message-Id: <457bc7438a4f0801dbf332fa2369248bddf5da0c.1678309546.git.dev <at> jpoiret.xyz>
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+Date: Wed, 8 Mar 2023 18:31:52 +0100
+Subject: [PATCH] Add environment variable for library directories
+
+AGDA_LIBDIRS is a new environment colon-separated variable for site libraries.
+Agda will look for .agda-lib files directly inside direct descendants of these.
+---
+ src/full/Agda/Interaction/Library.hs | 16 ++++++++++++++--
+ 1 file changed, 14 insertions(+), 2 deletions(-)
+
+diff --git a/src/full/Agda/Interaction/Library.hs b/src/full/Agda/Interaction/Library.hs
+index 09c1f2a82..774cc3e74 100644
+--- a/src/full/Agda/Interaction/Library.hs
++++ b/src/full/Agda/Interaction/Library.hs
+@@ -323,13 +323,25 @@ getInstalledLibraries overrideLibFile = mkLibM [] $ do
+ raiseErrors' [ LibrariesFileNotFound theOverrideLibFile ]
+ return []
+ Right file -> do
+- if not (lfExists file) then return [] else do
++ siteLibDirs <- liftIO $ fromMaybe [] . fmap splitAtColon . lookup "AGDA_LIBDIRS" <$> getEnvironment
++ siteLibs <- liftIO $ concat <$> mapM findSiteLibs siteLibDirs
++ if not (lfExists file) then parseLibFiles Nothing $ nubOn snd ((0,) <$> siteLibs) else do
+ ls <- liftIO $ stripCommentLines <$> UTF8.readFile (lfPath file)
+ files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ]
+- parseLibFiles (Just file) $ nubOn snd files
++ parseLibFiles (Just file) $ nubOn snd (files ++ fmap (0,) siteLibs)
+ `catchIO` \ e -> do
+ raiseErrors' [ ReadError e "Failed to read installed libraries." ]
+ return []
++ where splitAtColon :: String -> [String]
++ splitAtColon "" = []
++ splitAtColon str = case break (==':') str of
++ (a, _:b) -> a : splitAtColon b
++ (a, "") -> [a]
++ findSiteLibs :: String -> IO [String]
++ findSiteLibs dir = do
++ subDirs <- filterM doesDirectoryExist =<< map (dir </>) <$> listDirectory dir
++ subFiles <- mapM (\dir -> map (dir </>) <$> listDirectory dir) subDirs
++ return $ concatMap (filter (List.isSuffixOf ".agda-lib")) subFiles
+
+ -- | Parse the given library files.
+ --
+
+base-commit: 183534bc41af5a53daf685122997dc98883f2be2
+--
+2.39.1
+
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:05 GMT) Full text and rfc822 format available.Message #53 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 06/13] gnu: emacs-agda2-mode: Switch to G-Exps. Date: Sun, 30 Apr 2023 12:53:16 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/agda.scm (emacs-agda2-mode): Switch it up.
---
gnu/packages/agda.scm | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 69d6d22d32..d94036939c 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -133,10 +133,11 @@ (define-public emacs-agda2-mode
(source (package-source agda))
(build-system emacs-build-system)
(arguments
- `(#:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'enter-elisp-dir
- (lambda _ (chdir "src/data/emacs-mode") #t)))))
+ (list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'enter-elisp-dir
+ (lambda _ (chdir "src/data/emacs-mode"))))))
(home-page "https://agda.readthedocs.io/en/latest/tools/emacs-mode.html")
(synopsis "Emacs mode for Agda")
(description "This Emacs mode enables interactive development with
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:05 GMT) Full text and rfc822 format available.Message #56 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 09/13] build-system: New agda-build-system. Date: Sun, 30 Apr 2023 12:53:19 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* guix/build-system/agda.scm: New file.
* guix/build/agda-build-system.scm: New file.
* Makefile.am (MODULES): Register them.
* doc/guix.texi (Build Systems): Add documentation for agda-build-system.
---
Makefile.am | 2 +
doc/guix.texi | 21 ++++++
guix/build-system/agda.scm | 105 +++++++++++++++++++++++++++++
guix/build/agda-build-system.scm | 110 +++++++++++++++++++++++++++++++
4 files changed, 238 insertions(+)
create mode 100644 guix/build-system/agda.scm
create mode 100644 guix/build/agda-build-system.scm
diff --git a/Makefile.am b/Makefile.am
index a763a7e305..9d137cfbb3 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -140,6 +140,7 @@ MODULES = \
guix/platforms/riscv.scm \
guix/platforms/x86.scm \
guix/build-system.scm \
+ guix/build-system/agda.scm \
guix/build-system/android-ndk.scm \
guix/build-system/ant.scm \
guix/build-system/cargo.scm \
@@ -195,6 +196,7 @@ MODULES = \
guix/diagnostics.scm \
guix/ui.scm \
guix/status.scm \
+ guix/build/agda-build-system.scm \
guix/build/android-ndk-build-system.scm \
guix/build/ant-build-system.scm \
guix/build/download.scm \
diff --git a/doc/guix.texi b/doc/guix.texi
index 46e7fd3908..01cd199f0a 100644
--- a/doc/guix.texi
+++ b/doc/guix.texi
@@ -8885,6 +8885,27 @@ of @code{gnu-build-system}, and differ mainly in the set of inputs
implicitly added to the build process, and in the list of phases
executed. Some of these build systems are listed below.
+@defvar agda-build-system
+This variable is exported by @code{(guix build-system agda)}. It
+implements a build procedure for Agda libraries.
+
+It adds @code{agda} to the set of inputs. A different Agda can be
+specified with the @code{#:agda} key.
+
+The @code{#:plan} key is a list of cons cells @code{(@var{regexp}
+. @var{parameters})}, where @var{regexp} is a regexp that should match
+the @code{.agda} files to build, and @var{parameters} is an optional
+list of parameters that will be passed to @code{agda} when type-checking
+it.
+
+When the library uses Haskell to generate a file containing all imports,
+the convenience @code{#:gnu-and-haskell?} can be set to @code{#t} to add
+@code{ghc} and the standard inputs of @code{gnu-build-system} to the
+input list. You will still need to manually add a phase or tweak the
+@code{'build} phase, as in the definition of @code{agda-stdlib}.
+
+@end defvar
+
@defvar ant-build-system
This variable is exported by @code{(guix build-system ant)}. It
implements the build procedure for Java packages that can be built with
diff --git a/guix/build-system/agda.scm b/guix/build-system/agda.scm
new file mode 100644
index 0000000000..cf96ffaa68
--- /dev/null
+++ b/guix/build-system/agda.scm
@@ -0,0 +1,105 @@
+(define-module (guix build-system agda)
+ #:use-module (guix build-system)
+ #:use-module (guix build-system gnu)
+ #:use-module (guix build-system haskell)
+ #:use-module (guix gexp)
+ #:use-module (guix monads)
+ #:use-module (guix packages)
+ #:use-module (guix search-paths)
+ #:use-module (guix store)
+ #:use-module (guix utils)
+ #:export (default-agda
+
+ %agda-build-system-modules
+ agda-build-system))
+
+(define (default-agda)
+ ;; Lazily resolve the binding to avoid a circular dependency.
+ (let ((agda (resolve-interface '(gnu packages agda))))
+ (module-ref agda 'agda)))
+
+(define %agda-build-system-modules
+ `((guix build agda-build-system)
+ ,@%gnu-build-system-modules))
+
+(define %default-modules
+ '((guix build agda-build-system)
+ (guix build utils)))
+
+(define* (lower name
+ #:key source inputs native-inputs outputs system target
+ (agda (default-agda))
+ gnu-and-haskell?
+ #:allow-other-keys
+ #:rest arguments)
+ "Return a bag for NAME."
+ (define private-keywords
+ '(#:target #:agda #:gnu-and-haskell? #:inputs #:native-inputs))
+
+ ;; TODO: cross-compilation support
+ (and (not target)
+ (bag
+ (name name)
+ (system system)
+ (host-inputs `(,@(if source
+ `(("source" ,source))
+ '())
+ ,@inputs))
+ (build-inputs `(("agda" ,agda)
+ ,@(if gnu-and-haskell?
+ (cons*
+ (list "ghc" (default-haskell))
+ (standard-packages))
+ '())
+ ,(assoc "locales" (standard-packages))
+ ,@native-inputs))
+ (outputs outputs)
+ (build agda-build)
+ (arguments (strip-keyword-arguments private-keywords arguments)))))
+
+(define* (agda-build name inputs
+ #:key
+ source
+ (phases '%standard-phases)
+ (outputs '("out"))
+ (search-paths '())
+ (unpack-path "")
+ (build-flags ''())
+ (tests? #t)
+ (system (%current-system))
+ (guile #f)
+ plan
+ (extra-files '("^\\./.*\\.agda-lib$"))
+ (imported-modules %agda-build-system-modules)
+ (modules %default-modules))
+ (define builder
+ (with-imported-modules imported-modules
+ #~(begin
+ (use-modules #$@(sexp->gexp modules))
+ (agda-build #:name #$name
+ #:source #+source
+ #:system #$system
+ #:phases #$phases
+ #:outputs #$(outputs->gexp outputs)
+ #:search-paths '#$(sexp->gexp
+ (map search-path-specification->sexp
+ search-paths))
+ #:unpack-path #$unpack-path
+ #:build-flags #$build-flags
+ #:tests? #$tests?
+ #:inputs #$(input-tuples->gexp inputs)
+ #:plan '#$plan
+ #:extra-files '#$extra-files))))
+
+ (mlet %store-monad ((guile (package->derivation (or guile (default-guile))
+ system #:graft? #f)))
+ (gexp->derivation name builder
+ #:system system
+ #:guile-for-build guile)))
+
+(define agda-build-system
+ (build-system
+ (name 'agda)
+ (description
+ "Build system for Agda libraries")
+ (lower lower)))
diff --git a/guix/build/agda-build-system.scm b/guix/build/agda-build-system.scm
new file mode 100644
index 0000000000..1d7e80d61b
--- /dev/null
+++ b/guix/build/agda-build-system.scm
@@ -0,0 +1,110 @@
+(define-module (guix build agda-build-system)
+ #:use-module ((guix build gnu-build-system) #:prefix gnu:)
+ #:use-module (guix build utils)
+ #:use-module (srfi srfi-26)
+ #:use-module (srfi srfi-34)
+ #:use-module (srfi srfi-35)
+ #:use-module (ice-9 ftw)
+ #:use-module (ice-9 match)
+ #:export (%standard-phases
+ agda-build))
+
+(define* (set-locpath #:key inputs native-inputs #:allow-other-keys)
+ (let ((locales (assoc-ref (or native-inputs inputs) "locales")))
+ (setenv "GUIX_LOCPATH" (string-append locales "/lib/locale"))))
+
+(define %agda-possible-extensions
+ (cons
+ ".agda"
+ (map (cute string-append ".lagda" <>)
+ '(""
+ ".md"
+ ".org"
+ ".rst"
+ ".tex"))))
+
+(define (pattern-predicate pattern)
+ (define compiled-rx (make-regexp pattern))
+ (lambda (file stat)
+ (regexp-exec compiled-rx file)))
+
+(define* (build #:key plan #:allow-other-keys)
+ (for-each
+ (match-lambda
+ ((pattern . options)
+ (for-each
+ (lambda (file)
+ (apply invoke (cons* "agda" file options)))
+ (let ((files (find-files "." (pattern-predicate pattern))))
+ (if (null? files)
+ (raise
+ (make-compound-condition
+ (condition
+ (&message
+ (message (format #f "Plan pattern `~a' did not match any files"
+ pattern))))
+ (condition
+ (&error))))
+ files))))
+ (x
+ (raise
+ (make-compound-condition
+ (condition
+ (&message
+ (message (format #f "Malformed plan element `~a'" x))))
+ (condition
+ (&error))))))
+ plan))
+
+(define* (install #:key outputs name extra-files #:allow-other-keys)
+ (define libdir (string-append (assoc-ref outputs "out") "/lib/agda/" name))
+ (define agda-version
+ (car (scandir "./_build/"
+ (lambda (entry)
+ (not (member entry '("." "..")))))))
+ (define agdai-files
+ (with-directory-excursion
+ (string-join (list "." "_build" agda-version "agda") "/")
+ (find-files ".")))
+ (define (install-source agdai)
+ (define dir (dirname agdai))
+ ;; Drop .agdai
+ (define no-ext (string-drop-right agdai 6))
+ (define source
+ (match (filter file-exists? (map (cute string-append no-ext <>)
+ %agda-possible-extensions))
+ ((single) single)
+ (res (raise
+ (make-compound-condition
+ (condition
+ (&message
+ (message
+ (format #f
+ "Cannot find unique source file for agdai file `~a`, got `~a`"
+ agdai res))))
+ (condition
+ (&error)))))))
+ (install-file source (string-append libdir "/" dir)))
+ (for-each install-source agdai-files)
+ (copy-recursively "_build" (string-append libdir "/_build"))
+ (for-each
+ (lambda (pattern)
+ (for-each
+ (lambda (file)
+ (install-file file libdir))
+ (find-files "." (pattern-predicate pattern))))
+ extra-files))
+
+(define %standard-phases
+ (modify-phases gnu:%standard-phases
+ (add-before 'install-locale 'set-locpath set-locpath)
+ (delete 'bootstrap)
+ (delete 'configure)
+ (replace 'build build)
+ (delete 'check) ;; No universal checker
+ (replace 'install install)))
+
+(define* (agda-build #:key inputs (phases %standard-phases)
+ #:allow-other-keys #:rest args)
+ "Build the given Agda package, applying all of PHASES in order."
+ (apply gnu:gnu-build #:inputs inputs #:phases phases args))
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:05 GMT) Full text and rfc822 format available.Message #59 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 11/13] gnu: Add agda-categories. Date: Sun, 30 Apr 2023 12:53:21 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/patches/agda-categories-bump-stdlib-version.patch
* gnu/packages/patches/agda-categories-remove-incompatible-flags.patch
* gnu/packages/patches/agda-categories-use-find.patch: New patches.
* gnu/local.mk (dist_patch_DATA): Register them.
* gnu/packages/agda.scm: New variable agda-categories.
---
gnu/local.mk | 3 ++
gnu/packages/agda.scm | 35 ++++++++++++++++
.../agda-categories-bump-stdlib-version.patch | 42 +++++++++++++++++++
...categories-remove-incompatible-flags.patch | 31 ++++++++++++++
.../patches/agda-categories-use-find.patch | 31 ++++++++++++++
5 files changed, 142 insertions(+)
create mode 100644 gnu/packages/patches/agda-categories-bump-stdlib-version.patch
create mode 100644 gnu/packages/patches/agda-categories-remove-incompatible-flags.patch
create mode 100644 gnu/packages/patches/agda-categories-use-find.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 0a1c4dfb24..4193146862 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -880,6 +880,9 @@ dist_patch_DATA = \
%D%/packages/patches/aegisub-icu59-include-unistr.patch \
%D%/packages/patches/aegisub-boost68.patch \
%D%/packages/patches/aegisub-make43.patch \
+ %D%/packages/patches/agda-categories-bump-stdlib-version.patch \
+ %D%/packages/patches/agda-categories-remove-incompatible-flags.patch \
+ %D%/packages/patches/agda-categories-use-find.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 \
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index a6ff01b737..1068d8734f 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -230,3 +230,38 @@ (define-public agda-stdlib
(home-page "https://wiki.portal.chalmers.se/agda/pmwiki.php")
(license license:expat)))
+(define-public agda-categories
+ ;; Upstream hasn't released in a very long time, especially not against
+ ;; 2.6.3.
+ (let* ((revision "1")
+ (commit "20397e93a60ed1439ed57ee76ae377c66a5eb8d9"))
+ (package
+ (name "agda-categories")
+ (version (git-version "0.4" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/agda/agda-categories.git")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0q4dqvs4ig138wghlglz37ay5i524gk6k5x476ki5mnxc603bmqy"))
+ (patches (search-patches "agda-categories-bump-stdlib-version.patch"
+ "agda-categories-remove-incompatible-flags.patch"
+ "agda-categories-use-find.patch"))))
+ (build-system agda-build-system)
+ (arguments
+ (list
+ #:gnu-and-haskell? #t
+ #:phases
+ #~(modify-phases %standard-phases
+ (replace 'build
+ (lambda _
+ (invoke "make"))))))
+ (propagated-inputs
+ (list agda-stdlib))
+ (synopsis "A new Categories library for Agda")
+ (description "A new Categories library for Agda")
+ (home-page "https://github.com/agda/agda-categories")
+ (license license:expat))))
diff --git a/gnu/packages/patches/agda-categories-bump-stdlib-version.patch b/gnu/packages/patches/agda-categories-bump-stdlib-version.patch
new file mode 100644
index 0000000000..2e78cc1446
--- /dev/null
+++ b/gnu/packages/patches/agda-categories-bump-stdlib-version.patch
@@ -0,0 +1,42 @@
+From 080eae2adc1b0e8f1829c4138b3d462218a02f36 Mon Sep 17 00:00:00 2001
+Message-Id: <080eae2adc1b0e8f1829c4138b3d462218a02f36.1682840777.git.dev <at> jpoiret.xyz>
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+Date: Sun, 30 Apr 2023 09:32:59 +0200
+Subject: [PATCH] Bump Agda to 2.6.3 and stdlib to 1.7.2
+
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+
+---
+ .github/workflows/ci-ubuntu.yml | 4 ++--
+ agda-categories.agda-lib | 2 +-
+ 2 files changed, 3 insertions(+), 3 deletions(-)
+
+diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
+index ab26835d..25604420 100644
+--- a/.github/workflows/ci-ubuntu.yml
++++ b/.github/workflows/ci-ubuntu.yml
+@@ -45,8 +45,8 @@ on:
+ ########################################################################
+
+ env:
+- AGDA_COMMIT: tags/v2.6.2
+- STDLIB_VERSION: 1.7.1
++ AGDA_COMMIT: tags/v2.6.3
++ STDLIB_VERSION: 1.7.2
+
+ GHC_VERSION: 8.6.5
+ CABAL_VERSION: 3.2.0.0
+diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib
+index 186e350b..5b19c405 100644
+--- a/agda-categories.agda-lib
++++ b/agda-categories.agda-lib
+@@ -1,3 +1,3 @@
+ name: agda-categories
+-depend: standard-library-1.7.1
++depend: standard-library-1.7.2
+ include: src/
+
+base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9
+--
+2.39.2
+
diff --git a/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch b/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch
new file mode 100644
index 0000000000..dc33af7cf9
--- /dev/null
+++ b/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch
@@ -0,0 +1,31 @@
+From 3d73d59617281c6ae9c19032eae381ff77fd2e65 Mon Sep 17 00:00:00 2001
+Message-Id: <3d73d59617281c6ae9c19032eae381ff77fd2e65.1682841188.git.dev <at> jpoiret.xyz>
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+Date: Sun, 30 Apr 2023 09:51:12 +0200
+Subject: [PATCH] Remove stdlib-incompatible flags
+
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+
+---
+ Makefile | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/Makefile b/Makefile
+index 68846579..ba5923a2 100644
+--- a/Makefile
++++ b/Makefile
+@@ -1,6 +1,6 @@
+ .PHONY: test Everything.agda clean
+
+-OTHEROPTS = --auto-inline -Werror
++OTHEROPTS =
+
+ RTSARGS = +RTS -M6G -A128M -RTS ${OTHEROPTS}
+
+
+base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9
+prerequisite-patch-id: da10df58fa86d08b31174a01db7b9a02377aba55
+prerequisite-patch-id: 508dabd923ba9ac1ee4d8dab6697432b4bd8ba18
+--
+2.39.2
+
diff --git a/gnu/packages/patches/agda-categories-use-find.patch b/gnu/packages/patches/agda-categories-use-find.patch
new file mode 100644
index 0000000000..772352a0cb
--- /dev/null
+++ b/gnu/packages/patches/agda-categories-use-find.patch
@@ -0,0 +1,31 @@
+From 53922aedd81d5111d9007b41235aa12eaa2a863d Mon Sep 17 00:00:00 2001
+Message-Id: <53922aedd81d5111d9007b41235aa12eaa2a863d.1682840933.git.dev <at> jpoiret.xyz>
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+Date: Sun, 30 Apr 2023 09:48:21 +0200
+Subject: [PATCH] Use find instead of git ls-tree in Makefile
+
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+
+---
+ Makefile | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/Makefile b/Makefile
+index 158802d1..68846579 100644
+--- a/Makefile
++++ b/Makefile
+@@ -11,7 +11,7 @@ html: Everything.agda
+ agda ${RTSARGS} --html -i. Everything.agda
+
+ Everything.agda:
+- git ls-tree --full-tree -r --name-only HEAD | grep '^src/[^\.]*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda
++ find src -iname '*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda
+
+ clean:
+ find . -name '*.agdai' -exec rm \{\} \;
+
+base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9
+prerequisite-patch-id: da10df58fa86d08b31174a01db7b9a02377aba55
+--
+2.39.2
+
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:06 GMT) Full text and rfc822 format available.Message #62 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 12/13] gnu: Add agda-cubical. Date: Sun, 30 Apr 2023 12:53:22 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/agda.scm: New variable agda-cubical.
---
gnu/packages/agda.scm | 33 +++++++++++++++++++++++++++++++++
1 file changed, 33 insertions(+)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 1068d8734f..e75386c990 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -265,3 +265,36 @@ (define-public agda-categories
(description "A new Categories library for Agda")
(home-page "https://github.com/agda/agda-categories")
(license license:expat))))
+
+(define-public agda-cubical
+ ;; Upstream's HEAD follows the latest Agda release, but they don't release
+ ;; until a newer Agda release comes up, so their releases are always one
+ ;; version late.
+ (let* ((revision "1")
+ (commit "3dc3cd12579544c8c1c1d2c5f64fd8d577fd3d66"))
+ (package
+ (name "agda-cubical")
+ (version (git-version "0.4" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/agda/cubical.git")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "1b40adjgwrrdarzk0yiy2jmjgmf455ax6z70hfzdgc6j06vdb6mg"))))
+ (build-system agda-build-system)
+ (arguments
+ (list
+ #:gnu-and-haskell? #t
+ #:phases
+ #~(modify-phases %standard-phases
+ (replace 'build
+ (lambda _
+ (invoke "make"))))))
+ (synopsis "A standard library for Cubical Agda")
+ (description "A standard library for Cubical Agda, comparable to
+agda-stdlib but using cubical methods.")
+ (home-page "https://github.com/agda/cubical")
+ (license license:expat))))
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:54:06 GMT) Full text and rfc822 format available.Message #65 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 13/13] gnu: Add agda-1lab. Date: Sun, 30 Apr 2023 12:53:23 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* gnu/packages/agda.scm: New variable agda-1lab.
---
gnu/packages/agda.scm | 29 +++++++++++++++++++++++++++++
1 file changed, 29 insertions(+)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index e75386c990..2116ceced3 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -298,3 +298,32 @@ (define-public agda-cubical
agda-stdlib but using cubical methods.")
(home-page "https://github.com/agda/cubical")
(license license:expat))))
+
+(define-public agda-1lab
+ ;; Upstream doesn't do releases (yet). Use a commit that builds with 2.6.3,
+ ;; since they use Agda HEAD.
+ (let* ((revision "1")
+ (commit "47ca1d23640a6f49a3abe3c2fe27738bcc10c9c6"))
+ (package
+ (name "agda-1lab")
+ (version (git-version "0.0" revision commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/plt-amy/1lab.git")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0j7mp6c0xd0849skdxzncklkxynxnyfrbpcjv4qp5p1xfn0dnfqx"))))
+ (build-system agda-build-system)
+ (arguments
+ (list #:plan '(("src/index\\.lagda\\.md$"))))
+ (synopsis "Areference resource for mathematics done in Homotopy Type Theory")
+ (description "A formalised, cross-linked reference resource for
+mathematics done in Homotopy Type Theory. Unlike the HoTT book, the 1lab is
+not a “linear” resource: Concepts are presented as a directed graph, with
+links indicating dependencies.")
+ (home-page "https://1lab.dev")
+ (license license:agpl3))))
--
2.39.2
guix-patches <at> gnu.org:bug#61915; Package guix-patches.
(Sun, 30 Apr 2023 10:55:02 GMT) Full text and rfc822 format available.Message #68 received at 61915 <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: Josselin Poiret <dev <at> jpoiret.xyz>, Simon Tournier <zimon.toutoune <at> gmail.com>, 61915 <at> debbugs.gnu.org Subject: [PATCH v2 10/13] gnu: Add agda-stdlib. Date: Sun, 30 Apr 2023 12:53:20 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
* 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.
---
gnu/local.mk | 1 +
gnu/packages/agda.scm | 37 +++++++++++++++++++
.../patches/agda-stdlib-use-runhaskell.patch | 28 ++++++++++++++
3 files changed, 66 insertions(+)
create mode 100644 gnu/packages/patches/agda-stdlib-use-runhaskell.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 712649c5fc..0a1c4dfb24 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -881,6 +881,7 @@ dist_patch_DATA = \
%D%/packages/patches/aegisub-boost68.patch \
%D%/packages/patches/aegisub-make43.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-2.5-gcc8.patch \
%D%/packages/patches/akonadi-paths.patch \
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 17ea5b62be..a6ff01b737 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -30,6 +30,7 @@ (define-module (gnu packages agda)
#: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)
@@ -193,3 +194,39 @@ (define-public agda-ial
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))))
+ (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)))
+
diff --git a/gnu/packages/patches/agda-stdlib-use-runhaskell.patch b/gnu/packages/patches/agda-stdlib-use-runhaskell.patch
new file mode 100644
index 0000000000..21ce16689f
--- /dev/null
+++ b/gnu/packages/patches/agda-stdlib-use-runhaskell.patch
@@ -0,0 +1,28 @@
+From 3dc3c0856906d25bb697a4480a8457a69637cd51 Mon Sep 17 00:00:00 2001
+Message-Id: <3dc3c0856906d25bb697a4480a8457a69637cd51.1682798848.git.dev <at> jpoiret.xyz>
+From: Josselin Poiret <dev <at> jpoiret.xyz>
+Date: Sat, 29 Apr 2023 22:06:55 +0200
+Subject: [PATCH] Makefile: use runhaskell instead of cabal
+
+From: Josselin Poiret <dev <at> 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
+
--
2.39.2
Josselin Poiret <dev <at> jpoiret.xyz>
to control <at> debbugs.gnu.org.
(Sun, 30 Apr 2023 11:24:02 GMT) Full text and rfc822 format available.Josselin Poiret <dev <at> jpoiret.xyz>:Josselin Poiret <dev <at> jpoiret.xyz>:Message #75 received at 61915-done <at> debbugs.gnu.org (full text, mbox):
From: Josselin Poiret <dev <at> jpoiret.xyz> To: 61915-done <at> debbugs.gnu.org Subject: Re: [PATCH v2 00/13] Update agda, add build-system and libraries. Date: Sun, 04 Jun 2023 11:47:37 +0200
[Message part 1 (text/plain, inline)]
Hi everyone, Josselin Poiret <dev <at> jpoiret.xyz> writes: > Josselin Poiret (13): > gnu: Add ghc-peano. > gnu: Add ghc-vector-hashtables. > gnu: agda: Update to 2.6.3 and switch to git-fetch. > gnu: agda: Build info manual. > gnu: emacs-agda2-mode: No longer inherit from agda. > gnu: emacs-agda2-mode: Switch to G-Exps. > gnu: agda: Add AGDA_LIBDIRS search-path. > build-system/haskell: Export default-haskell. > build-system: New agda-build-system. > gnu: Add agda-stdlib. > gnu: Add agda-categories. > gnu: Add agda-cubical. > gnu: Add agda-1lab. Pushed as e198fe4e942c58136dd4cb8ebf49cade58a8f5e3 with some additions, notably refactoring some descriptions that the linter didn't like, and updating agda-categories to the new released version, agda-cubical and agda-ial to a new commit. Best, -- Josselin Poiret
[signature.asc (application/pgp-signature, inline)]
Josselin Poiret <dev <at> jpoiret.xyz>:Christopher Rodriguez <yewscion <at> gmail.com>:Debbugs Internal Request <help-debbugs <at> gnu.org>
to internal_control <at> debbugs.gnu.org.
(Sun, 02 Jul 2023 11:24:05 GMT) Full text and rfc822 format available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.