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

Previous Next

Full log

View this message in rfc822 format

From: Nicolas Graves <ngraves <at> ngraves.fr>
To: emma <bigbookofbug <at> proton.me>, 78289 <at> debbugs.gnu.org
Subject: [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

Previous Next

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