ProofGeneral
Incompatibility with `package-quickstart`
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
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
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!)
-
what test should we add to the CI to test that the refactor indeed fixes the issue?
-
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.
So I have 2 questions (Cc @hendriktews, feel free to comment if you have an opinion!)
- 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:
- M-x package-quickstart-refresh RET
- rm ~/.emacs.d/package-quickstart.elc
- Run
emacs.
Apparently when ~/.emacs.d/package-quickstart.el gets compiled (which
is done automatically in recent Emacsen), the problem does not appear.
- 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. 🙁
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?
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".