ci/coq-tests.el fails completely with emacs 28

[hendriktews]

See testrun on PR #626 (https://github.com/ProofGeneral/PG/actions/runs/2450648668). All test fail with (error "Defining as dynamic an already lexical var"). The problem is independent of the Coq version, all combinations tested with emacs 28 fail the same way.

[hendriktews]

The problem is that

(let ((test-var nil))
  (eval '(defcustom test-var t "XXX")))

works fine in emacs 27 while it fails in internal--define-uninitialized-variable with "Defining as dynamic an already lexical var".
The failing tests have coq-auto-adapt-printing-width let-bound in coq-fixture-on-file and open in that let binding a .v file, which lets to loading coq/coq.el and the defpacustom auto-adapt-printing-width there.

[monnier]

FWIW, here's a patch I've had here for a while, which should happen to fix this problem:

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 8d36bab177..4e30d23c13 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -16,6 +16,7 @@
 (setq ert-batch-backtrace-right-margin 79)
 
 (require 'subr-x) ;; for (string-trim)
+(require 'ert)
 ;;(require 'ert-async)
 ;;(setq ert-async-timeout 2)
 
@@ -130,8 +131,9 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
 ;;   proof-shell-start()
 ;;   proof-shell-ready-prover()
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;; For info on macros: https://mullikine.github.io/posts/macro-tutorial
-;;; (pp (macroexpand '(macro args)))
+;; For info on macros: https://mullikine.github.io/posts/macro-tutorial
+;; (pp (macroexpand '(macro args)))
+  (defvar coq-auto-adapt-printing-width) ;Bind it dynamically!
   (save-excursion
     (let* (;; avoids bad width detection in batch mode 
            (coq-auto-adapt-printing-width nil)
@@ -151,7 +153,7 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
               (coq-mock body))))
       (coq-test-exit)
       (coq-set-flags nil flags)
-      (not-modified nil) ; Clear modification  
+      (set-buffer-modified-p nil) ; Clear modification  
       (kill-buffer buffer) 
       (when rmfile (message "Removing file %s ..." rmfile))
       (ignore-errors (delete-file rmfile)))))

[hendriktews]

IMO this is an emacs bug, see https://debbugs.gnu.org/cgi/bugreport.cgi?bug=55914

[hendriktews]

FWIW, here's a patch I've had here for a while, which should happen to fix this problem:

Thanks. However, I would probably prefer a solution that instantiates PG to Coq before starting any of the tests.

[erikmd]

Thanks a lot @hendriktews for spotting and fixing this! 👍