GNU bug report logs - #61848
[[PATCH] 0/4] Agda Update and Standard Library

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 61848 in the body.
You can then email your comments to 61848 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Christopher Rodriguez <yewscion <at> gmail.com>
To: guix-patches <at> gnu.org
Cc: Christopher Rodriguez <yewscion <at> gmail.com>
Subject: [[PATCH] 0/4] Agda Update and Standard Library
Date: Mon, 27 Feb 2023 13:10:55 -0500

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

Message #8 received at 61848 <at> debbugs.gnu.org (full text, mbox):

From: Christopher Rodriguez <yewscion <at> gmail.com>
To: 61848 <at> debbugs.gnu.org
Cc: Christopher Rodriguez <yewscion <at> gmail.com>
Subject: [[PATCH] 1/4] gnu/packages/haskell-xyz.scm: Add ghc-vector-hashtables.
Date: Mon, 27 Feb 2023 13:13:20 -0500

Signed-off-by: Christopher Rodriguez <yewscion <at> 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

Message #11 received at 61848 <at> debbugs.gnu.org (full text, mbox):

From: Christopher Rodriguez <yewscion <at> gmail.com>
To: 61848 <at> debbugs.gnu.org
Cc: Christopher Rodriguez <yewscion <at> gmail.com>
Subject: [[PATCH] 2/4] gnu/packages/agda.scm: Add agda v2.6.3.
Date: Mon, 27 Feb 2023 13:13:21 -0500

Signed-off-by: Christopher Rodriguez <yewscion <at> 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

Message #14 received at 61848 <at> debbugs.gnu.org (full text, mbox):

From: Christopher Rodriguez <yewscion <at> gmail.com>
To: 61848 <at> debbugs.gnu.org
Cc: Christopher Rodriguez <yewscion <at> gmail.com>
Subject: [[PATCH] 3/4] gnu/packages/agda.scm: Add emacs-agda2-mode v2.6.3.
Date: Mon, 27 Feb 2023 13:13:22 -0500

Signed-off-by: Christopher Rodriguez <yewscion <at> 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

Message #17 received at 61848 <at> debbugs.gnu.org (full text, mbox):

From: Christopher Rodriguez <yewscion <at> gmail.com>
To: 61848 <at> debbugs.gnu.org
Cc: Christopher Rodriguez <yewscion <at> gmail.com>
Subject: [[PATCH] 4/4] gnu/packages/agda.scm: Add agda-stdlib v1.7.2.
Date: Mon, 27 Feb 2023 13:13:23 -0500

Signed-off-by: Christopher Rodriguez <yewscion <at> 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

Message #20 received at 61848 <at> debbugs.gnu.org (full text, mbox):

From: Josselin Poiret <dev <at> jpoiret.xyz>
To: Christopher Rodriguez <yewscion <at> gmail.com>, 61848 <at> debbugs.gnu.org
Cc: control <at> debbugs.gnu.org
Subject: Re: [bug#61848] [[PATCH] 0/4] Agda Update and Standard Library
Date: Sun, 30 Apr 2023 13:23:46 +0200

[Message part 1 (text/plain, inline)]

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

[signature.asc (application/pgp-signature, inline)]

Previous Next

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