Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix compilation issues and remove uses of old advice facility #670

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Fix compilation issues and remove uses of old advice facility #670

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8985fa9
ci/*.el: Fix compilation problems using the ELPA scripts
monnier Sep 21, 2022
d58636b
Use the new advice facility
monnier Sep 21, 2022
6ee5a18
Various cosmetic changes and fix some warnings
monnier Sep 21, 2022
e71b59e
test: Clarify ci/{init-tests.el,coq-tests.el}
erikmd Nov 28, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions ci/compile-tests/cct-lib.el
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
;; This file is part of Proof General.
;; This file is part of Proof General. -*- lexical-binding: t; -*-
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi @monnier !

I am a aware that indeed, adding lexical-binding as soon as possible is a good rule-of-thumb if we can.

But just to name a potential issue, we had found some months ago when discussing in our regular PG telco that when you had enabled this mode everywhere in the code maintained by @hendriktews, the lexical-binding had broken some invariants :-/ (in some subtle cases I don't remember now)

And even I'm not fully savvy of all the implications of this mode, I just wanted to raise this point and say that maybe, it'd be wise not to add it blindly without some additional discussion…

So @monnier, could you try to summarize all the pros and cons of adding it?

Anyway, thanks for proposing this PR 👍

;;
;; © Copyright 2020 - 2021 Hendrik Tews
;;
Expand Down Expand Up @@ -30,7 +30,7 @@
;; require proof-site, otherwise proof-ready-for-assistant won't be
;; defined.
(require 'proof-site)
(proof-ready-for-assistant 'coq)
(eval-and-compile (proof-ready-for-assistant 'coq))
(require 'coq-compile-common)
(require 'ert)

Expand Down Expand Up @@ -90,7 +90,7 @@ cannot be accessed."
"Return an assoc list of FILES with their modification times.
The modification time is an emacs time value, it's nil if file
cannot be accessed."
(mapcar 'cct-record-change-time files))
(mapcar #'cct-record-change-time files))

(defun cct-split-change-times (file-change-times files)
"Split assoc list FILE-CHANGE-TIMES.
Expand Down Expand Up @@ -162,7 +162,7 @@ Runs `cct-before-busy-waiting-hook' and
PG uses a number of overlapping and non-overlapping spans (read
overlays) in the asserted and queue region of the proof buffer,
see the comments in generic/proof-script.el. Spans of type
vanilla (stored at 'type in the span property list) are created
vanilla (stored at `type' in the span property list) are created
for real commands (not for comments). They hold various
information that is used, among others, for backtracking.

Expand All @@ -185,7 +185,7 @@ and `current-message' does not return anything."

(defun cct-check-locked (line locked-state)
"Check that line LINE has locked state LOCKED-STATE
LOCKED-STATE must be 'locked or 'unlocked. This function checks
LOCKED-STATE must be `locked' or `unlocked'. This function checks
whether line LINE is inside or outside the asserted (locked)
region of the buffer and signals a test failure if not."
(let ((locked (eq locked-state 'locked)))
Expand Down Expand Up @@ -216,7 +216,7 @@ region of the buffer and signals a test failure if not."

(defun cct-check-files-locked (line lock-state files)
"Check that all FILES at line number LINE have lock state LOCK-STATE.
LOCK-STATE must be either 'locked or 'unlocked. FILES must be
LOCK-STATE must be either `locked' or `unlocked'. FILES must be
list of file names."
(when cct--debug-tests
(message "check files %s at line %d: %s"
Expand All @@ -233,7 +233,7 @@ list of file names."
The comparison treats ANCESTORS as set but the file names must
be `equal' as strings.

Ancestors are recoreded in the 'coq-locked-ancestors property of
Ancestors are recoreded in the `coq-locked-ancestors' property of
the vanilla spans of require commands, see the in-file
documentation of coq/coq-par-compile.el."
(let ((locked-ancestors
Expand Down
6 changes: 4 additions & 2 deletions ci/coq-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@
(setq coq-test-dir (file-name-directory buffer-file-name))
(error "You should set 'coq-test-dir, or run coq-test.el from a file buffer.")))

;; FIXME: Merely loading a file should not have such side effects.
;; We should move that code into a function.
(setq debug-on-error t) ; open the debugger on error -- may be commented-out
(setq ert-batch-backtrace-right-margin 79)

Expand All @@ -20,7 +22,7 @@
;;(setq ert-async-timeout 2)

;; Load Coq instance of Proof General now.
(proof-ready-for-assistant 'coq)
(eval-and-compile (proof-ready-for-assistant 'coq))
(require 'coq)

;;; Code:
Expand Down Expand Up @@ -155,7 +157,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)))))
Expand Down
8 changes: 7 additions & 1 deletion ci/init-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,9 @@

;;; Code:

;; FIXME: Merely loading a file should not have such side effects.
;; We should move all of that code into a function.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi @monnier!
I was the main author of this file init-tests.el and coq-tests.el, and I'm totally aware that they raise unusual side effects at load time, but note that these two files are not intended at all to be required by users: the presence of these two files is just to make it possible (and easy) to load all the features, mocks, and so on, from the CI (without writing quoted-cluttered elisp code directly in the bash script) → see in particular the following line:

PG/ci/test.sh

Line 39 in 8e688a6

assert emacs --batch -l ert --eval "$form" -l init-tests.el -l proof-general.el -l coq-tests.el -f ert-run-tests-batch-and-exit

Are you fine with this layout?

or would you still request a refactoring of these two files?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Side question: would you recommend removing this line, perhaps? ↓

PG/ci/coq-tests.el

Line 371 in 8e688a6

(provide 'coq-tests)

which has no equivalent at the end of init-tests.el, for example.

;; Setup MELPA
(require 'package)
(setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3")
Expand All @@ -24,7 +27,10 @@
(unless (package-installed-p 'ert-async)
(package-refresh-contents)
(package-install 'ert-async))

(eval-when-compile
(require 'ert-async))
;; FIXME: Why do we have this `require' and why is it within
;; an `eval-when-compile'?
(require 'ert-async nil t))

;;; init-tests.el ends here
13 changes: 7 additions & 6 deletions ci/simple-tests/test-coq-par-job-needs-compilation-quick.el
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
;;; test-coq-par-job-needs-compilation-quick.el --- test compilation internals
;;; test-coq-par-job-needs-compilation-quick.el --- test compilation internals -*- lexical-binding: t; -*-

;; This file is part of Proof General.

;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
;; Portions © Copyright 2003-2022 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 2021 Hendrik Tews
Expand Down Expand Up @@ -33,7 +33,7 @@
;;; Code:

(require 'proof-site)
(proof-ready-for-assistant 'coq)
(eval-and-compile (proof-ready-for-assistant 'coq))
(require 'coq-par-compile)
(eval-when-compile (require 'cl-lib))

Expand Down Expand Up @@ -756,7 +756,7 @@ relative ages.")
"Wellformedness check for the test specifications."
(mapc
(lambda (test)
(let ((test-id (format "%s" (car test))))
;; (let ((test-id (format "%s" (car test))))
;; a test is a list of 4 elements and the first element is a list itself
(should
(and
Expand All @@ -770,7 +770,8 @@ relative ages.")
(quick-mode (car variant))
(compilation-result (nth 1 variant))
(delete-result (nth 2 variant))
(req-obj-result (nth 3 variant)))
;; (req-obj-result (nth 3 variant))
)
;; the delete field, when set, must be a member of the files list
(should (or (not delete-result)
(member delete-result files)))
Expand All @@ -780,7 +781,7 @@ relative ages.")
(should (not delete-result))
(should (eq compilation-result
(not (eq (car (last (car test))) 'vo)))))))
(cdr test))))
(cdr test))) ;; )
coq--par-job-needs-compilation-tests))

(defun test-coq-par-sym-to-file (dir sym)
Expand Down
4 changes: 2 additions & 2 deletions ci/simple-tests/test-prelude-correct.el
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
;; This file is part of Proof General.
;; This file is part of Proof General. -*- lexical-binding: t; -*-
;;
;; © Copyright 2021 Hendrik Tews
;;
Expand All @@ -21,7 +21,7 @@
;;
;; Load stuff for `coq--version<'
(require 'proof-site)
(proof-ready-for-assistant 'coq)
(eval-and-compile (proof-ready-for-assistant 'coq))
(require 'coq-system)

(defconst coq--post-v810 (coq--post-v810)
Expand Down
Loading