Fix compilation issues and remove uses of old advice facility

[monnier]

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.

[Matafou]

LGTM. Thanks Stefan.

[erikmd]

@monnier Hi again!, FYI we had a PG telco this morning, and just to recap:

• @Matafou (the assignee of this PR) plans to merge this PR soon this week (not before Wednesday)
• Meanwhile, @hendriktews and I will take a closer look at some specific files to help with the review
• And also @monnier, feel free to comment if you have some hints regarding my previous questions

Thanks 👍👍

[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:

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.

[monnier]

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

[monnier]

• 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.

[erikmd]

Hi Stefan!

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.

OK, but I don't see why "they may get loaded anyway" :)

To put things differently:

• this ci/init-tests.el just acts as an adhoc init.el file (where the side-effects are desirable), loaded by the CI,
• and likewise ci/coq-tests.el is either loaded by the CI, or by us to debug tests, see also e.g.:

https://github.com/ProofGeneral/PG/blob/master/ci/coq-tests.el#L8

Furthermore, note that the ci folder is NOT exported to MELPA, according to this recipe I had submitted:

https://github.com/melpa/melpa/blob/master/recipes/proof-general#L5-L8

But do you believe that the ci folder could be mistakenly exported to NonGNU ELPA? in which case, could you disable this?

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 (provide 'coq-tests) line which seems unneeded, and replace (require 'ert-async nil t) with (require 'ert-async), because the init-tests.el's role is essentially to install ert-async, which is a package needed by (CI and locally-runnable) tests, so if (require 'ert-async) fails, it is valuable to know that it failed.

[monnier]

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

[erikmd]

Hi @monnier ! thanks. Actually I don't disagree with what you propose… but in thise case, could you please push some commit in your PR that implements this suggestion of yours?