GNU bug report logs - #78289
[PATCH] gnu: emacs-lean4-mode: add data dir to output

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 78289 in the body.
You can then email your comments to 78289 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: emma <bigbookofbug <at> proton.me>
To: "guix-patches <at> gnu.org" <guix-patches <at> gnu.org>
Subject: [PATCH] gnu: emacs-lean4-mode: add data dir to output
Date: Wed, 07 May 2025 02:25:07 +0000

[Message part 1 (text/plain, inline)]

---

gnu/packages/emacs-xyz.scm | 11 +++++++++++
1 file changed, 11 insertions(+)

diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scm
index 50a6f4c386..fd919aa210 100644
--- a/gnu/packages/emacs-xyz.scm
+++ b/gnu/packages/emacs-xyz.scm
@@ -3081,6 +3081,17 @@ (define-public emacs-lean4-mode
;; TODO: Just emacs-magit-section instead of emacs-magit would be enough.
(propagated-inputs
(list emacs-compat emacs-lsp-mode emacs-dash emacs-magit))
+ (arguments
+ (list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'install 'install-data
+ (lambda _
+ (let ((data (string-append #$output
+ "/share/emacs/site-lisp/"
+ "lean4-mode-1.1.2/data")))
+ (mkdir-p data)
+ (copy-recursively "data" data)))))))
(synopsis "Lean 4 major mode for Emacs")
(description "This package provides a major mode for the Lean theorem
prover, version 4.")

base-commit: d110f7dd006f4e47aa56de3cdaf5bb4b82eb5ca2
--
2.49.0

emma (bigbookofbug)
EF515F7D600717781DF9AB2E0FB1CF2867A117F5

Sent with [Proton Mail](https://proton.me/mail/home) secure email.

[Message part 2 (text/html, inline)]

Message #8 received at 78289 <at> debbugs.gnu.org (full text, mbox):

From: Nicolas Graves <ngraves <at> ngraves.fr>
To: emma <bigbookofbug <at> proton.me>, 78289 <at> debbugs.gnu.org
Subject: Re: [bug#78289] [PATCH] gnu: emacs-lean4-mode: add data dir to output
Date: Thu, 08 May 2025 16:13:40 +0200

Hi Emma,
TY for your contribution!

You can use elpa-directory to make this code easier to read, see for
instance :
https://issues.guix.gnu.org/issue/78315/attachment/51/

Also :
  - arguments field usually comes after build-system
  - the code is not formatted properly.  If you don't use a fancy editor
  with support for guile, you can always run
  ./pre-inst-env guix style emacs-lean4-mode to do it for you.

Can you submit a new version with that taken into account?  Thanks!

On 2025-05-07 02:25, emma via Guix-patches via wrote:

> ---
>
> gnu/packages/emacs-xyz.scm | 11 +++++++++++
> 1 file changed, 11 insertions(+)
>
> diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scm
> index 50a6f4c386..fd919aa210 100644
> --- a/gnu/packages/emacs-xyz.scm
> +++ b/gnu/packages/emacs-xyz.scm
> @@ -3081,6 +3081,17 @@ (define-public emacs-lean4-mode
> ;; TODO: Just emacs-magit-section instead of emacs-magit would be enough.
> (propagated-inputs
> (list emacs-compat emacs-lsp-mode emacs-dash emacs-magit))
> + (arguments
> + (list
> + #:phases
> + #~(modify-phases %standard-phases
> + (add-after 'install 'install-data
> + (lambda _
> + (let ((data (string-append #$output
> + "/share/emacs/site-lisp/"
> + "lean4-mode-1.1.2/data")))
> + (mkdir-p data)
> + (copy-recursively "data" data)))))))
> (synopsis "Lean 4 major mode for Emacs")
> (description "This package provides a major mode for the Lean theorem
> prover, version 4.")
>
> base-commit: d110f7dd006f4e47aa56de3cdaf5bb4b82eb5ca2
> --
> 2.49.0
>
> emma (bigbookofbug)
> EF515F7D600717781DF9AB2E0FB1CF2867A117F5
>
> Sent with [Proton Mail](https://proton.me/mail/home) secure email.

-- 
Best regards,
Nicolas Graves

Message #11 received at 78289 <at> debbugs.gnu.org (full text, mbox):

From: emma <bigbookofbug <at> proton.me>
To: Nicolas Graves <ngraves <at> ngraves.fr>,
 "78289 <at> debbugs.gnu.org" <78289 <at> debbugs.gnu.org>
Subject: Re: [bug#78289] [PATCH] gnu: emacs-lean4-mode: add data dir to output
Date: Fri, 09 May 2025 14:24:02 +0000

[Message part 1 (text/plain, inline)]

hi Nicolas,

thank you for the info about guix style! attaching a diff to this reply after applying the updates. my email client has a habit of chewing up patches and send-email is currently throwing errors for me



emma (bigbookofbug)
EF515F7D600717781DF9AB2E0FB1CF2867A117F5

Sent with Proton Mail secure email.

On Thursday, May 8th, 2025 at 2:13 PM, Nicolas Graves <ngraves <at> ngraves.fr> wrote:

> Hi Emma,
> TY for your contribution!
> 
> You can use elpa-directory to make this code easier to read, see for
> instance :
> https://issues.guix.gnu.org/issue/78315/attachment/51/
> 
> Also :
> - arguments field usually comes after build-system
> - the code is not formatted properly. If you don't use a fancy editor
> with support for guile, you can always run
> ./pre-inst-env guix style emacs-lean4-mode to do it for you.
> 
> Can you submit a new version with that taken into account? Thanks!
> 
> On 2025-05-07 02:25, emma via Guix-patches via wrote:
> 
> > ---
> > 
> > gnu/packages/emacs-xyz.scm | 11 +++++++++++
> > 1 file changed, 11 insertions(+)
> > 
> > diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scm
> > index 50a6f4c386..fd919aa210 100644
> > --- a/gnu/packages/emacs-xyz.scm
> > +++ b/gnu/packages/emacs-xyz.scm
> > @@ -3081,6 +3081,17 @@ (define-public emacs-lean4-mode
> > ;; TODO: Just emacs-magit-section instead of emacs-magit would be enough.
> > (propagated-inputs
> > (list emacs-compat emacs-lsp-mode emacs-dash emacs-magit))
> > + (arguments
> > + (list
> > + #:phases
> > + #~(modify-phases %standard-phases
> > + (add-after 'install 'install-data
> > + (lambda _
> > + (let ((data (string-append #$output
> > + "/share/emacs/site-lisp/"
> > + "lean4-mode-1.1.2/data")))
> > + (mkdir-p data)
> > + (copy-recursively "data" data)))))))
> > (synopsis "Lean 4 major mode for Emacs")
> > (description "This package provides a major mode for the Lean theorem
> > prover, version 4.")
> > 
> > base-commit: d110f7dd006f4e47aa56de3cdaf5bb4b82eb5ca2
> > --
> > 2.49.0
> > 
> > emma (bigbookofbug)
> > EF515F7D600717781DF9AB2E0FB1CF2867A117F5
> > 
> > Sent with Proton Mail secure email.
> 
> 
> --
> Best regards,
> Nicolas Graves

[0001-styling-updated.patch (text/x-patch, attachment)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.