* [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode.
@ 2018-07-21 15:59 Alex ter Weele
[not found] ` <handler.32235.B.15321888082039.ack@debbugs.gnu.org>
0 siblings, 1 reply; 6+ messages in thread
From: Alex ter Weele @ 2018-07-21 15:59 UTC (permalink / raw)
To: 32235
^ permalink raw reply [flat|nested] 6+ messages in thread
* [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode.
[not found] ` <handler.32235.B.15321888082039.ack@debbugs.gnu.org>
@ 2018-07-21 16:13 ` Alex ter Weele
2018-07-22 14:40 ` Marius Bakke
0 siblings, 1 reply; 6+ messages in thread
From: Alex ter Weele @ 2018-07-21 16:13 UTC (permalink / raw)
To: 32235
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: 0001-gnu-agda-Compile-.agda-files.patch --]
[-- Type: text/x-patch, Size: 1976 bytes --]
From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele@gmail.com>
Date: Fri, 20 Jul 2018 21:35:14 -0500
Subject: [PATCH 1/2] gnu: agda: Compile .agda files.
* gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files.
---
gnu/packages/agda.scm | 23 +++++++++++++++++++++++
1 file changed, 23 insertions(+)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 6aa230116..f7474aae3 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -67,6 +67,29 @@
("ghc-text" ,ghc-text)
("ghc-unordered-containers" ,ghc-unordered-containers)
("ghc-zlib" ,ghc-zlib)))
+ (arguments
+ `(#:modules ((guix build haskell-build-system)
+ (guix build utils)
+ (srfi srfi-26))
+ #:phases
+ (modify-phases %standard-phases
+ (add-after 'compile 'agda-compile
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (agda-compiler (string-append out "/bin/agda"))
+ (agda-files-path (string-append
+ out
+ "/share/x86_64-linux-ghc-8.0.2/Agda-"
+ ,version
+ "/lib/prim/Agda/"))
+ (agda-files (append
+ (find-files agda-files-path "\\.agda$")
+ (find-files (string-append
+ agda-files-path
+ "Builtin")
+ "\\.agda$"))))
+ (for-each (cut invoke agda-compiler <>) agda-files)
+ #t))))))
(home-page "http://wiki.portal.chalmers.se/agda/")
(synopsis
"Dependently typed functional programming language and proof assistant")
--
2.18.0
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0002-gnu-Add-emacs-agda2-mode.patch --]
[-- Type: text/x-patch, Size: 1600 bytes --]
From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele@gmail.com>
Date: Sat, 21 Jul 2018 10:57:35 -0500
Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode
* gnu/packages/agda.scm (emacs-agda2-mode): New variable.
---
gnu/packages/agda.scm | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index f7474aae3..1a2078c07 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -20,6 +20,7 @@
#:use-module (gnu packages haskell)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
+ #:use-module (guix build-system emacs)
#:use-module (guix build-system haskell)
#:use-module (guix build-system trivial)
#:use-module (guix download)
@@ -107,3 +108,18 @@ such as Coq, Epigram and NuPRL.")
;; Agda is distributed under the MIT license, and a couple of
;; source files are BSD-3. See LICENSE for details.
(license (list license:expat license:bsd-3))))
+
+(define-public emacs-agda2-mode
+ (package
+ (inherit agda)
+ (name "agda2-mode")
+ (build-system emacs-build-system)
+ (arguments
+ `(#:phases
+ (modify-phases %standard-phases
+ (add-after 'unpack 'enter-elisp-dir
+ (lambda _ (chdir "src/data/emacs-mode"))))))
+ (home-page "https://agda.readthdocs.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.")))
--
2.18.0
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode.
2018-07-21 16:13 ` Alex ter Weele
@ 2018-07-22 14:40 ` Marius Bakke
2018-07-28 2:39 ` Alex ter Weele
0 siblings, 1 reply; 6+ messages in thread
From: Marius Bakke @ 2018-07-22 14:40 UTC (permalink / raw)
To: Alex ter Weele, 32235
[-- Attachment #1: Type: text/plain, Size: 2439 bytes --]
Alex ter Weele <alex.ter.weele@gmail.com> writes:
> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
> From: Alex ter Weele <alex.ter.weele@gmail.com>
> Date: Fri, 20 Jul 2018 21:35:14 -0500
> Subject: [PATCH 1/2] gnu: agda: Compile .agda files.
>
> * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files.
[...]
> + (arguments
> + `(#:modules ((guix build haskell-build-system)
> + (guix build utils)
> + (srfi srfi-26))
> + #:phases
> + (modify-phases %standard-phases
> + (add-after 'compile 'agda-compile
> + (lambda* (#:key outputs #:allow-other-keys)
> + (let* ((out (assoc-ref outputs "out"))
> + (agda-compiler (string-append out "/bin/agda"))
> + (agda-files-path (string-append
> + out
> + "/share/x86_64-linux-ghc-8.0.2/Agda-"
This is unfortunate, since it hard-codes both architecture and GHC
version. Can you think of another method to find these files?
Are there ".agda" files elsewhere under "/share"? Could the find-files
invokation below simply search "out/share", for example?
Worst case scenario we'll have to dynamically generate that GHC path
based on architecture and version, but hoping there's another way.
> + ,version
> + "/lib/prim/Agda/"))
> + (agda-files (append
> + (find-files agda-files-path "\\.agda$")
> + (find-files (string-append
> + agda-files-path
> + "Builtin")
> + "\\.agda$"))))
(find-files ...) recurses through subdirectories, are you sure adding an
extra pass for "Builtin/*.agda" makes a difference here?
> + (for-each (cut invoke agda-compiler <>) agda-files)
> + #t))))))
> (home-page "http://wiki.portal.chalmers.se/agda/")
Otherwise LGTM.
[...]
> From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001
> From: Alex ter Weele <alex.ter.weele@gmail.com>
> Date: Sat, 21 Jul 2018 10:57:35 -0500
> Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode
>
> * gnu/packages/agda.scm (emacs-agda2-mode): New variable.
LGTM!
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 487 bytes --]
^ permalink raw reply [flat|nested] 6+ messages in thread
* [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode.
2018-07-22 14:40 ` Marius Bakke
@ 2018-07-28 2:39 ` Alex ter Weele
2018-07-28 15:42 ` Marius Bakke
0 siblings, 1 reply; 6+ messages in thread
From: Alex ter Weele @ 2018-07-28 2:39 UTC (permalink / raw)
To: Marius Bakke; +Cc: Alex ter Weele, 32235
[-- Attachment #1: Type: text/plain, Size: 2658 bytes --]
Marius Bakke <mbakke@fastmail.com> writes:
> Alex ter Weele <alex.ter.weele@gmail.com> writes:
>
>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
>> From: Alex ter Weele <alex.ter.weele@gmail.com>
>> Date: Fri, 20 Jul 2018 21:35:14 -0500
>> Subject: [PATCH 1/2] gnu: agda: Compile .agda files.
>>
>> * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files.
>
> [...]
>
>> + (arguments
>> + `(#:modules ((guix build haskell-build-system)
>> + (guix build utils)
>> + (srfi srfi-26))
>> + #:phases
>> + (modify-phases %standard-phases
>> + (add-after 'compile 'agda-compile
>> + (lambda* (#:key outputs #:allow-other-keys)
>> + (let* ((out (assoc-ref outputs "out"))
>> + (agda-compiler (string-append out "/bin/agda"))
>> + (agda-files-path (string-append
>> + out
>> + "/share/x86_64-linux-ghc-8.0.2/Agda-"
>
> This is unfortunate, since it hard-codes both architecture and GHC
> version. Can you think of another method to find these files?
>
> Are there ".agda" files elsewhere under "/share"? Could the find-files
> invokation below simply search "out/share", for example?
>
That works!
>> + ,version
>> + "/lib/prim/Agda/"))
>> + (agda-files (append
>> + (find-files agda-files-path "\\.agda$")
>> + (find-files (string-append
>> + agda-files-path
>> + "Builtin")
>> + "\\.agda$"))))
>
> (find-files ...) recurses through subdirectories, are you sure adding an
> extra pass for "Builtin/*.agda" makes a difference here?
>
Removed.
>> + (for-each (cut invoke agda-compiler <>) agda-files)
>> + #t))))))
>> (home-page "http://wiki.portal.chalmers.se/agda/")
>
> Otherwise LGTM.
>
> [...]
>
>> From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001
>> From: Alex ter Weele <alex.ter.weele@gmail.com>
>> Date: Sat, 21 Jul 2018 10:57:35 -0500
>> Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode
>>
>> * gnu/packages/agda.scm (emacs-agda2-mode): New variable.
>
> LGTM!
I found a few potential issues with it. The variable and package names
were mismatched, the inputs were inherited, and the home page was
misspelled. Corrected in the following patch series.
Thanks for the review!
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0001-gnu-agda-Compile-.agda-files.patch --]
[-- Type: text/x-patch, Size: 1397 bytes --]
From 51ad1e736760fb083fd04d933f9aaf6658b4b7fe Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele@gmail.com>
Date: Fri, 20 Jul 2018 21:35:14 -0500
Subject: [PATCH 1/2] gnu: agda: Compile .agda files.
* gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files.
---
gnu/packages/agda.scm | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 6aa230116..d677bb7e5 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -67,6 +67,19 @@
("ghc-text" ,ghc-text)
("ghc-unordered-containers" ,ghc-unordered-containers)
("ghc-zlib" ,ghc-zlib)))
+ (arguments
+ `(#:modules ((guix build haskell-build-system)
+ (guix build utils)
+ (srfi srfi-26))
+ #:phases
+ (modify-phases %standard-phases
+ (add-after 'compile 'agda-compile
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (agda-compiler (string-append out "/bin/agda")))
+ (for-each (cut invoke agda-compiler <>)
+ (find-files (string-append out "/share") "\\.agda$"))
+ #t))))))
(home-page "http://wiki.portal.chalmers.se/agda/")
(synopsis
"Dependently typed functional programming language and proof assistant")
--
2.18.0
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #3: 0002-gnu-Add-emacs-agda2-mode.patch --]
[-- Type: text/x-patch, Size: 1624 bytes --]
From b57cfb8766e85a4c2c8491415f2bf0d9357bcca2 Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele@gmail.com>
Date: Sat, 21 Jul 2018 10:57:35 -0500
Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode
* gnu/packages/agda.scm (emacs-agda2-mode): New variable.
---
gnu/packages/agda.scm | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index d677bb7e5..7bdf10e61 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -20,6 +20,7 @@
#:use-module (gnu packages haskell)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
+ #:use-module (guix build-system emacs)
#:use-module (guix build-system haskell)
#:use-module (guix build-system trivial)
#:use-module (guix download)
@@ -97,3 +98,19 @@ such as Coq, Epigram and NuPRL.")
;; Agda is distributed under the MIT license, and a couple of
;; source files are BSD-3. See LICENSE for details.
(license (list license:expat license:bsd-3))))
+
+(define-public emacs-agda2-mode
+ (package
+ (inherit agda)
+ (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"))))))
+ (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.")))
--
2.18.0
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode.
2018-07-28 2:39 ` Alex ter Weele
@ 2018-07-28 15:42 ` Marius Bakke
2018-07-29 21:39 ` bug#32235: " Marius Bakke
0 siblings, 1 reply; 6+ messages in thread
From: Marius Bakke @ 2018-07-28 15:42 UTC (permalink / raw)
To: Alex ter Weele; +Cc: 32235
[-- Attachment #1: Type: text/plain, Size: 2838 bytes --]
Alex ter Weele <alex.ter.weele@gmail.com> writes:
> Marius Bakke <mbakke@fastmail.com> writes:
>
>> Alex ter Weele <alex.ter.weele@gmail.com> writes:
>>
>>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
>>> From: Alex ter Weele <alex.ter.weele@gmail.com>
>>> Date: Fri, 20 Jul 2018 21:35:14 -0500
>>> Subject: [PATCH 1/2] gnu: agda: Compile .agda files.
>>>
>>> * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files.
>>
>> [...]
>>
>>> + (arguments
>>> + `(#:modules ((guix build haskell-build-system)
>>> + (guix build utils)
>>> + (srfi srfi-26))
>>> + #:phases
>>> + (modify-phases %standard-phases
>>> + (add-after 'compile 'agda-compile
>>> + (lambda* (#:key outputs #:allow-other-keys)
>>> + (let* ((out (assoc-ref outputs "out"))
>>> + (agda-compiler (string-append out "/bin/agda"))
>>> + (agda-files-path (string-append
>>> + out
>>> + "/share/x86_64-linux-ghc-8.0.2/Agda-"
>>
>> This is unfortunate, since it hard-codes both architecture and GHC
>> version. Can you think of another method to find these files?
>>
>> Are there ".agda" files elsewhere under "/share"? Could the find-files
>> invokation below simply search "out/share", for example?
>>
>
> That works!
>
>>> + ,version
>>> + "/lib/prim/Agda/"))
>>> + (agda-files (append
>>> + (find-files agda-files-path "\\.agda$")
>>> + (find-files (string-append
>>> + agda-files-path
>>> + "Builtin")
>>> + "\\.agda$"))))
>>
>> (find-files ...) recurses through subdirectories, are you sure adding an
>> extra pass for "Builtin/*.agda" makes a difference here?
>>
>
> Removed.
>
>>> + (for-each (cut invoke agda-compiler <>) agda-files)
>>> + #t))))))
>>> (home-page "http://wiki.portal.chalmers.se/agda/")
>>
>> Otherwise LGTM.
>>
>> [...]
>>
>>> From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001
>>> From: Alex ter Weele <alex.ter.weele@gmail.com>
>>> Date: Sat, 21 Jul 2018 10:57:35 -0500
>>> Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode
>>>
>>> * gnu/packages/agda.scm (emacs-agda2-mode): New variable.
>>
>> LGTM!
>
> I found a few potential issues with it. The variable and package names
> were mismatched, the inputs were inherited, and the home page was
> misspelled. Corrected in the following patch series.
>
> Thanks for the review!
Thanks for catching my review mistake! All LGTM.
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 487 bytes --]
^ permalink raw reply [flat|nested] 6+ messages in thread
* bug#32235: [PATCH] Fix Agda compilation, add Agda's emacs mode.
2018-07-28 15:42 ` Marius Bakke
@ 2018-07-29 21:39 ` Marius Bakke
0 siblings, 0 replies; 6+ messages in thread
From: Marius Bakke @ 2018-07-29 21:39 UTC (permalink / raw)
To: Alex ter Weele; +Cc: 32235-done
[-- Attachment #1: Type: text/plain, Size: 3185 bytes --]
Marius Bakke <mbakke@fastmail.com> writes:
> Alex ter Weele <alex.ter.weele@gmail.com> writes:
>
>> Marius Bakke <mbakke@fastmail.com> writes:
>>
>>> Alex ter Weele <alex.ter.weele@gmail.com> writes:
>>>
>>>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
>>>> From: Alex ter Weele <alex.ter.weele@gmail.com>
>>>> Date: Fri, 20 Jul 2018 21:35:14 -0500
>>>> Subject: [PATCH 1/2] gnu: agda: Compile .agda files.
>>>>
>>>> * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files.
>>>
>>> [...]
>>>
>>>> + (arguments
>>>> + `(#:modules ((guix build haskell-build-system)
>>>> + (guix build utils)
>>>> + (srfi srfi-26))
>>>> + #:phases
>>>> + (modify-phases %standard-phases
>>>> + (add-after 'compile 'agda-compile
>>>> + (lambda* (#:key outputs #:allow-other-keys)
>>>> + (let* ((out (assoc-ref outputs "out"))
>>>> + (agda-compiler (string-append out "/bin/agda"))
>>>> + (agda-files-path (string-append
>>>> + out
>>>> + "/share/x86_64-linux-ghc-8.0.2/Agda-"
>>>
>>> This is unfortunate, since it hard-codes both architecture and GHC
>>> version. Can you think of another method to find these files?
>>>
>>> Are there ".agda" files elsewhere under "/share"? Could the find-files
>>> invokation below simply search "out/share", for example?
>>>
>>
>> That works!
>>
>>>> + ,version
>>>> + "/lib/prim/Agda/"))
>>>> + (agda-files (append
>>>> + (find-files agda-files-path "\\.agda$")
>>>> + (find-files (string-append
>>>> + agda-files-path
>>>> + "Builtin")
>>>> + "\\.agda$"))))
>>>
>>> (find-files ...) recurses through subdirectories, are you sure adding an
>>> extra pass for "Builtin/*.agda" makes a difference here?
>>>
>>
>> Removed.
>>
>>>> + (for-each (cut invoke agda-compiler <>) agda-files)
>>>> + #t))))))
>>>> (home-page "http://wiki.portal.chalmers.se/agda/")
>>>
>>> Otherwise LGTM.
>>>
>>> [...]
>>>
>>>> From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001
>>>> From: Alex ter Weele <alex.ter.weele@gmail.com>
>>>> Date: Sat, 21 Jul 2018 10:57:35 -0500
>>>> Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode
>>>>
>>>> * gnu/packages/agda.scm (emacs-agda2-mode): New variable.
>>>
>>> LGTM!
>>
>> I found a few potential issues with it. The variable and package names
>> were mismatched, the inputs were inherited, and the home page was
>> misspelled. Corrected in the following patch series.
>>
>> Thanks for the review!
>
> Thanks for catching my review mistake! All LGTM.
Whoops, Ludovic helpfully reminded me on IRC that you don't yet have
commit access. I've pushed these patches.
(note that I added a #t after the chdir for emacs-agda2-mode, since the
return value of chdir is unspecified)
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 487 bytes --]
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2018-07-29 21:40 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2018-07-21 15:59 [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode Alex ter Weele
[not found] ` <handler.32235.B.15321888082039.ack@debbugs.gnu.org>
2018-07-21 16:13 ` Alex ter Weele
2018-07-22 14:40 ` Marius Bakke
2018-07-28 2:39 ` Alex ter Weele
2018-07-28 15:42 ` Marius Bakke
2018-07-29 21:39 ` bug#32235: " Marius Bakke
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).