GNU bug report logs -
#32235
[PATCH] Fix Agda compilation, add Agda's emacs mode.
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 32235 in the body.
You can then email your comments to 32235 AT debbugs.gnu.org in the normal way.
Toggle the display of automated, internal messages from the tracker.
Report forwarded
to
guix-patches <at> gnu.org:
bug#32235; Package
guix-patches.
(Sat, 21 Jul 2018 16:01:02 GMT)
Full text and
rfc822 format available.
Acknowledgement sent
to
Alex ter Weele <alex.ter.weele <at> gmail.com>:
New bug report received and forwarded. Copy sent to
guix-patches <at> gnu.org.
(Sat, 21 Jul 2018 16:01:02 GMT)
Full text and
rfc822 format available.
Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
Information forwarded
to
guix-patches <at> gnu.org:
bug#32235; Package
guix-patches.
(Sat, 21 Jul 2018 16:15:01 GMT)
Full text and
rfc822 format available.
Message #8 received at 32235 <at> debbugs.gnu.org (full text, mbox):
[0001-gnu-agda-Compile-.agda-files.patch (text/x-patch, attachment)]
[0002-gnu-Add-emacs-agda2-mode.patch (text/x-patch, attachment)]
Information forwarded
to
guix-patches <at> gnu.org:
bug#32235; Package
guix-patches.
(Sun, 22 Jul 2018 14:41:02 GMT)
Full text and
rfc822 format available.
Message #11 received at 32235 <at> debbugs.gnu.org (full text, mbox):
[Message part 1 (text/plain, inline)]
Alex ter Weele <alex.ter.weele <at> gmail.com> writes:
> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
> From: Alex ter Weele <alex.ter.weele <at> 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 <at> 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!
[signature.asc (application/pgp-signature, inline)]
Information forwarded
to
guix-patches <at> gnu.org:
bug#32235; Package
guix-patches.
(Sat, 28 Jul 2018 02:40:02 GMT)
Full text and
rfc822 format available.
Message #14 received at 32235 <at> debbugs.gnu.org (full text, mbox):
[Message part 1 (text/plain, inline)]
Marius Bakke <mbakke <at> fastmail.com> writes:
> Alex ter Weele <alex.ter.weele <at> gmail.com> writes:
>
>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
>> From: Alex ter Weele <alex.ter.weele <at> 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 <at> 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!
[0001-gnu-agda-Compile-.agda-files.patch (text/x-patch, inline)]
From 51ad1e736760fb083fd04d933f9aaf6658b4b7fe Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele <at> 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
[0002-gnu-Add-emacs-agda2-mode.patch (text/x-patch, inline)]
From b57cfb8766e85a4c2c8491415f2bf0d9357bcca2 Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele <at> 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
Information forwarded
to
guix-patches <at> gnu.org:
bug#32235; Package
guix-patches.
(Sat, 28 Jul 2018 15:44:02 GMT)
Full text and
rfc822 format available.
Message #17 received at 32235 <at> debbugs.gnu.org (full text, mbox):
[Message part 1 (text/plain, inline)]
Alex ter Weele <alex.ter.weele <at> gmail.com> writes:
> Marius Bakke <mbakke <at> fastmail.com> writes:
>
>> Alex ter Weele <alex.ter.weele <at> gmail.com> writes:
>>
>>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
>>> From: Alex ter Weele <alex.ter.weele <at> 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 <at> 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.
[signature.asc (application/pgp-signature, inline)]
Reply sent
to
Marius Bakke <mbakke <at> fastmail.com>:
You have taken responsibility.
(Sun, 29 Jul 2018 21:40:01 GMT)
Full text and
rfc822 format available.
Notification sent
to
Alex ter Weele <alex.ter.weele <at> gmail.com>:
bug acknowledged by developer.
(Sun, 29 Jul 2018 21:40:02 GMT)
Full text and
rfc822 format available.
Message #22 received at 32235-done <at> debbugs.gnu.org (full text, mbox):
[Message part 1 (text/plain, inline)]
Marius Bakke <mbakke <at> fastmail.com> writes:
> Alex ter Weele <alex.ter.weele <at> gmail.com> writes:
>
>> Marius Bakke <mbakke <at> fastmail.com> writes:
>>
>>> Alex ter Weele <alex.ter.weele <at> gmail.com> writes:
>>>
>>>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
>>>> From: Alex ter Weele <alex.ter.weele <at> 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 <at> 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)
[signature.asc (application/pgp-signature, inline)]
bug archived.
Request was from
Debbugs Internal Request <help-debbugs <at> gnu.org>
to
internal_control <at> debbugs.gnu.org.
(Mon, 27 Aug 2018 11:24:05 GMT)
Full text and
rfc822 format available.
This bug report was last modified 7 years and 11 days ago.
Previous Next
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.