Fix compilation issues and remove uses of old advice facility #670
Conversation
Compilation typically failed because the files required some coq*.el file when the `coq` subdir wasn't yet in `load-path`. While at it, enable lexical-binding where still missing, and fix some warnings. * ci/simple-tests/test-prelude-correct.el: * ci/simple-tests/test-coq-par-job-needs-compilation-quick.el: * ci/compile-tests/cct-lib.el: * ci/coq-tests.el: Eval `proof-ready-for-assistant` also during compilation so that (require 'coq*) doesn't error out. * ci/coq-tests.el (coq-fixture-on-file): Avoid `not-modified` which is "interactive only". * ci/init-tests.el: Don't fail compilation if `ert-async` is absent. * ci/compile-tests/cct-lib.el: Fix compile warnings about quotes in docstrings. Prefer #' to quote function names. * ci/simple-tests/test-coq-par-job-needs-compilation-quick.el (test-coq-par-test-data-invarint): Remove unused vars `test-id` and `req-obj-result`.
Replace all uses of `defadvice` with `advice-add`. * coq/coq.el: Remove coding cookie since .el files default to utf-8. (coq--unset-double-hit-advice): New function extracted from advice. (proof-electric-terminator-enable): Use `advice-add` instead of `defadvice`. * generic/pg-autotest.el (proof--debug-to-log): New function extracted from advice. (proof-debug): Advice with `advice-add` rather than `defadvice`. * generic/proof-syntax.el: * lib/bufhist.el: Update comments to refer to `advice-add` rather than `defadvice`.
Enable `lexical-binding` when missing in the files recently modified. Fix compile warnings about quotes in docstrings. Prefer #' to quote function names. * coq/coq.el: Require `proof-syntax`, `proof-useropts`, and `proof-utils` to silence some compiler warnings. (action, string): Move dynbound declaration to a smaller scope in `coq-preprocessing`. (coq-set-state-infos, coq-grab-punctuation-left): Fit docstring within 80 columns. (coq-diffs--setter, coq-diffs): Move `coq-diffs` var before first use. (coq-shell-theorem-dependency-list-regexp) (coq-dependency-menu-system-specific) (coq-dependencies-system-specific): Move vars before their first use. (coq-proof-tree-insert-evar-command): Simplify with `or`. (coq-preprocessing): Declare `action` and `string` locally to be dynbound. (coq-highlight-span-dependencies): Remove unused var `proof-pos`. <trailer>: Remove second coding cookie since .el files default to utf-8. * generic/pg-autotest.el: Use `lexical-binding`. (pg-autotest-test-script-randomjumps): Remove unused var `random-edit`. (pg-autotest-test-eval): Use lexical binding. * generic/proof-script.el (proof-colour-locked, proof-setup-imenu) (proof-colour-locked-span, proof-script-delete-spans) (proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window): Fit docstring within 80 columns. * generic/proof-syntax.el: Use `lexical-binding`. (proof-replace-regexp-in-string, proof-re-search-forward) (proof-re-search-backward, proof-re-search-forward-safe): Fit docstring within 80 columns. (proof-format): Use lexical binding. * doc/PG-adapting.texi: (Auto)Update accordingly.
monnier
force-pushed
the
scratch-defadvice-compilation
branch
from
c93e58e
to
6ee5a18
Compare
|
LGTM. Thanks Stefan. |
| @@ -1,4 +1,4 @@ | |||
| ;; This file is part of Proof General. | |||
| ;; This file is part of Proof General. -*- lexical-binding: t; -*- | |||
There was a problem hiding this comment.
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 👍
ci/init-tests.el
Outdated
| ;; FIXME: Merely loading a file should not have such side effects. | ||
| ;; We should move all of that code into a function. | ||
|
|
There was a problem hiding this comment.
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:
Line 39 in 8e688a6
Are you fine with this layout?
or would you still request a refactoring of these two files?
There was a problem hiding this comment.
Side question: would you recommend removing this line, perhaps? ↓
Line 371 in 8e688a6
which has no equivalent at the end of init-tests.el, for example.
|
@monnier Hi again!, FYI we had a PG telco this morning, and just to recap:
Thanks 👍👍 |
|
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:
Problem is that they may get loaded anyway.
or would you still request a refactoring of these two files?
The refactoring is trivial: just wrap the code within `(defun foo ()
...)` and then in your scripts add a corresponding `-f foo` when
launching Emacs.
|
|
> +;; FIXME: Merely loading a file should not have such side effects.
+;; We should move all of that code into a function.
+
Side question: would you recommend removing this line, perhaps? ↓
https://github.com/ProofGeneral/PG/blob/8e688a67703e4a132cc09bece1b746289868f6ab/ci/coq-tests.el#L371
which has no equivalent at the end of `init-tests.el`, for example.
For files which we don't `require`, it doesn't matter much either way.
|
|
* And also @monnier, feel free to comment if you have some hints regarding
my previous questions
Regarding the use of `lexical-binding`, it can leads to slightly more
efficient code when it matters, but more importantly it gives better
warnings and better matches programmers's expectations.
Also, the long term plan is to phase out the non-lexical-binding
dialect. Switching tends to introduce regressions, of course, but
that's because of the change itself, not because of the new dialect.
|
|
Hi Stefan!
OK, but I don't see why "they may get loaded anyway" :) To put things differently:
https://github.com/ProofGeneral/PG/blob/master/ci/coq-tests.el#L8 Furthermore, note that the https://github.com/melpa/melpa/blob/master/recipes/proof-general#L5-L8 But do you believe that the Finally, even if I see your point of "better safe than sorry", I don't see any issue with these two files, which are not distributed to end users. Still, I will push a small commit to remove the |
|
OK, but I don't see why "they may get loaded anyway".
Accidents happen. IOW, it's just prophylaxis.
[ Also because code tends to have a life of its own, so even if in this
specific case a bunch of constraints in the context should make it very
unlikely, it may bite when that code ends up used in another
context. IOW, it's poor style that leads to real problems in general
and it's rampant in ELisp, so I'm on a crusade against that style :-) ]
But **do you believe that the `ci` folder could be mistakenly exported to
NonGNU ELPA**? in which case, could you disable this?
A quick check of
http://elpa.nongnu.org/nongnu-devel/proof-general-4.6snapshot0.20221114.104412.tar
confirms that the `ci` subdir is *not* included in the tarballs.
OTOH, it will be included when the package is installed via
`package-vc`, Borg, and various other package systems which just
clone the source repository, of course.
Stefan
|
|
Hi @monnier ! thanks. |
These patches fix some compilation problems (when compiling with the generic ELPA scripts rather than with our ad-hoc makefile), replace uses of the old advice facility with the corresponding new functions, and then fixes some (not all) compilation warnings and cosmetic issues found in the affected files.