gnu: proof-general: Adjust autoloads for Emacs.

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.

Signed-off-by: Nicolas Goaziou <mail@nicolasgoaziou.fr>

gnu/packages/coq.scm

@@ -136,24 +136,20 @@ It is developed using Objective Caml and Camlp5.")
                   "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
       (build-system gnu-build-system)
       (native-inputs
-       `(("which" ,which)
+       `(("emacs" ,emacs-minimal)
-         ("emacs" ,emacs-minimal)
          ("texinfo" ,texinfo)))
       (inputs
-       `(("host-emacs" ,emacs)
+       `(("perl" ,perl)))
-         ("perl" ,perl)
-         ("coq" ,coq)))
       (arguments
+       (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_START=" %output
+                              (string-append "ELISP=" %output ,base-directory)
-                                           "/share/emacs/site-lisp/ProofGeneral"))
+                              (string-append "DEST_ELISP=" %output ,base-directory)
-         #:modules ((guix build gnu-build-system)
+                              (string-append "ELISP_START=" %output ,base-directory))
-                    (guix build utils)
-                    (guix build emacs-utils))
-         #:imported-modules (,@%gnu-build-system-modules
-                             (guix build emacs-utils))
            #:phases
            (modify-phases %standard-phases
              (delete 'configure)
@@ -163,12 +159,14 @@ It is developed using Objective Caml and Camlp5.")
                    (("\\(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)
+               (lambda _
-               (let ((out   (assoc-ref outputs "out"))
-                     (coq   (assoc-ref inputs "coq"))
-                     (emacs (assoc-ref inputs "host-emacs")))
                  (substitute* "Makefile"
-                   (("/sbin/install-info") "install-info")))))
+                   (("/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.
@@ -179,7 +177,24 @@ It is developed using Objective Caml and Camlp5.")
                  ;; due to unresolved errors building them.
                  (substitute* "Makefile"
                    ((" [^ ]*\\.pdf") ""))
-               (apply invoke "make" "install-doc" make-flags))))))
+                 (apply invoke "make" "install-doc" make-flags)))
+             (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 renaming 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")))))))))
       (home-page "https://proofgeneral.github.io/")
       (synopsis "Generic front-end for proof assistants based on Emacs")
       (description