* [bug#61915] [PATCH v2 01/13] gnu: Add ghc-peano.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 02/13] gnu: Add ghc-vector-hashtables Josselin Poiret via Guix-patches via
` (12 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/haskell-xyz.scm (ghc-peano): New variable.
---
gnu/packages/haskell-xyz.scm | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)
diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index a411bfc40a..0c1eb15d79 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -8602,6 +8602,26 @@ (define-public ghc-pcre-light
syntax and semantics as Perl 5.")
(license license:bsd-3)))
+(define-public ghc-peano
+ (package
+ (name "ghc-peano")
+ (version "0.1.0.1")
+ (source (origin
+ (method url-fetch)
+ (uri (hackage-uri "peano" version))
+ (sha256
+ (base32
+ "0yzcxrl41dacvx2wkyxjj7hgvz56l4qb59r4h9rmaqd7jcwx5z9i"))))
+ (build-system haskell-build-system)
+ (arguments
+ `(#:cabal-revision ("3"
+ "0wl22dnz6ld300cg6id3lw991bp8kdfi8h0nbv37vn79i1zdcj5n")))
+ (home-page "http://hackage.haskell.org/package/peano")
+ (synopsis "Peano numbers")
+ (description "Provides an efficient Haskell implementation of Peano
+numbers")
+ (license license:bsd-3)))
+
(define-public ghc-persistent
(package
(name "ghc-persistent")
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 02/13] gnu: Add ghc-vector-hashtables.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 01/13] gnu: Add ghc-peano Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 03/13] gnu: agda: Update to 2.6.3 and switch to git-fetch Josselin Poiret via Guix-patches via
` (11 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/haskell-xyz.scm (ghc-vector-hashtables): New variable.
---
gnu/packages/haskell-xyz.scm | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index 0c1eb15d79..aaa7255956 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -13328,6 +13328,27 @@ (define-public ghc-vector-builder
vector.")
(license license:expat)))
+(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)
+ (inputs (list ghc-primitive ghc-vector ghc-hashable))
+ (native-inputs (list ghc-hspec ghc-quickcheck ghc-quickcheck-instances
+ hspec-discover))
+ (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).")
+ (license license:bsd-3)))
+
(define-public ghc-vector-th-unbox
(package
(name "ghc-vector-th-unbox")
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 03/13] gnu: agda: Update to 2.6.3 and switch to git-fetch.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 01/13] gnu: Add ghc-peano Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 02/13] gnu: Add ghc-vector-hashtables Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 04/13] gnu: agda: Build info manual Josselin Poiret via Guix-patches via
` (10 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/agda.scm (agda): Update to 2.6.3, switch to fetching using git so
that doc files are included, and add new dependency ghc-vector-hashtables.
---
gnu/packages/agda.scm | 13 ++++++++-----
1 file changed, 8 insertions(+), 5 deletions(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 7128a3f108..252193de90 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -37,15 +37,17 @@ (define-module (gnu packages agda)
(define-public agda
(package
(name "agda")
- (version "2.6.2.2")
+ (version "2.6.3")
(source
(origin
- (method url-fetch)
- (uri (hackage-uri "Agda" version))
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/agda/agda.git")
+ (commit (string-append "v" version))))
+ (file-name (git-file-name name version))
(sha256
- (base32 "0yjjbhc593ylrm4mq4j01nkdvh7xqsg5in30wxj4y53vf5hkggp5"))))
+ (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q"))))
(build-system haskell-build-system)
- (properties '((upstream-name . "Agda")))
(inputs
(list ghc-aeson
ghc-alex
@@ -68,6 +70,7 @@ (define-public agda
ghc-strict
ghc-unordered-containers
ghc-uri-encode
+ ghc-vector-hashtables
ghc-zlib))
(arguments
(list #:modules `((guix build haskell-build-system)
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 04/13] gnu: agda: Build info manual.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (2 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 03/13] gnu: agda: Update to 2.6.3 and switch to git-fetch Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 05/13] gnu: emacs-agda2-mode: No longer inherit from agda Josselin Poiret via Guix-patches via
` (9 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/agda.scm (agda): Build the user manual as an info manual.
---
gnu/packages/agda.scm | 21 ++++++++++++++++++++-
1 file changed, 20 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 252193de90..eba48da0ff 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -25,6 +25,10 @@ (define-module (gnu packages agda)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
+ #:use-module (gnu packages imagemagick)
+ #:use-module (gnu packages python)
+ #:use-module (gnu packages sphinx)
+ #:use-module (gnu packages texinfo)
#:use-module (guix build-system emacs)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
@@ -72,6 +76,12 @@ (define-public agda
ghc-uri-encode
ghc-vector-hashtables
ghc-zlib))
+ (native-inputs
+ (list python
+ python-sphinx
+ python-sphinx-rtd-theme
+ texinfo
+ imagemagick))
(arguments
(list #:modules `((guix build haskell-build-system)
(guix build utils)
@@ -88,7 +98,16 @@ (define-public agda
(let ((agda-compiler (string-append #$output "/bin/agda")))
(for-each (cut invoke agda-compiler <>)
(find-files (string-append #$output "/share")
- "\\.agda$"))))))))
+ "\\.agda$")))))
+ (add-after 'agda-compile 'install-info
+ (lambda _
+ (with-directory-excursion "doc/user-manual"
+ (invoke "sphinx-build" "-b" "texinfo"
+ "." "_build_texinfo")
+ (with-directory-excursion "_build_texinfo"
+ (setenv "infodir" (string-append #$output
+ "/share/info"))
+ (invoke "make" "install-info"))))))))
(home-page "https://wiki.portal.chalmers.se/agda/")
(synopsis
"Dependently typed functional programming language and proof assistant")
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 05/13] gnu: emacs-agda2-mode: No longer inherit from agda.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (3 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 04/13] gnu: agda: Build info manual Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 06/13] gnu: emacs-agda2-mode: Switch to G-Exps Josselin Poiret via Guix-patches via
` (8 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/agda.scm (emacs-agda2-mode): Remove it. Made no sense, as we only
need the source, which we can refer to without inheriting the whole thing.
---
gnu/packages/agda.scm | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index eba48da0ff..69d6d22d32 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -128,10 +128,10 @@ (define-public agda
(define-public emacs-agda2-mode
(package
- (inherit agda)
(name "emacs-agda2-mode")
+ (version (package-version agda))
+ (source (package-source agda))
(build-system emacs-build-system)
- (inputs '())
(arguments
`(#:phases
(modify-phases %standard-phases
@@ -140,7 +140,8 @@ (define-public emacs-agda2-mode
(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.")))
+Agda. It also aids the input of Unicode characters.")
+ (license (package-license agda))))
(define-public agda-ial
(package
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 06/13] gnu: emacs-agda2-mode: Switch to G-Exps.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (4 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 05/13] gnu: emacs-agda2-mode: No longer inherit from agda Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 07/13] gnu: agda: Add AGDA_LIBDIRS search-path Josselin Poiret via Guix-patches via
` (7 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/agda.scm (emacs-agda2-mode): Switch it up.
---
gnu/packages/agda.scm | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 69d6d22d32..d94036939c 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -133,10 +133,11 @@ (define-public emacs-agda2-mode
(source (package-source agda))
(build-system emacs-build-system)
(arguments
- `(#:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'enter-elisp-dir
- (lambda _ (chdir "src/data/emacs-mode") #t)))))
+ (list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'enter-elisp-dir
+ (lambda _ (chdir "src/data/emacs-mode"))))))
(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
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 07/13] gnu: agda: Add AGDA_LIBDIRS search-path.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (5 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 06/13] gnu: emacs-agda2-mode: Switch to G-Exps Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 08/13] build-system/haskell: Export default-haskell Josselin Poiret via Guix-patches via
` (6 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/patches/agda-libdirs-env-variable.patch: New patch.
* gnu/local.mk (dist_patch_DATA): Register it.
* gnu/packages/agda.scm (agda): Patch agda, and add search path.
---
gnu/local.mk | 1 +
gnu/packages/agda.scm | 10 +++-
.../patches/agda-libdirs-env-variable.patch | 49 +++++++++++++++++++
3 files changed, 59 insertions(+), 1 deletion(-)
create mode 100644 gnu/packages/patches/agda-libdirs-env-variable.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 1a84e5b499..712649c5fc 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -880,6 +880,7 @@ dist_patch_DATA = \
%D%/packages/patches/aegisub-icu59-include-unistr.patch \
%D%/packages/patches/aegisub-boost68.patch \
%D%/packages/patches/aegisub-make43.patch \
+ %D%/packages/patches/agda-libdirs-env-variable.patch \
%D%/packages/patches/agg-am_c_prototype.patch \
%D%/packages/patches/agg-2.5-gcc8.patch \
%D%/packages/patches/akonadi-paths.patch \
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index d94036939c..17ea5b62be 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -22,6 +22,7 @@
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
(define-module (gnu packages agda)
+ #:use-module (gnu packages)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -50,7 +51,8 @@ (define-public agda
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
- (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q"))))
+ (base32 "1s7zd01i8pmvi90ywx497kc07z50nah7h0fc2dn6jzb132k5sh1q"))
+ (patches (search-patches "agda-libdirs-env-variable.patch"))))
(build-system haskell-build-system)
(inputs
(list ghc-aeson
@@ -108,6 +110,12 @@ (define-public agda
(setenv "infodir" (string-append #$output
"/share/info"))
(invoke "make" "install-info"))))))))
+ (search-paths
+ (list (search-path-specification
+ (variable "AGDA_LIBDIRS")
+ (files (list "lib/agda")))))
+ (native-search-paths
+ search-paths)
(home-page "https://wiki.portal.chalmers.se/agda/")
(synopsis
"Dependently typed functional programming language and proof assistant")
diff --git a/gnu/packages/patches/agda-libdirs-env-variable.patch b/gnu/packages/patches/agda-libdirs-env-variable.patch
new file mode 100644
index 0000000000..3b291358a6
--- /dev/null
+++ b/gnu/packages/patches/agda-libdirs-env-variable.patch
@@ -0,0 +1,49 @@
+From 457bc7438a4f0801dbf332fa2369248bddf5da0c Mon Sep 17 00:00:00 2001
+Message-Id: <457bc7438a4f0801dbf332fa2369248bddf5da0c.1678309546.git.dev@jpoiret.xyz>
+From: Josselin Poiret <dev@jpoiret.xyz>
+Date: Wed, 8 Mar 2023 18:31:52 +0100
+Subject: [PATCH] Add environment variable for library directories
+
+AGDA_LIBDIRS is a new environment colon-separated variable for site libraries.
+Agda will look for .agda-lib files directly inside direct descendants of these.
+---
+ src/full/Agda/Interaction/Library.hs | 16 ++++++++++++++--
+ 1 file changed, 14 insertions(+), 2 deletions(-)
+
+diff --git a/src/full/Agda/Interaction/Library.hs b/src/full/Agda/Interaction/Library.hs
+index 09c1f2a82..774cc3e74 100644
+--- a/src/full/Agda/Interaction/Library.hs
++++ b/src/full/Agda/Interaction/Library.hs
+@@ -323,13 +323,25 @@ getInstalledLibraries overrideLibFile = mkLibM [] $ do
+ raiseErrors' [ LibrariesFileNotFound theOverrideLibFile ]
+ return []
+ Right file -> do
+- if not (lfExists file) then return [] else do
++ siteLibDirs <- liftIO $ fromMaybe [] . fmap splitAtColon . lookup "AGDA_LIBDIRS" <$> getEnvironment
++ siteLibs <- liftIO $ concat <$> mapM findSiteLibs siteLibDirs
++ if not (lfExists file) then parseLibFiles Nothing $ nubOn snd ((0,) <$> siteLibs) else do
+ ls <- liftIO $ stripCommentLines <$> UTF8.readFile (lfPath file)
+ files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ]
+- parseLibFiles (Just file) $ nubOn snd files
++ parseLibFiles (Just file) $ nubOn snd (files ++ fmap (0,) siteLibs)
+ `catchIO` \ e -> do
+ raiseErrors' [ ReadError e "Failed to read installed libraries." ]
+ return []
++ where splitAtColon :: String -> [String]
++ splitAtColon "" = []
++ splitAtColon str = case break (==':') str of
++ (a, _:b) -> a : splitAtColon b
++ (a, "") -> [a]
++ findSiteLibs :: String -> IO [String]
++ findSiteLibs dir = do
++ subDirs <- filterM doesDirectoryExist =<< map (dir </>) <$> listDirectory dir
++ subFiles <- mapM (\dir -> map (dir </>) <$> listDirectory dir) subDirs
++ return $ concatMap (filter (List.isSuffixOf ".agda-lib")) subFiles
+
+ -- | Parse the given library files.
+ --
+
+base-commit: 183534bc41af5a53daf685122997dc98883f2be2
+--
+2.39.1
+
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 08/13] build-system/haskell: Export default-haskell.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (6 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 07/13] gnu: agda: Add AGDA_LIBDIRS search-path Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 09/13] build-system: New agda-build-system Josselin Poiret via Guix-patches via
` (5 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* guix/build-system/haskell.scm: Export default-haskell.
---
guix/build-system/haskell.scm | 1 +
1 file changed, 1 insertion(+)
diff --git a/guix/build-system/haskell.scm b/guix/build-system/haskell.scm
index b8858421c2..f8568e33db 100644
--- a/guix/build-system/haskell.scm
+++ b/guix/build-system/haskell.scm
@@ -33,6 +33,7 @@ (define-module (guix build-system haskell)
#:use-module (ice-9 match)
#:use-module (srfi srfi-1)
#:export (hackage-uri
+ default-haskell
%haskell-build-system-modules
haskell-build
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 09/13] build-system: New agda-build-system.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (7 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 08/13] build-system/haskell: Export default-haskell Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 10/13] gnu: Add agda-stdlib Josselin Poiret via Guix-patches via
` (4 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* guix/build-system/agda.scm: New file.
* guix/build/agda-build-system.scm: New file.
* Makefile.am (MODULES): Register them.
* doc/guix.texi (Build Systems): Add documentation for agda-build-system.
---
Makefile.am | 2 +
doc/guix.texi | 21 ++++++
guix/build-system/agda.scm | 105 +++++++++++++++++++++++++++++
guix/build/agda-build-system.scm | 110 +++++++++++++++++++++++++++++++
4 files changed, 238 insertions(+)
create mode 100644 guix/build-system/agda.scm
create mode 100644 guix/build/agda-build-system.scm
diff --git a/Makefile.am b/Makefile.am
index a763a7e305..9d137cfbb3 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -140,6 +140,7 @@ MODULES = \
guix/platforms/riscv.scm \
guix/platforms/x86.scm \
guix/build-system.scm \
+ guix/build-system/agda.scm \
guix/build-system/android-ndk.scm \
guix/build-system/ant.scm \
guix/build-system/cargo.scm \
@@ -195,6 +196,7 @@ MODULES = \
guix/diagnostics.scm \
guix/ui.scm \
guix/status.scm \
+ guix/build/agda-build-system.scm \
guix/build/android-ndk-build-system.scm \
guix/build/ant-build-system.scm \
guix/build/download.scm \
diff --git a/doc/guix.texi b/doc/guix.texi
index 46e7fd3908..01cd199f0a 100644
--- a/doc/guix.texi
+++ b/doc/guix.texi
@@ -8885,6 +8885,27 @@ of @code{gnu-build-system}, and differ mainly in the set of inputs
implicitly added to the build process, and in the list of phases
executed. Some of these build systems are listed below.
+@defvar agda-build-system
+This variable is exported by @code{(guix build-system agda)}. It
+implements a build procedure for Agda libraries.
+
+It adds @code{agda} to the set of inputs. A different Agda can be
+specified with the @code{#:agda} key.
+
+The @code{#:plan} key is a list of cons cells @code{(@var{regexp}
+. @var{parameters})}, where @var{regexp} is a regexp that should match
+the @code{.agda} files to build, and @var{parameters} is an optional
+list of parameters that will be passed to @code{agda} when type-checking
+it.
+
+When the library uses Haskell to generate a file containing all imports,
+the convenience @code{#:gnu-and-haskell?} can be set to @code{#t} to add
+@code{ghc} and the standard inputs of @code{gnu-build-system} to the
+input list. You will still need to manually add a phase or tweak the
+@code{'build} phase, as in the definition of @code{agda-stdlib}.
+
+@end defvar
+
@defvar ant-build-system
This variable is exported by @code{(guix build-system ant)}. It
implements the build procedure for Java packages that can be built with
diff --git a/guix/build-system/agda.scm b/guix/build-system/agda.scm
new file mode 100644
index 0000000000..cf96ffaa68
--- /dev/null
+++ b/guix/build-system/agda.scm
@@ -0,0 +1,105 @@
+(define-module (guix build-system agda)
+ #:use-module (guix build-system)
+ #:use-module (guix build-system gnu)
+ #:use-module (guix build-system haskell)
+ #:use-module (guix gexp)
+ #:use-module (guix monads)
+ #:use-module (guix packages)
+ #:use-module (guix search-paths)
+ #:use-module (guix store)
+ #:use-module (guix utils)
+ #:export (default-agda
+
+ %agda-build-system-modules
+ agda-build-system))
+
+(define (default-agda)
+ ;; Lazily resolve the binding to avoid a circular dependency.
+ (let ((agda (resolve-interface '(gnu packages agda))))
+ (module-ref agda 'agda)))
+
+(define %agda-build-system-modules
+ `((guix build agda-build-system)
+ ,@%gnu-build-system-modules))
+
+(define %default-modules
+ '((guix build agda-build-system)
+ (guix build utils)))
+
+(define* (lower name
+ #:key source inputs native-inputs outputs system target
+ (agda (default-agda))
+ gnu-and-haskell?
+ #:allow-other-keys
+ #:rest arguments)
+ "Return a bag for NAME."
+ (define private-keywords
+ '(#:target #:agda #:gnu-and-haskell? #:inputs #:native-inputs))
+
+ ;; TODO: cross-compilation support
+ (and (not target)
+ (bag
+ (name name)
+ (system system)
+ (host-inputs `(,@(if source
+ `(("source" ,source))
+ '())
+ ,@inputs))
+ (build-inputs `(("agda" ,agda)
+ ,@(if gnu-and-haskell?
+ (cons*
+ (list "ghc" (default-haskell))
+ (standard-packages))
+ '())
+ ,(assoc "locales" (standard-packages))
+ ,@native-inputs))
+ (outputs outputs)
+ (build agda-build)
+ (arguments (strip-keyword-arguments private-keywords arguments)))))
+
+(define* (agda-build name inputs
+ #:key
+ source
+ (phases '%standard-phases)
+ (outputs '("out"))
+ (search-paths '())
+ (unpack-path "")
+ (build-flags ''())
+ (tests? #t)
+ (system (%current-system))
+ (guile #f)
+ plan
+ (extra-files '("^\\./.*\\.agda-lib$"))
+ (imported-modules %agda-build-system-modules)
+ (modules %default-modules))
+ (define builder
+ (with-imported-modules imported-modules
+ #~(begin
+ (use-modules #$@(sexp->gexp modules))
+ (agda-build #:name #$name
+ #:source #+source
+ #:system #$system
+ #:phases #$phases
+ #:outputs #$(outputs->gexp outputs)
+ #:search-paths '#$(sexp->gexp
+ (map search-path-specification->sexp
+ search-paths))
+ #:unpack-path #$unpack-path
+ #:build-flags #$build-flags
+ #:tests? #$tests?
+ #:inputs #$(input-tuples->gexp inputs)
+ #:plan '#$plan
+ #:extra-files '#$extra-files))))
+
+ (mlet %store-monad ((guile (package->derivation (or guile (default-guile))
+ system #:graft? #f)))
+ (gexp->derivation name builder
+ #:system system
+ #:guile-for-build guile)))
+
+(define agda-build-system
+ (build-system
+ (name 'agda)
+ (description
+ "Build system for Agda libraries")
+ (lower lower)))
diff --git a/guix/build/agda-build-system.scm b/guix/build/agda-build-system.scm
new file mode 100644
index 0000000000..1d7e80d61b
--- /dev/null
+++ b/guix/build/agda-build-system.scm
@@ -0,0 +1,110 @@
+(define-module (guix build agda-build-system)
+ #:use-module ((guix build gnu-build-system) #:prefix gnu:)
+ #:use-module (guix build utils)
+ #:use-module (srfi srfi-26)
+ #:use-module (srfi srfi-34)
+ #:use-module (srfi srfi-35)
+ #:use-module (ice-9 ftw)
+ #:use-module (ice-9 match)
+ #:export (%standard-phases
+ agda-build))
+
+(define* (set-locpath #:key inputs native-inputs #:allow-other-keys)
+ (let ((locales (assoc-ref (or native-inputs inputs) "locales")))
+ (setenv "GUIX_LOCPATH" (string-append locales "/lib/locale"))))
+
+(define %agda-possible-extensions
+ (cons
+ ".agda"
+ (map (cute string-append ".lagda" <>)
+ '(""
+ ".md"
+ ".org"
+ ".rst"
+ ".tex"))))
+
+(define (pattern-predicate pattern)
+ (define compiled-rx (make-regexp pattern))
+ (lambda (file stat)
+ (regexp-exec compiled-rx file)))
+
+(define* (build #:key plan #:allow-other-keys)
+ (for-each
+ (match-lambda
+ ((pattern . options)
+ (for-each
+ (lambda (file)
+ (apply invoke (cons* "agda" file options)))
+ (let ((files (find-files "." (pattern-predicate pattern))))
+ (if (null? files)
+ (raise
+ (make-compound-condition
+ (condition
+ (&message
+ (message (format #f "Plan pattern `~a' did not match any files"
+ pattern))))
+ (condition
+ (&error))))
+ files))))
+ (x
+ (raise
+ (make-compound-condition
+ (condition
+ (&message
+ (message (format #f "Malformed plan element `~a'" x))))
+ (condition
+ (&error))))))
+ plan))
+
+(define* (install #:key outputs name extra-files #:allow-other-keys)
+ (define libdir (string-append (assoc-ref outputs "out") "/lib/agda/" name))
+ (define agda-version
+ (car (scandir "./_build/"
+ (lambda (entry)
+ (not (member entry '("." "..")))))))
+ (define agdai-files
+ (with-directory-excursion
+ (string-join (list "." "_build" agda-version "agda") "/")
+ (find-files ".")))
+ (define (install-source agdai)
+ (define dir (dirname agdai))
+ ;; Drop .agdai
+ (define no-ext (string-drop-right agdai 6))
+ (define source
+ (match (filter file-exists? (map (cute string-append no-ext <>)
+ %agda-possible-extensions))
+ ((single) single)
+ (res (raise
+ (make-compound-condition
+ (condition
+ (&message
+ (message
+ (format #f
+ "Cannot find unique source file for agdai file `~a`, got `~a`"
+ agdai res))))
+ (condition
+ (&error)))))))
+ (install-file source (string-append libdir "/" dir)))
+ (for-each install-source agdai-files)
+ (copy-recursively "_build" (string-append libdir "/_build"))
+ (for-each
+ (lambda (pattern)
+ (for-each
+ (lambda (file)
+ (install-file file libdir))
+ (find-files "." (pattern-predicate pattern))))
+ extra-files))
+
+(define %standard-phases
+ (modify-phases gnu:%standard-phases
+ (add-before 'install-locale 'set-locpath set-locpath)
+ (delete 'bootstrap)
+ (delete 'configure)
+ (replace 'build build)
+ (delete 'check) ;; No universal checker
+ (replace 'install install)))
+
+(define* (agda-build #:key inputs (phases %standard-phases)
+ #:allow-other-keys #:rest args)
+ "Build the given Agda package, applying all of PHASES in order."
+ (apply gnu:gnu-build #:inputs inputs #:phases phases args))
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 10/13] gnu: Add agda-stdlib.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (8 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 09/13] build-system: New agda-build-system Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 11/13] gnu: Add agda-categories Josselin Poiret via Guix-patches via
` (3 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/patches/agda-stdlib-use-runhaskell.patch: New patch.
* gnu/local.mk (dist_patch_DATA): Register it.
* gnu/packages/agda.scm: New variable agda-stdlib.
---
gnu/local.mk | 1 +
gnu/packages/agda.scm | 37 +++++++++++++++++++
.../patches/agda-stdlib-use-runhaskell.patch | 28 ++++++++++++++
3 files changed, 66 insertions(+)
create mode 100644 gnu/packages/patches/agda-stdlib-use-runhaskell.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 712649c5fc..0a1c4dfb24 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -881,6 +881,7 @@ dist_patch_DATA = \
%D%/packages/patches/aegisub-boost68.patch \
%D%/packages/patches/aegisub-make43.patch \
%D%/packages/patches/agda-libdirs-env-variable.patch \
+ %D%/packages/patches/agda-stdlib-use-runhaskell.patch \
%D%/packages/patches/agg-am_c_prototype.patch \
%D%/packages/patches/agg-2.5-gcc8.patch \
%D%/packages/patches/akonadi-paths.patch \
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 17ea5b62be..a6ff01b737 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -30,6 +30,7 @@ (define-module (gnu packages agda)
#:use-module (gnu packages python)
#:use-module (gnu packages sphinx)
#:use-module (gnu packages texinfo)
+ #:use-module (guix build-system agda)
#:use-module (guix build-system emacs)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
@@ -193,3 +194,39 @@ (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
+ (package
+ (name "agda-stdlib")
+ (version "1.7.2")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/agda/agda-stdlib")
+ (commit (string-append "v" version))))
+ (sha256
+ (base32
+ "065hf24xjpciwdrvk4isslgcgi01q0k93ql0y1sjqqvy5ryg5xmy"))))
+ (build-system agda-build-system)
+ (arguments
+ (list
+ #:plan '(("^\\./README.agda$" "-i."))
+ #:gnu-and-haskell? #t
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-before 'build 'generate-everything
+ (lambda* (#:key inputs native-inputs #:allow-other-keys)
+ (invoke
+ (search-input-file (or native-inputs inputs) "/bin/runhaskell")
+ "GenerateEverything.hs"))))))
+ (native-inputs (list ghc-filemanip))
+ (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)))
+
diff --git a/gnu/packages/patches/agda-stdlib-use-runhaskell.patch b/gnu/packages/patches/agda-stdlib-use-runhaskell.patch
new file mode 100644
index 0000000000..21ce16689f
--- /dev/null
+++ b/gnu/packages/patches/agda-stdlib-use-runhaskell.patch
@@ -0,0 +1,28 @@
+From 3dc3c0856906d25bb697a4480a8457a69637cd51 Mon Sep 17 00:00:00 2001
+Message-Id: <3dc3c0856906d25bb697a4480a8457a69637cd51.1682798848.git.dev@jpoiret.xyz>
+From: Josselin Poiret <dev@jpoiret.xyz>
+Date: Sat, 29 Apr 2023 22:06:55 +0200
+Subject: [PATCH] Makefile: use runhaskell instead of cabal
+
+From: Josselin Poiret <dev@jpoiret.xyz>
+
+---
+ GNUmakefile | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/GNUmakefile b/GNUmakefile
+index c5d886e03..f3cb2a1e7 100644
+--- a/GNUmakefile
++++ b/GNUmakefile
+@@ -21,7 +21,7 @@ Everything.agda:
+ # command `cabal install` is needed by cabal-install <= 2.4.*. I did
+ # not found any problem running both commands with different versions
+ # of cabal-install. See Issue #1001.
+- cabal run GenerateEverything
++ runhaskell GenerateEverything
+
+ .PHONY: listings
+ listings: Everything.agda
+--
+2.39.2
+
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 11/13] gnu: Add agda-categories.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (9 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 10/13] gnu: Add agda-stdlib Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 12/13] gnu: Add agda-cubical Josselin Poiret via Guix-patches via
` (2 subsequent siblings)
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/patches/agda-categories-bump-stdlib-version.patch
* gnu/packages/patches/agda-categories-remove-incompatible-flags.patch
* gnu/packages/patches/agda-categories-use-find.patch: New patches.
* gnu/local.mk (dist_patch_DATA): Register them.
* gnu/packages/agda.scm: New variable agda-categories.
---
gnu/local.mk | 3 ++
gnu/packages/agda.scm | 35 ++++++++++++++++
.../agda-categories-bump-stdlib-version.patch | 42 +++++++++++++++++++
...categories-remove-incompatible-flags.patch | 31 ++++++++++++++
.../patches/agda-categories-use-find.patch | 31 ++++++++++++++
5 files changed, 142 insertions(+)
create mode 100644 gnu/packages/patches/agda-categories-bump-stdlib-version.patch
create mode 100644 gnu/packages/patches/agda-categories-remove-incompatible-flags.patch
create mode 100644 gnu/packages/patches/agda-categories-use-find.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 0a1c4dfb24..4193146862 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -880,6 +880,9 @@ dist_patch_DATA = \
%D%/packages/patches/aegisub-icu59-include-unistr.patch \
%D%/packages/patches/aegisub-boost68.patch \
%D%/packages/patches/aegisub-make43.patch \
+ %D%/packages/patches/agda-categories-bump-stdlib-version.patch \
+ %D%/packages/patches/agda-categories-remove-incompatible-flags.patch \
+ %D%/packages/patches/agda-categories-use-find.patch \
%D%/packages/patches/agda-libdirs-env-variable.patch \
%D%/packages/patches/agda-stdlib-use-runhaskell.patch \
%D%/packages/patches/agg-am_c_prototype.patch \
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index a6ff01b737..1068d8734f 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -230,3 +230,38 @@ (define-public agda-stdlib
(home-page "https://wiki.portal.chalmers.se/agda/pmwiki.php")
(license license:expat)))
+(define-public agda-categories
+ ;; Upstream hasn't released in a very long time, especially not against
+ ;; 2.6.3.
+ (let* ((revision "1")
+ (commit "20397e93a60ed1439ed57ee76ae377c66a5eb8d9"))
+ (package
+ (name "agda-categories")
+ (version (git-version "0.4" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/agda/agda-categories.git")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0q4dqvs4ig138wghlglz37ay5i524gk6k5x476ki5mnxc603bmqy"))
+ (patches (search-patches "agda-categories-bump-stdlib-version.patch"
+ "agda-categories-remove-incompatible-flags.patch"
+ "agda-categories-use-find.patch"))))
+ (build-system agda-build-system)
+ (arguments
+ (list
+ #:gnu-and-haskell? #t
+ #:phases
+ #~(modify-phases %standard-phases
+ (replace 'build
+ (lambda _
+ (invoke "make"))))))
+ (propagated-inputs
+ (list agda-stdlib))
+ (synopsis "A new Categories library for Agda")
+ (description "A new Categories library for Agda")
+ (home-page "https://github.com/agda/agda-categories")
+ (license license:expat))))
diff --git a/gnu/packages/patches/agda-categories-bump-stdlib-version.patch b/gnu/packages/patches/agda-categories-bump-stdlib-version.patch
new file mode 100644
index 0000000000..2e78cc1446
--- /dev/null
+++ b/gnu/packages/patches/agda-categories-bump-stdlib-version.patch
@@ -0,0 +1,42 @@
+From 080eae2adc1b0e8f1829c4138b3d462218a02f36 Mon Sep 17 00:00:00 2001
+Message-Id: <080eae2adc1b0e8f1829c4138b3d462218a02f36.1682840777.git.dev@jpoiret.xyz>
+From: Josselin Poiret <dev@jpoiret.xyz>
+Date: Sun, 30 Apr 2023 09:32:59 +0200
+Subject: [PATCH] Bump Agda to 2.6.3 and stdlib to 1.7.2
+
+From: Josselin Poiret <dev@jpoiret.xyz>
+
+---
+ .github/workflows/ci-ubuntu.yml | 4 ++--
+ agda-categories.agda-lib | 2 +-
+ 2 files changed, 3 insertions(+), 3 deletions(-)
+
+diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
+index ab26835d..25604420 100644
+--- a/.github/workflows/ci-ubuntu.yml
++++ b/.github/workflows/ci-ubuntu.yml
+@@ -45,8 +45,8 @@ on:
+ ########################################################################
+
+ env:
+- AGDA_COMMIT: tags/v2.6.2
+- STDLIB_VERSION: 1.7.1
++ AGDA_COMMIT: tags/v2.6.3
++ STDLIB_VERSION: 1.7.2
+
+ GHC_VERSION: 8.6.5
+ CABAL_VERSION: 3.2.0.0
+diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib
+index 186e350b..5b19c405 100644
+--- a/agda-categories.agda-lib
++++ b/agda-categories.agda-lib
+@@ -1,3 +1,3 @@
+ name: agda-categories
+-depend: standard-library-1.7.1
++depend: standard-library-1.7.2
+ include: src/
+
+base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9
+--
+2.39.2
+
diff --git a/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch b/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch
new file mode 100644
index 0000000000..dc33af7cf9
--- /dev/null
+++ b/gnu/packages/patches/agda-categories-remove-incompatible-flags.patch
@@ -0,0 +1,31 @@
+From 3d73d59617281c6ae9c19032eae381ff77fd2e65 Mon Sep 17 00:00:00 2001
+Message-Id: <3d73d59617281c6ae9c19032eae381ff77fd2e65.1682841188.git.dev@jpoiret.xyz>
+From: Josselin Poiret <dev@jpoiret.xyz>
+Date: Sun, 30 Apr 2023 09:51:12 +0200
+Subject: [PATCH] Remove stdlib-incompatible flags
+
+From: Josselin Poiret <dev@jpoiret.xyz>
+
+---
+ Makefile | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/Makefile b/Makefile
+index 68846579..ba5923a2 100644
+--- a/Makefile
++++ b/Makefile
+@@ -1,6 +1,6 @@
+ .PHONY: test Everything.agda clean
+
+-OTHEROPTS = --auto-inline -Werror
++OTHEROPTS =
+
+ RTSARGS = +RTS -M6G -A128M -RTS ${OTHEROPTS}
+
+
+base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9
+prerequisite-patch-id: da10df58fa86d08b31174a01db7b9a02377aba55
+prerequisite-patch-id: 508dabd923ba9ac1ee4d8dab6697432b4bd8ba18
+--
+2.39.2
+
diff --git a/gnu/packages/patches/agda-categories-use-find.patch b/gnu/packages/patches/agda-categories-use-find.patch
new file mode 100644
index 0000000000..772352a0cb
--- /dev/null
+++ b/gnu/packages/patches/agda-categories-use-find.patch
@@ -0,0 +1,31 @@
+From 53922aedd81d5111d9007b41235aa12eaa2a863d Mon Sep 17 00:00:00 2001
+Message-Id: <53922aedd81d5111d9007b41235aa12eaa2a863d.1682840933.git.dev@jpoiret.xyz>
+From: Josselin Poiret <dev@jpoiret.xyz>
+Date: Sun, 30 Apr 2023 09:48:21 +0200
+Subject: [PATCH] Use find instead of git ls-tree in Makefile
+
+From: Josselin Poiret <dev@jpoiret.xyz>
+
+---
+ Makefile | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/Makefile b/Makefile
+index 158802d1..68846579 100644
+--- a/Makefile
++++ b/Makefile
+@@ -11,7 +11,7 @@ html: Everything.agda
+ agda ${RTSARGS} --html -i. Everything.agda
+
+ Everything.agda:
+- git ls-tree --full-tree -r --name-only HEAD | grep '^src/[^\.]*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda
++ find src -iname '*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda
+
+ clean:
+ find . -name '*.agdai' -exec rm \{\} \;
+
+base-commit: 20397e93a60ed1439ed57ee76ae377c66a5eb8d9
+prerequisite-patch-id: da10df58fa86d08b31174a01db7b9a02377aba55
+--
+2.39.2
+
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 12/13] gnu: Add agda-cubical.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (10 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 11/13] gnu: Add agda-categories Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-04-30 10:53 ` [bug#61915] [PATCH v2 13/13] gnu: Add agda-1lab Josselin Poiret via Guix-patches via
2023-06-04 9:47 ` bug#61915: [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/agda.scm: New variable agda-cubical.
---
gnu/packages/agda.scm | 33 +++++++++++++++++++++++++++++++++
1 file changed, 33 insertions(+)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 1068d8734f..e75386c990 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -265,3 +265,36 @@ (define-public agda-categories
(description "A new Categories library for Agda")
(home-page "https://github.com/agda/agda-categories")
(license license:expat))))
+
+(define-public agda-cubical
+ ;; Upstream's HEAD follows the latest Agda release, but they don't release
+ ;; until a newer Agda release comes up, so their releases are always one
+ ;; version late.
+ (let* ((revision "1")
+ (commit "3dc3cd12579544c8c1c1d2c5f64fd8d577fd3d66"))
+ (package
+ (name "agda-cubical")
+ (version (git-version "0.4" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/agda/cubical.git")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "1b40adjgwrrdarzk0yiy2jmjgmf455ax6z70hfzdgc6j06vdb6mg"))))
+ (build-system agda-build-system)
+ (arguments
+ (list
+ #:gnu-and-haskell? #t
+ #:phases
+ #~(modify-phases %standard-phases
+ (replace 'build
+ (lambda _
+ (invoke "make"))))))
+ (synopsis "A standard library for Cubical Agda")
+ (description "A standard library for Cubical Agda, comparable to
+agda-stdlib but using cubical methods.")
+ (home-page "https://github.com/agda/cubical")
+ (license license:expat))))
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* [bug#61915] [PATCH v2 13/13] gnu: Add agda-1lab.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (11 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 12/13] gnu: Add agda-cubical Josselin Poiret via Guix-patches via
@ 2023-04-30 10:53 ` Josselin Poiret via Guix-patches via
2023-06-04 9:47 ` bug#61915: [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-04-30 10:53 UTC (permalink / raw)
To: Josselin Poiret, Simon Tournier, 61915
From: Josselin Poiret <dev@jpoiret.xyz>
* gnu/packages/agda.scm: New variable agda-1lab.
---
gnu/packages/agda.scm | 29 +++++++++++++++++++++++++++++
1 file changed, 29 insertions(+)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index e75386c990..2116ceced3 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -298,3 +298,32 @@ (define-public agda-cubical
agda-stdlib but using cubical methods.")
(home-page "https://github.com/agda/cubical")
(license license:expat))))
+
+(define-public agda-1lab
+ ;; Upstream doesn't do releases (yet). Use a commit that builds with 2.6.3,
+ ;; since they use Agda HEAD.
+ (let* ((revision "1")
+ (commit "47ca1d23640a6f49a3abe3c2fe27738bcc10c9c6"))
+ (package
+ (name "agda-1lab")
+ (version (git-version "0.0" revision commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/plt-amy/1lab.git")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "0j7mp6c0xd0849skdxzncklkxynxnyfrbpcjv4qp5p1xfn0dnfqx"))))
+ (build-system agda-build-system)
+ (arguments
+ (list #:plan '(("src/index\\.lagda\\.md$"))))
+ (synopsis "Areference resource for mathematics done in Homotopy Type Theory")
+ (description "A formalised, cross-linked reference resource for
+mathematics done in Homotopy Type Theory. Unlike the HoTT book, the 1lab is
+not a “linear” resource: Concepts are presented as a directed graph, with
+links indicating dependencies.")
+ (home-page "https://1lab.dev")
+ (license license:agpl3))))
--
2.39.2
^ permalink raw reply related [flat|nested] 22+ messages in thread* bug#61915: [PATCH v2 00/13] Update agda, add build-system and libraries.
2023-04-30 10:53 ` [bug#61915] [PATCH v2 00/13] Update agda, add build-system and libraries Josselin Poiret via Guix-patches via
` (12 preceding siblings ...)
2023-04-30 10:53 ` [bug#61915] [PATCH v2 13/13] gnu: Add agda-1lab Josselin Poiret via Guix-patches via
@ 2023-06-04 9:47 ` Josselin Poiret via Guix-patches via
13 siblings, 0 replies; 22+ messages in thread
From: Josselin Poiret via Guix-patches via @ 2023-06-04 9:47 UTC (permalink / raw)
To: 61915-done
[-- Attachment #1: Type: text/plain, Size: 870 bytes --]
Hi everyone,
Josselin Poiret <dev@jpoiret.xyz> writes:
> Josselin Poiret (13):
> gnu: Add ghc-peano.
> gnu: Add ghc-vector-hashtables.
> gnu: agda: Update to 2.6.3 and switch to git-fetch.
> gnu: agda: Build info manual.
> gnu: emacs-agda2-mode: No longer inherit from agda.
> gnu: emacs-agda2-mode: Switch to G-Exps.
> gnu: agda: Add AGDA_LIBDIRS search-path.
> build-system/haskell: Export default-haskell.
> build-system: New agda-build-system.
> gnu: Add agda-stdlib.
> gnu: Add agda-categories.
> gnu: Add agda-cubical.
> gnu: Add agda-1lab.
Pushed as e198fe4e942c58136dd4cb8ebf49cade58a8f5e3 with some additions,
notably refactoring some descriptions that the linter didn't like, and
updating agda-categories to the new released version, agda-cubical and
agda-ial to a new commit.
Best,
--
Josselin Poiret
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 682 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread