ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
492 stars 88 forks source link

Incompatibility with `package-quickstart` #771

Open monnier opened 4 months ago

monnier commented 4 months ago

if you create a ~/.emacs.d/package-quickstart.el file with M-x package-quickstart-refresh, you may see startup error messages like:

Error during quickstart: (file-missing "Cannot open load file" "Aucun fichier ou dossier de ce type" "<...>/.emacs.d/generic/proof-site")

This is because of the use of load-file-name within an eval-and-compile inside an autoloaded chunk of code. The patch below seems to fix it (and it also takes advantage of macroexp-file-name when available).

diff --git a/proof-general.el b/proof-general.el
index c1f4c9127f..b948fe2172 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.

 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2022  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2024  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -55,19 +55,21 @@
 ;;   mostly mode hooks and autoloads).

 ;;;###autoload
-(eval-and-compile
-  (defvar pg-init--script-full-path
-    (or (bound-and-true-p byte-compile-current-file)
-        (and load-in-progress load-file-name)
+(defmacro pg-init--pg-root ()
+  `(file-name-directory
+    ,(if (fboundp 'macroexp-file-name) ;; Emacs≥28
+         `(macroexp-file-name)
+       `(or (bound-and-true-p byte-compile-current-file)
+            (and load-in-progress load-file-name)
+            buffer-file-name))))

-        (buffer-file-name)))
-  (defvar pg-init--pg-root
-    (file-name-directory pg-init--script-full-path)))

 ;;;###autoload
 (unless (bound-and-true-p byte-compile-current-file)
-  ;; This require breaks compilation, so it must only run when loading the package.
-  (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root)))
+  ;; This `require' breaks compilation, so it must run only when loading
+  ;; the package.
+  (require 'proof-site (expand-file-name "generic/proof-site"
+                                         (pg-init--pg-root))))

 (eval-when-compile
   ;; FIXME: [ This is used during installation of the ELPA package ]
@@ -81,7 +83,7 @@
            "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox" "qrhl"
            )))
     (dolist (dir byte-compile-directories)
-      (add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))
+      (add-to-list 'load-path (expand-file-name dir (pg-init--pg-root))))))

 (provide 'proof-general)
 ;;; proof-general.el ends here
monnier commented 4 months ago

Nah, scratch that, it doesn't fix it either.

monnier commented 4 months ago

OK, this one seems to fare better (and I believe my test does now test what I intended):

diff --git a/proof-general.el b/proof-general.el
index c1f4c9127f..72945239e2 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.

 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2022  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2024  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -54,20 +54,15 @@
 ;; * Loading a minimal PG setup on startup (not all of Proof General, of course;
 ;;   mostly mode hooks and autoloads).

-;;;###autoload
-(eval-and-compile
-  (defvar pg-init--script-full-path
-    (or (bound-and-true-p byte-compile-current-file)
-        (and load-in-progress load-file-name)
-
-        (buffer-file-name)))
-  (defvar pg-init--pg-root
-    (file-name-directory pg-init--script-full-path)))
-
 ;;;###autoload
 (unless (bound-and-true-p byte-compile-current-file)
-  ;; This require breaks compilation, so it must only run when loading the package.
-  (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root)))
+  ;; This require breaks compilation, so it must run only when loading
+  ;; the package.
+  (require 'proof-site
+           (expand-file-name "generic/proof-site"
+                             (file-name-directory
+                              (or (and load-in-progress load-file-name)
+                                  buffer-file-name)))))

 (eval-when-compile
   ;; FIXME: [ This is used during installation of the ELPA package ]
@@ -76,12 +71,17 @@
   ;; session, so we here add to load-path all the subdirectories so
   ;; that files in (say) coq/ can (require 'coq-foo) and the compiler will find
   ;; the corresponding file.
-  (let ((byte-compile-directories
+  (let ((pg-root
+         (file-name-directory
+          (or (bound-and-true-p byte-compile-current-file)
+              (and load-in-progress load-file-name)
+              buffer-file-name)))
+        (byte-compile-directories
          '("generic" "lib"
            "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox" "qrhl"
            )))
     (dolist (dir byte-compile-directories)
-      (add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))
+      (add-to-list 'load-path (expand-file-name dir pg-root)))))

 (provide 'proof-general)
 ;;; proof-general.el ends here
erikmd commented 4 months ago

Hi @monnier, thanks for your report and the patches!

The code you touched was initially written by @cpitclaudel so I Cc him in case he'd like to comment as well.


AFAIAC, I wasn't aware of package-quickstart but I see this is a new emacs feature (since 27.1) that is documented here.

I believe it'd be nice indeed to refactor this startup code provided this is backed up by CI tests.

So I have 2 questions (Cc @hendriktews, feel free to comment if you have an opinion!)

  1. what test should we add to the CI to test that the refactor indeed fixes the issue?

  2. is it needed to add some specific tests to ensure the refactor does not break existing "workflows"? (including MELPA's build (for instance, I've been told about this project: https://github.com/riscy/melpazoid (developed by one of the MELPA maintainers))), or not and I'm just worrying too much.

monnier commented 4 months ago

So I have 2 questions (Cc @hendriktews, feel free to comment if you have an opinion!)

  1. what test should we add to the CI to test that the refactor indeed fixes the issue?

Good question. Currently, I can reproduce the problem in the following way:

Apparently when ~/.emacs.d/package-quickstart.el gets compiled (which is done automatically in recent Emacsen), the problem does not appear.

  1. Is it needed to add some specific tests to ensure the refactor does not break existing workflows?

Most likely, yes. Several years ago I had proposed and installed a fairly different approach to this part of the initialization and it broke some other workflow so it got reverted, but I don't think we recorded the particular setup in a test. 🙁

hendriktews commented 1 month ago

Thanks for reporting the issue and the hints on testing. Am I right that before doing package-quickstart-refresh you have set package-quickstart to t and have installed Proof General as MELPA package? Could you give a hint on how to test your (or other) changes in proof-general.el? I hope it is not necessary to setup a fake Emacs package repo with the patched PG version for this?

monnier commented 1 month ago

Indeed, I have package-quickstart set to t, but I have not installed the package from MELPA (I would have used NonGNU ELPA instead). I have it installed using some scripts that have a similar effect to package-vc-install.

How to test such changes before installing them is indeed not completely trivial because of the need to make the modified code appear as an installed package (for package-quickstart-refresh).

Assuming your Git clone is in /foo/bar/proof-general/ and that there's no much else in /foo/bar/, you should be able to use something like the 100% untested test code ahead:

(write-region "(define-package \"proof-general\" \"4.6snapshot\" \"<Description>\" nil)" nil
              "/foo/bar/proof-general/proof-general-pkg.el")
(package-generate-autoloads 'proof-general "/foo/bar/proof-general/")
(add-to-list 'package-directory-list "/foo/bar/")
(package-quickstart-refresh)
(delete-file "~/.emacs.d/package-quickstart.elc")

after which starting a new emacs session should show (or not) the "Error during quickstart".

hendriktews commented 1 month ago

Thanks a lot, I will try to make a CI test out of this.