[[PATCH] 0/4] Agda Update and Standard Library

Done

Details

2 participants

Josselin Poiret
Christopher Rodriguez

Owner: unassigned

Submitted by: Christopher Rodriguez

Severity: normal

Merged with

61915

Christopher Rodriguez wrote on 27 Feb 2023 19:10

Recipients:(address . guix-patches@gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)

Message-ID:20230227181055.21133-1-yewscion@gmail.com

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

Christopher Rodriguez wrote on 27 Feb 2023 19:13

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

Recipients:(address . 61848@debbugs.gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)

Message-ID:20230227181323.21387-1-yewscion@gmail.com

Signed-off-by: Christopher Rodriguez <yewscion@gmail.com>

---

gnu/packages/haskell-xyz.scm | 23 +++++++++++++++++++++++

1 file changed, 23 insertions(+)

Toggle diff (36 lines)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

Christopher Rodriguez wrote on 27 Feb 2023 19:13

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

Recipients:(address . 61848@debbugs.gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)

Message-ID:20230227181323.21387-2-yewscion@gmail.com

Signed-off-by: Christopher Rodriguez <yewscion@gmail.com>

---

gnu/packages/agda.scm | 13 +++++++++++++

1 file changed, 13 insertions(+)

Toggle diff (26 lines)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

Christopher Rodriguez wrote on 27 Feb 2023 19:13

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

Recipients:(address . 61848@debbugs.gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)

Message-ID:20230227181323.21387-3-yewscion@gmail.com

Signed-off-by: Christopher Rodriguez <yewscion@gmail.com>

---

gnu/packages/agda.scm | 16 ++++++++++++++++

1 file changed, 16 insertions(+)

Toggle diff (29 lines)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

Christopher Rodriguez wrote on 27 Feb 2023 19:13

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

Recipients:(address . 61848@debbugs.gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)

Message-ID:20230227181323.21387-4-yewscion@gmail.com

Signed-off-by: Christopher Rodriguez <yewscion@gmail.com>

---

gnu/packages/agda.scm | 41 +++++++++++++++++++++++++++++++++++++++++

1 file changed, 41 insertions(+)

Toggle diff (58 lines)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

Josselin Poiret wrote on 30 Apr 2023 13:23

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

Recipients:(address . control@debbugs.gnu.org)

Message-ID:87bkj5ehq5.fsf@jpoiret.xyz

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

Your comment

This issue is archived.

To comment on this conversation send an email to 61848@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it

mumi current 61848

Then, you may apply the latest patchset in this issue (with sign off)

mumi am -- -s

Or, compose a reply to this issue

mumi compose

Or, send patches to this issue

mumi send-email *.patch

is:open	open issues
is:done	closed issues
submitter:<who>	search issue submitter
author:<who>	search by message author
date:yesterday..now	search by issue date
mdate:3m..2d	search by message date