[bug#61915] [PATCH 0/4] Update Agda to 2.6.3

[bug#61915] [PATCH 0/4] Update Agda to 2.6.3

[Josselin Poiret via Guix-patches via]

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

[bug#61915] [PATCH 1/4] gnu: Add ghc-peano

[Josselin Poiret via Guix-patches via]

* 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

[bug#61915] [PATCH 2/4] gnu: Add ghc-vector-hashtables

[Josselin Poiret via Guix-patches via]

* 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

[bug#61915] [PATCH 3/4] gnu: agda: Update to 2.6.3 and switch to git-fetch

[Josselin Poiret via Guix-patches via]

* 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

[bug#61915] [PATCH 4/4] gnu: agda: Build info manual

[Josselin Poiret via Guix-patches via]

* 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

[bug#61915] [PATCH 0/4] Update Agda to 2.6.3

[Simon Tournier]

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@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@gmail.com>

Cheers,
simon

[bug#61915] [PATCH 0/4] Update Agda to 2.6.3

[Josselin Poiret via Guix-patches via]

[-- Attachment #1: Type: text/plain, Size: 401 bytes --]

Hi Simon,

Simon Tournier <zimon.toutoune@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@2.6.2 around in that other patchset, but
I'll have a look there soon.

Best,
-- 
Josselin Poiret

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 682 bytes --]

[bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries.

[Josselin Poiret via Guix-patches via]

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

[bug#61915] [PATCH v2 01/13] gnu: Add ghc-peano.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 02/13] gnu: Add ghc-vector-hashtables.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 03/13] gnu: agda: Update to 2.6.3 and switch to git-fetch.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 04/13] gnu: agda: Build info manual.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 05/13] gnu: emacs-agda2-mode: No longer inherit from agda.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 06/13] gnu: emacs-agda2-mode: Switch to G-Exps.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 07/13] gnu: agda: Add AGDA_LIBDIRS search-path.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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@jpoiret.xyz>
+From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 08/13] build-system/haskell: Export default-haskell.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 09/13] build-system: New agda-build-system.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 10/13] gnu: Add agda-stdlib.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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@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
+
-- 
2.39.2

[bug#61915] [PATCH v2 11/13] gnu: Add agda-categories.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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@jpoiret.xyz>
+From: Josselin Poiret <dev@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@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@jpoiret.xyz>
+From: Josselin Poiret <dev@jpoiret.xyz>
+Date: Sun, 30 Apr 2023 09:51:12 +0200
+Subject: [PATCH] Remove stdlib-incompatible flags
+
+From: Josselin Poiret <dev@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@jpoiret.xyz>
+From: Josselin Poiret <dev@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@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

[bug#61915] [PATCH v2 12/13] gnu: Add agda-cubical.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

[bug#61915] [PATCH v2 13/13] gnu: Add agda-1lab.

[Josselin Poiret via Guix-patches via]

From: Josselin Poiret <dev@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

bug#61915: [PATCH v2 00/13] Update agda, add build-system and libraries.

[Josselin Poiret via Guix-patches via]

[-- Attachment #1: Type: text/plain, Size: 870 bytes --]

Hi everyone,

Josselin Poiret <dev@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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 682 bytes --]