[bug#61848] [[PATCH] 0/4] Agda Update and Standard Library

[bug#61848] [[PATCH] 0/4] Agda Update and Standard Library

[Christopher Rodriguez]

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

[bug#61848] [[PATCH] 1/4] gnu/packages/haskell-xyz.scm: Add ghc-vector-hashtables.

[Christopher Rodriguez]

Signed-off-by: Christopher Rodriguez <yewscion@gmail.com>
---
 gnu/packages/haskell-xyz.scm | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index b6c3a71045..44d58d83e7 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -14033,6 +14033,29 @@ (define-public ghc-pointed
      "This Haskell library provides pointed and copointed data types.")
     (license license:bsd-3)))
 
+(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)
+    (properties '((upstream-name . "vector-hashtables")))
+    (inputs (list ghc-primitive ghc-vector ghc-hashable ghc-hspec-discover))
+    (native-inputs (list ghc-hspec ghc-quickcheck ghc-quickcheck-instances))
+    (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).  See
+\"Data.Vector.Hashtables\" for documentation.")
+    (license license:bsd-3)))
+
+
 (define-public ghc-vector-instances
   (package
     (name "ghc-vector-instances")
-- 
2.39.1

[bug#61848] [[PATCH] 2/4] gnu/packages/agda.scm: Add agda v2.6.3.

[Christopher Rodriguez]

Signed-off-by: Christopher Rodriguez <yewscion@gmail.com>
---
 gnu/packages/agda.scm | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 7128a3f108..7089ba5e93 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -104,6 +104,19 @@ (define-public agda
     ;; source files are BSD-3.  See LICENSE for details.
     (license (list license:expat license:bsd-3))))
 
+(define-public agda-2.6.3
+  (package
+    (inherit agda)
+    (version "2.6.3")
+    (source (origin
+              (method url-fetch)
+              (uri (hackage-uri "Agda" version))
+              (sha256
+               (base32
+                "05k0insn1c2dbpddl1slcdn972j8vgkzzy870yxl43j75j0ckb5y"))))
+    (inputs (modify-inputs (package-inputs agda)
+              (append ghc-vector-hashtables)))))
+
 (define-public emacs-agda2-mode
   (package
     (inherit agda)
-- 
2.39.1

[bug#61848] [[PATCH] 3/4] gnu/packages/agda.scm: Add emacs-agda2-mode v2.6.3.

[Christopher Rodriguez]

Signed-off-by: Christopher Rodriguez <yewscion@gmail.com>
---
 gnu/packages/agda.scm | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 7089ba5e93..816a34fc10 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -133,6 +133,22 @@ (define-public emacs-agda2-mode
     (description "This Emacs mode enables interactive development with
 Agda.  It also aids the input of Unicode characters.")))
 
+(define-public emacs-agda2-mode-2.6.3
+  (package
+    (inherit agda-2.6.3)
+    (name "emacs-agda2-mode")
+    (build-system emacs-build-system)
+    (inputs '())
+    (arguments
+     `(#:phases (modify-phases %standard-phases
+                  (add-after 'unpack 'enter-elisp-dir
+                    (lambda _
+                      (chdir "src/data/emacs-mode") #t)))))
+    (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.")))
+
 (define-public agda-ial
   (package
     (name "agda-ial")
-- 
2.39.1

[bug#61848] [[PATCH] 4/4] gnu/packages/agda.scm: Add agda-stdlib v1.7.2.

[Christopher Rodriguez]

Signed-off-by: Christopher Rodriguez <yewscion@gmail.com>
---
 gnu/packages/agda.scm | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 816a34fc10..488314473e 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -28,6 +28,7 @@ (define-module (gnu packages agda)
   #:use-module (guix build-system emacs)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system haskell)
+  #:use-module (guix build-system copy)
   #:use-module (guix gexp)
   #:use-module (guix download)
   #:use-module (guix git-download)
@@ -190,3 +191,43 @@ (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
+  (let* ((revision "1")
+         (commit "b2e6385c1636897dbee0b10f7194376ff2c1753b"))
+    (package
+      (name "agda-stdlib")
+      (version (git-version "1.7.2" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/agda/agda-stdlib")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "065hf24xjpciwdrvk4isslgcgi01q0k93ql0y1sjqqvy5ryg5xmy"))))
+      (outputs '("out"))
+      (build-system copy-build-system)
+      (arguments
+       (let ((library-directory (string-append "share/agda/agda-stdlib-"
+                                               version "/")))
+         (list #:install-plan #~'(("src" #$library-directory)
+                                  ("_build" #$library-directory)
+                                  ("standard-library.agda-lib" #$library-directory))
+               #:phases #~(modify-phases %standard-phases
+                            (add-before 'install 'create-interfaces
+                              (lambda _
+                                (map (lambda (x)
+                                       (system (string-append "agda " x)))
+                                     (find-files "src" ".*\\.agda"))))))))
+      (native-inputs (list agda-2.6.3))
+      (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))))
-- 
2.39.1

[bug#61848] [[PATCH] 0/4] Agda Update and Standard Library

[Josselin Poiret via Guix-patches via]

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

merge 61848 61915
thankyou

Hi Christopher,

Sorry to come back so late to this patchset.  I finally got around to
work on this, and decided to plainly add an agda-build-system, and
shuffle some stuff around to make Guix work properly with Agda
libraries.  This lets us add agda-stdlib, cubical, agda-categories, etc.
I'm merging both issues, I hope that's fine with you.  Let me know what
you think.

Best,
-- 
Josselin Poiret

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