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 all 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
12 changes: 5 additions & 7 deletions ci/coq-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,9 @@
;;; Eval this to run the tests interactively <C-x C-e>
;;
;; (progn (load-file "coq-tests.el") (call-interactively #'ert))
;;
;; Note that loading this file triggers some side effects, such as:
;; (setq debug-on-error t)

(unless (and (boundp 'coq-test-dir) coq-test-dir) ; if set by ./test.sh
(if buffer-file-name
Expand All @@ -20,7 +23,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 +158,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 Expand Up @@ -364,10 +367,5 @@ Tactic failure: Cannot solve this goal."))))
(coq-test-goto-before "(*proof*)")
(backward-char 3)
(should (span-at (point) 'proofusing))))))




(provide 'coq-tests)

;;; coq-tests.el ends here
2 changes: 2 additions & 0 deletions ci/init-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,9 @@
(unless (package-installed-p 'ert-async)
(package-refresh-contents)
(package-install 'ert-async))

(eval-when-compile
;; This `require' command is just an "installation unit test".
(require 'ert-async))

;;; 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