GNU bug report logs - #51755
[PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)

Previous Next

Package: guix-patches;

Reported by: zimoun <zimon.toutoune <at> gmail.com>

Date: Wed, 10 Nov 2021 19:35:02 UTC

Severity: normal

Tags: patch

Done: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>

Bug is archived. No further changes may be made.

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 51755 in the body.
You can then email your comments to 51755 AT debbugs.gnu.org in the normal way.

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

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to guix-patches <at> gnu.org:
bug#51755; Package guix-patches. (Wed, 10 Nov 2021 19:35:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to zimoun <zimon.toutoune <at> gmail.com>:
New bug report received and forwarded. Copy sent to guix-patches <at> gnu.org. (Wed, 10 Nov 2021 19:35:02 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: guix-patches <at> gnu.org
Cc: zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)
Date: Wed, 10 Nov 2021 20:26:22 +0100
Hi,

This is a follow-up of bug#46016 [1] and I think close it.

Now, it is possible to use ProofGeneral as any other Emacs packages.  For
instance,

   guix shell emacs proof-general coq
   emacs foo.v

For now, the dependency of 'coq' is removed as with many Emacs packages.
Other said, the user has to provide such dependency.  IMHO, it is the spirit
of such package where the 'prover' is let to the user (several are more or
less supported, see doc [2]).

Cheers,
simon



1: <http://issues.guix.gnu.org/issue/46016>
2: <https://proofgeneral.github.io/doc/master/userman/Introducing-Proof-General/#Supported-proof-assistants>


zimoun (1):
  gnu: proof-general: Adjust autoloads for Emacs.

 gnu/packages/coq.scm | 85 +++++++++++++++++++++++---------------------
 1 file changed, 45 insertions(+), 40 deletions(-)


base-commit: 140b486437670ce95cb24a935b58cba52a9dac31
-- 
2.33.1





Information forwarded to guix-patches <at> gnu.org:
bug#51755; Package guix-patches. (Wed, 10 Nov 2021 19:38:01 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: 51755 <at> debbugs.gnu.org
Cc: zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs.
Date: Wed, 10 Nov 2021 20:37:48 +0100
Fixes <https://bugs.gnu.org/46016>.

* gnu/packages/coq.scm (proof-general)[native-inputs]: Remove 'which'.
[inputs]: Remove 'coq' and 'emacs'.
[arguments]<#:make-flags>: Adjust to find 'emacs'.
Set 'ELISP' and 'DEST_LISP'.
<#:modules, #:imported-modules>: Remove.
<#:phases>: Remove call to 'which' in Makefile.
Add copy file allowing Emacs autoloads.
Clean unnecessary code.
---
 gnu/packages/coq.scm | 85 +++++++++++++++++++++++---------------------
 1 file changed, 45 insertions(+), 40 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index dccb9bea4c..2cf9d1a602 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -135,50 +135,55 @@ (define-public proof-general
                   "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
       (build-system gnu-build-system)
       (native-inputs
-       `(("which" ,which)
-         ("emacs" ,emacs-minimal)
+       `(("emacs" ,emacs-minimal)
          ("texinfo" ,texinfo)))
       (inputs
-       `(("host-emacs" ,emacs)
-         ("perl" ,perl)
-         ("coq" ,coq)))
+       `(("perl" ,perl)))
       (arguments
-       `(#:tests? #f                   ; no check target
-         #:make-flags (list (string-append "PREFIX=" %output)
-                            (string-append "DEST_PREFIX=" %output)
-                            (string-append "ELISP_START=" %output
-                                           "/share/emacs/site-lisp/ProofGeneral"))
-         #:modules ((guix build gnu-build-system)
-                    (guix build utils)
-                    (guix build emacs-utils))
-         #:imported-modules (,@%gnu-build-system-modules
-                             (guix build emacs-utils))
-         #:phases
-         (modify-phases %standard-phases
-           (delete 'configure)
-           (add-after 'unpack 'disable-byte-compile-error-on-warn
-             (lambda _
-               (substitute* "Makefile"
-                 (("\\(setq byte-compile-error-on-warn t\\)")
-                  "(setq byte-compile-error-on-warn nil)"))))
-           (add-after 'unpack 'patch-hardcoded-paths
-             (lambda* (#:key inputs outputs #:allow-other-keys)
-               (let ((out   (assoc-ref outputs "out"))
-                     (coq   (assoc-ref inputs "coq"))
-                     (emacs (assoc-ref inputs "host-emacs")))
+       (let ((base-directory "/share/emacs/site-lisp/ProofGeneral"))
+         `(#:tests? #f                   ; no check target
+           #:make-flags (list (string-append "PREFIX=" %output)
+                              (string-append "EMACS=" (assoc-ref %build-inputs "emacs")
+                                             "/bin/emacs")
+                              (string-append "DEST_PREFIX=" %output)
+                              (string-append "ELISP=" %output ,base-directory)
+                              (string-append "DEST_ELISP=" %output ,base-directory)
+                              (string-append "ELISP_START=" %output ,base-directory))
+           #:phases
+           (modify-phases %standard-phases
+             (delete 'configure)
+             (add-after 'unpack 'disable-byte-compile-error-on-warn
+               (lambda _
+                 (substitute* "Makefile"
+                   (("\\(setq byte-compile-error-on-warn t\\)")
+                    "(setq byte-compile-error-on-warn nil)"))))
+             (add-after 'unpack 'patch-hardcoded-paths
+               (lambda _
+                 (substitute* "Makefile"
+                   (("/sbin/install-info") "install-info"))))
+             (add-after 'unpack 'remove-which
+               (lambda _
+                 (substitute* "Makefile"
+                   (("`which perl`") "perl")
+                   (("`which bash`") "bash"))))
+             (add-after 'unpack 'clean
+               (lambda _
+                 ;; Delete the pre-compiled elc files for Emacs 23.
+                 (invoke "make" "clean")))
+             (add-after 'install 'install-doc
+               (lambda* (#:key make-flags #:allow-other-keys)
+                 ;; XXX FIXME avoid building/installing pdf files,
+                 ;; due to unresolved errors building them.
                  (substitute* "Makefile"
-                   (("/sbin/install-info") "install-info")))))
-           (add-after 'unpack 'clean
-             (lambda _
-               ;; Delete the pre-compiled elc files for Emacs 23.
-               (invoke "make" "clean")))
-           (add-after 'install 'install-doc
-             (lambda* (#:key make-flags #:allow-other-keys)
-               ;; XXX FIXME avoid building/installing pdf files,
-               ;; due to unresolved errors building them.
-               (substitute* "Makefile"
-                 ((" [^ ]*\\.pdf") ""))
-               (apply invoke "make" "install-doc" make-flags))))))
+                   ((" [^ ]*\\.pdf") ""))
+                 (apply invoke "make" "install-doc" make-flags)))
+             (add-after 'install 'allow-subfolders-autoloads
+               (lambda* (#:key outputs #:allow-other-keys)
+                 (let ((out (assoc-ref outputs "out")))
+                   ;; Make it visible by Emacs
+                   (copy-file "proof-general.el"
+                              (string-append out ,base-directory
+                                             "/proof-general-autoloads.el")))))))))
       (home-page "https://proofgeneral.github.io/")
       (synopsis "Generic front-end for proof assistants based on Emacs")
       (description
-- 
2.33.1





Information forwarded to guix-patches <at> gnu.org:
bug#51755; Package guix-patches. (Fri, 19 Nov 2021 12:28:01 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: 51755 <at> debbugs.gnu.org
Cc: Julien Lepiller <julien <at> lepiller.eu>,
 Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
Subject: Re: [bug#51755] [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)
Date: Fri, 19 Nov 2021 13:27:13 +0100
Hi Coq or Emacs reviewers,

On Wed, 10 Nov 2021 at 20:26, zimoun <zimon.toutoune <at> gmail.com> wrote:

> This is a follow-up of bug#46016 [1] and I think close it.
>
> Now, it is possible to use ProofGeneral as any other Emacs packages.  For
> instance,
>
>    guix shell emacs proof-general coq
>    emacs foo.v
>
> For now, the dependency of 'coq' is removed as with many Emacs packages.
> Other said, the user has to provide such dependency.  IMHO, it is the spirit
> of such package where the 'prover' is let to the user (several are more or
> less supported, see doc [2]).
>
> 1: <http://issues.guix.gnu.org/issue/46016>
> 2: <https://proofgeneral.github.io/doc/master/userman/Introducing-Proof-General/#Supported-proof-assistants>

Friendly ping. :-)


Cheers,
simon




Information forwarded to guix-patches <at> gnu.org:
bug#51755; Package guix-patches. (Sun, 21 Nov 2021 18:42:02 GMT) Full text and rfc822 format available.

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

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 51755 <at> debbugs.gnu.org
Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads
 for Emacs.
Date: Sun, 21 Nov 2021 19:40:56 +0100
Hello,

zimoun <zimon.toutoune <at> gmail.com> writes:

> * gnu/packages/coq.scm (proof-general)[native-inputs]: Remove 'which'.
> [inputs]: Remove 'coq' and 'emacs'.
> [arguments]<#:make-flags>: Adjust to find 'emacs'.
> Set 'ELISP' and 'DEST_LISP'.
> <#:modules, #:imported-modules>: Remove.
> <#:phases>: Remove call to 'which' in Makefile.
> Add copy file allowing Emacs autoloads.
> Clean unnecessary code.

Thanks.

> +             (add-after 'install 'allow-subfolders-autoloads
> +               (lambda* (#:key outputs #:allow-other-keys)
> +                 (let ((out (assoc-ref outputs "out")))
> +                   ;; Make it visible by Emacs
> +                   (copy-file "proof-general.el"
> +                              (string-append out ,base-directory
> +                                             "/proof-general-autoloads.el")))))))))

So, IIUC, the above is basically a hack: you disguise the main file into
an autoloads file because no autoloads file is generated from the code
base? If so, this might deserve a longer comment, IMO.

Otherwise, LGTM.

Regards,
-- 
Nicolas Goaziou




Information forwarded to guix-patches <at> gnu.org:
bug#51755; Package guix-patches. (Sun, 21 Nov 2021 19:08:01 GMT) Full text and rfc822 format available.

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

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>, zimoun <zimon.toutoune <at> gmail.com>
Cc: 51755 <at> debbugs.gnu.org
Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads
 for Emacs.
Date: Sun, 21 Nov 2021 20:07:48 +0100
Hi,

Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou:
> > +             (add-after 'install 'allow-subfolders-autoloads
> > +               (lambda* (#:key outputs #:allow-other-keys)
> > +                 (let ((out (assoc-ref outputs "out")))
> > +                   ;; Make it visible by Emacs
> > +                   (copy-file "proof-general.el"
> > +                              (string-append out ,base-directory
> > +                                             "/proof-general-
> > autoloads.el")))))))))
> 
> So, IIUC, the above is basically a hack: you disguise the main file
> into an autoloads file because no autoloads file is generated from
> the code base? If so, this might deserve a longer comment, IMO.
On a related note, what would be so bad about having to (require
'proof-general) interactively?  Alternatively, we could in an after-
unpack phase add autoload cookies to the source file or write our own
autoloads altogether.  WDYT?





Information forwarded to guix-patches <at> gnu.org:
bug#51755; Package guix-patches. (Sun, 21 Nov 2021 20:16:01 GMT) Full text and rfc822 format available.

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

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Cc: 51755 <at> debbugs.gnu.org, zimoun <zimon.toutoune <at> gmail.com>
Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads
 for Emacs.
Date: Sun, 21 Nov 2021 21:15:30 +0100
Hello,

Liliana Marie Prikler <liliana.prikler <at> gmail.com> writes:

> Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou:

>> So, IIUC, the above is basically a hack: you disguise the main file
>> into an autoloads file because no autoloads file is generated from
>> the code base? If so, this might deserve a longer comment, IMO.

Actually, my assumption was wrong. "proof-general.el" is
a meta-autoloads file:

    ;; This file is a thin, package.el-friendly wrapper around generic/proof-site,
    ;; suitable for execution on Emacs start-up.  It serves two purposes:
    ;;
    ;; * Setting up the load path when byte-compiling PG.
    ;; * Loading a minimal PG setup on startup (not all of Proof General, of course;
    ;;   mostly mode hooks and autoloads).

> On a related note, what would be so bad about having to (require
> 'proof-general) interactively?

When not byte compiled, the file only does

  (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root)))

I guess we could also provide a single autoloads file doing just that
or, according to the manual,

  (load "PROOF-GENERAL-HOME/generic/proof-site.el")

> Alternatively, we could in an after-
> unpack phase add autoload cookies to the source file or write our own
> autoloads altogether.  WDYT?

Autoload cookies are already present in the code base, but in
sub-directories.

OTOH, I assume the solution proposed by Zimoun, as hackish as it is,
works well enough. And it requires less work. IMO, it is acceptable with
a good comment.

Regards,
-- 
Nicolas Goaziou




Information forwarded to guix-patches <at> gnu.org:
bug#51755; Package guix-patches. (Sun, 21 Nov 2021 21:22:02 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>, Liliana Marie Prikler
 <liliana.prikler <at> gmail.com>
Cc: 51755 <at> debbugs.gnu.org
Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads
 for Emacs.
Date: Sun, 21 Nov 2021 22:11:58 +0100
Hi,

Thanks for the review.


On Sun, 21 Nov 2021 at 21:15, Nicolas Goaziou <mail <at> nicolasgoaziou.fr> wrote:
> Liliana Marie Prikler <liliana.prikler <at> gmail.com> writes:
>> Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou:

>>> So, IIUC, the above is basically a hack: you disguise the main file
>>> into an autoloads file because no autoloads file is generated from
>>> the code base? If so, this might deserve a longer comment, IMO.
>
> Actually, my assumption was wrong. "proof-general.el" is
> a meta-autoloads file:
>
>     ;; This file is a thin, package.el-friendly wrapper around generic/proof-site,
>     ;; suitable for execution on Emacs start-up.  It serves two purposes:
>     ;;
>     ;; * Setting up the load path when byte-compiling PG.
>     ;; * Loading a minimal PG setup on startup (not all of Proof General, of course;
>     ;;   mostly mode hooks and autoloads).

Yes.  Note that ’proof-general’ was at one moment in its long history a
standalone package, i.e., running ’bin/proofgeneneral’ started Emacs and
launched everything.  This had been removed long time ago [1] but the
current code inherits this long history.

1: <https://github.com/ProofGeneral/PG/commit/1a18e33658645a81225c56b5d4f4a4b89434d301>


>> Alternatively, we could in an after-
>> unpack phase add autoload cookies to the source file or write our own
>> autoloads altogether.  WDYT?
>
> Autoload cookies are already present in the code base, but in
> sub-directories.

Yes.  The limitation comes from this subdirectory structure.  This
breaks the usual way of packaging Emacs tools for Guix, IIUC.


> OTOH, I assume the solution proposed by Zimoun, as hackish as it is,
> works well enough. And it requires less work. IMO, it is acceptable with
> a good comment.

From my point of view, my proposed patch appears to me the easiest fix.
If something is better, please let me know. :-)


About the comment, I thought « allow-subfolders-autoloads » and « Make
it visible by Emacs » would have been enough. ;-)

--8<---------------cut here---------------start------------->8---
             (add-after 'install 'allow-subfolders-autoloads
               (lambda* (#:key outputs #:allow-other-keys)
                 (let ((out (assoc-ref outputs "out")))
                   ;; Make it visible by Emacs
--8<---------------cut here---------------end--------------->8---


Instead, I propose to extend to:

--8<---------------cut here---------------start------------->8---
             (add-after 'install 'allow-subfolders-autoloads
               ;; Autoload cookies are present in sub-directories. A friendly
               ;; wrapper proof-general.el around generic/proof-site.el is
               ;; provided for execution on Emacs start-up.  It serves two
               ;; purposes:
               ;; * Setting up the load path when byte-compiling pg.
               ;; * Loading a minimal PG setup on startup (not all of Proof
               ;; General, of course;mostly mode hooks and autoloads).
               ;; The rename to proof-general-autoloads.el is Guix specific.
               (lambda* (#:key outputs #:allow-other-keys)
                 (let ((out (assoc-ref outputs "out")))
                   (copy-file "proof-general.el"
                              (string-append out ,base-directory
                                             "/proof-general-autoloads.el")))))))))
--8<---------------cut here---------------end--------------->8---


Is it fine?  If yes, I can send* a v2.  Or please push directly. :-)



Cheers,
simon

*send v2: for the record, I do not have commit right. ;-)




Reply sent to Nicolas Goaziou <mail <at> nicolasgoaziou.fr>:
You have taken responsibility. (Mon, 22 Nov 2021 18:23:02 GMT) Full text and rfc822 format available.

Notification sent to zimoun <zimon.toutoune <at> gmail.com>:
bug acknowledged by developer. (Mon, 22 Nov 2021 18:23:02 GMT) Full text and rfc822 format available.

Message #28 received at 51755-done <at> debbugs.gnu.org (full text, mbox):

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 51755-done <at> debbugs.gnu.org,
 Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads
 for Emacs.
Date: Mon, 22 Nov 2021 19:22:39 +0100
Hello,

zimoun <zimon.toutoune <at> gmail.com> writes:

> Instead, I propose to extend to:
>
> --8<---------------cut here---------------start------------->8---
>              (add-after 'install 'allow-subfolders-autoloads
>                ;; Autoload cookies are present in sub-directories. A friendly
>                ;; wrapper proof-general.el around generic/proof-site.el is
>                ;; provided for execution on Emacs start-up.  It serves two
>                ;; purposes:
>                ;; * Setting up the load path when byte-compiling pg.
>                ;; * Loading a minimal PG setup on startup (not all of Proof
>                ;; General, of course;mostly mode hooks and autoloads).
>                ;; The rename to proof-general-autoloads.el is Guix specific.
>                (lambda* (#:key outputs #:allow-other-keys)
>                  (let ((out (assoc-ref outputs "out")))
>                    (copy-file "proof-general.el"
>                               (string-append out ,base-directory
>                                              "/proof-general-autoloads.el")))))))))
> --8<---------------cut here---------------end--------------->8---
>
>
> Is it fine?  If yes, I can send* a v2.  Or please push directly. :-)

I pushed it directly. Thank you!

Regards,
-- 
Nicolas Goaziou




Information forwarded to guix-patches <at> gnu.org:
bug#51755; Package guix-patches. (Mon, 22 Nov 2021 21:53:01 GMT) Full text and rfc822 format available.

Message #31 received at 51755-done <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
Cc: 51755-done <at> debbugs.gnu.org,
 Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads
 for Emacs.
Date: Sun, 21 Nov 2021 23:17:45 +0100
Hi Nicolas,

On Mon, 22 Nov 2021 at 19:22, Nicolas Goaziou <mail <at> nicolasgoaziou.fr> wrote:

> I pushed it directly. Thank you!

Thank you.

Cheers,
simon




bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Tue, 21 Dec 2021 12:24:09 GMT) Full text and rfc822 format available.

This bug report was last modified 2 years and 88 days ago.

Previous Next


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