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

  • Done
  • quality assurance status badge
Details
2 participants
  • Josselin Poiret
  • Christopher Rodriguez
Owner
unassigned
Submitted by
Christopher Rodriguez
Severity
normal
Merged with
C
C
Christopher Rodriguez wrote on 27 Feb 2023 19:10
(address . guix-patches@gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)
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
C
C
Christopher Rodriguez wrote on 27 Feb 2023 19:13
[[PATCH] 1/4] gnu/packages/haskell-xyz.scm: Add ghc-vector-hashtables.
(address . 61848@debbugs.gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)
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
C
C
Christopher Rodriguez wrote on 27 Feb 2023 19:13
[[PATCH] 2/4] gnu/packages/agda.scm: Add agda v2.6.3.
(address . 61848@debbugs.gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)
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
C
C
Christopher Rodriguez wrote on 27 Feb 2023 19:13
[[PATCH] 3/4] gnu/packages/agda.scm: Add emacs-agda2-mode v2.6.3.
(address . 61848@debbugs.gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)
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
C
C
Christopher Rodriguez wrote on 27 Feb 2023 19:13
[[PATCH] 4/4] gnu/packages/agda.scm: Add agda-stdlib v1.7.2.
(address . 61848@debbugs.gnu.org)(name . Christopher Rodriguez)(address . yewscion@gmail.com)
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
J
J
Josselin Poiret wrote on 30 Apr 2023 13:23
Re: [bug#61848] [[PATCH] 0/4] Agda Update and Standard Library
(address . control@debbugs.gnu.org)
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
-----BEGIN PGP SIGNATURE-----

iQHEBAEBCgAuFiEEOSSM2EHGPMM23K8vUF5AuRYXGooFAmROT8IQHGRldkBqcG9p
cmV0Lnh5egAKCRBQXkC5FhcaiuKWC/9CpM+11dIOqK+g78h1XSmQUQ0/JA4c7ASR
ZeGVR+WoK+s1Gvm+YqfROLvnSPsycJ5nkEu2DbNgd+O/dAUkzEkvpaJTeA745Cio
go8UZdZswy9i4uXJEIhznv4bGQseI3gjS/gr9lKCIa4V0kyHPH0ErNc/YiN7VHh7
F/sZqEQN5cPKS6bcVUQuF06IaIgUYDhSn/GbJJq1DMsc5WZ8zC1fYEdartRqLvPs
Vdbbs3mNbByqT2YG8G0D/8ApyRZfsAbKlWdFX5rnYBqWVy/xhX97jIkFIrXmUdEg
6wjvOlpxht0X8L9hmEmRf7zDKmlI+hscLIAi6ZEMTs1COETmPXMgogef8uQ3Sl+E
7tmDf8T89dPCizEcv9bdv/a4YfN8oXqhR01F/LQBG1zQ0oJIYF9ziYx1dWpEB08w
/Jg753tpTb/5DnuH4n5/7Q7dGXQBt76fuPZcOW1/FYh61hgawiGwbQA77mFxuXv6
6DzEk4u9QVg6KUsEbR1fzTqmEZvVRAo=
=tahV
-----END PGP SIGNATURE-----

?