GNU bug report logs -
#61848
[[PATCH] 0/4] Agda Update and Standard Library
Previous Next
Full log
Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
Hello all,
This patch series adds the option to install agda v2.6.3, and the current
version of the standard library alongside it.
Salient Points:
* Agda v2.6.3 requires ghc-vector-hashtables to build.
* As v2.6.2.2 is an LTS on Stackage, v2.6.3 is implemented as a variant.
* Because of this, a variant of emacs-agda2-mode was created with the same
version number.
* agda-stdlib needs to be precompiled in order to be usable due to limitations
in the Agda tooling ecosystem (no way to specify a different default build
directory aside from either _build or alongside the source, both of which
are read-only. However, they are also not going to change post-install, so
while the compilation takes a while it is merely a prerequisite to using the
library, and not a blocker). I conferred with someone on #agda, and it seems
this is how Nix does it, mostly (they opt for the --local-interfaces option,
which makes all interfaces live next to their source files, instead of in a
dedicated, versioned _build directory, which is the default and what this
patch does).
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(+)
--
2.39.1
This bug report was last modified 2 years and 47 days ago.
Previous Next
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.