mbox series

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

Message ID cover.1682851600.git.dev@jpoiret.xyz
Headers show
Series Update agda, add build-system and libraries. | expand

Message

Josselin Poiret April 30, 2023, 10:53 a.m. UTC 
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

Comments

Josselin Poiret June 4, 2023, 9:47 a.m. UTC | #1 
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,