GNU bug report logs - #61915
[PATCH 0/4] Update Agda to 2.6.3

Previous Next

Full log

View this message in rfc822 format

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: [bug#61915] [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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.