[Matafou]

This PR is currently based on another one: #893.

Switch all Elisp files to lexical binding.

Currently depends on #893 (its commits appear here until it is merged).

• Add the lexical-binding: t to the remaining files and fix the places that relied on dynamic binding (package-menu-async, warning-minimum-level, proverid).
• Variables shared with hooks (queueitems, string, action, scriptspan, curvalue): the function arguments that initialize them now have an -arg suffix, because in interpreted code a lexical argument of the same name hides the dynamic binding. This was breaking "compile before Require" when PG was loaded from sources.
• New test ci/simple-tests/coq-test-hook-variables.el covering these hooks with proof-shell.el both interpreted and byte-compiled.

Tested locally with Emacs 30.1 and rocq-9.2, rocq-9.0 and coq-8.20, without and with .elc: simple-tests, compile-tests, test-indent, make tests, qrhl-all, doc magic.

[Matafou]

@hendriktews I know you basically have no time to chheck. I will have a special look at proof-tree before merging.

[Matafou]

For the record proof-tree seems to work OK.

[Matafou]

I think it is worth explaining the problems encountered with the switch to lexical binding. It allows:

1. my fellow co-devs to check errors or oversigths,
2. maybe some expert (@monnier ?) can comment.

Note: this is a text generated by the llm (claude) that helped me during the switch.

Pitfalls of the switch to lexical binding

1. Variables shared with hook functions

proof-shell.el binds some variables, runs a hook, then reads the variables back. The hook functions read or modify them. With lexical binding, a let is not visible from the hook functions. These variables must therefore stay dynamic, with a file-level defvar (499c249):

• string, action and scriptspan for proof-shell-insert-hook;
• queueitems for proof-shell-extend-queue-hook;
• prover-was-busy for proof-shell-signal-interrupt-hook.

These are short, unprefixed names that are easy to miss. Find them by reading what the functions of each hook read or modify.

2. An argument with the same name as a dynamic variable

This was the trickiest bug. In proof-extend-queue, the argument was named queueitems, like the dynamic variable it initializes. The effect depended on the mode:

• Byte-compiled: everything worked.
• Interpreted (no .elc, as in the CI and in many users' setups): the lexical argument hid the dynamic binding when the variable was read back after running the hook, so the changes made by the hook functions were lost. For instance, with coq-compile-before-require, Require commands were sent to Coq before their dependencies were compiled.

Fixes:

• 79bac23 fixes queueitems;
• 9179010 systematically uses the suffix -arg for such arguments: queueitems-arg, action-arg, scriptspan-arg, and curvalue-arg in proof-assistant-format;
• ae6abad adds a test that the hook functions can read and modify these variables, with proof-shell.el both interpreted and byte-compiled.

Important

Test both interpreted and byte-compiled. The bug above only shows up in interpreted code.

3. Binding a variable of a library that is not loaded yet

If package.el is not loaded when the code is compiled or evaluated, (let ((package-menu-async nil)) …) has no effect: the binding is lexical and package.el does not see it. The fix is to declare the variable special with a defvar without value (917a845):

• package-menu-async in proof-upgrade-elpa-packages;
• warning-minimum-log-level and warning-minimum-level in proof-debug.

4. setq of a buffer-local variable named like an argument

In pg-pgip-process-newfile, (setq proverid proverid) was meant to set the buffer-local variable. With lexical binding, it sets the argument to itself and does nothing. Fixed with (set (make-local-variable 'proverid) proverid) (917a845).

5. Generic code stays backward compatible

The other provers (EasyCrypt, qRHL, …) use the same hooks. The names of the dynamic variables are unchanged. Only internal arguments are renamed, and defvar/declare-function forms are added (a34eeb0, 499c249, 9179010).

6. Method

• Test on several Coq/Rocq versions (rocq-9.2, rocq-9.0, coq-8.20) and on all test suites: simple-tests, compile-tests, test-indent, make tests, qRHL, and the doc.

• Run make -C ci/simple-tests clean first, otherwise the .success stamps skip tests.

• Switch in two steps for an easier review:

  • 8ad4d6e adds the lexical-binding cookie everywhere;
  • 917a845 fixes the places that relied on dynamic binding.

• The compiler warnings ("reference to free variable", "function not known to be defined") help a lot, but they do not detect pitfall 2.

• Clean up the compiler warnings first (a34eeb0, Fix unknown functions #893). Besides making the warnings that matter for lexical binding visible, this revealed real bugs that predate the switch, fixed separately in Fix category1 bugs #892: an eq comparison between a symbol and a string in pg-pgip.el (9d23486), and a misplaced parenthesis making most of a cond unreachable in pg-autotest.el (e8dff44).

[Matafou]

@cpitclaudel you might want to test company-coq against this branch. I don't know how much you rely on dynamic variables. It seems to work ok.

[monnier]

`proof-shell.el` binds some variables, runs a hook, then reads the variables back. The hook functions read or modify them. With lexical binding, a `let` is not visible from the hook functions. These variables must therefore stay dynamic, with a file-level `defvar` (499c249): - `string`, `action` and `scriptspan` for `proof-shell-insert-hook`; - `queueitems` for `proof-shell-extend-queue-hook`; - `prover-was-busy` for `proof-shell-signal-interrupt-hook`. These are short, unprefixed names that are easy to miss. Find them by reading what the functions of each hook read or modify.

BTW, while the immediate solution is to (defvar VAR) somewhere before the var is let-bound, in the longer term, we should rename those vars to have an appropriate namespace prefix.

### 4. `setq` of a buffer-local variable named like an argument In `pg-pgip-process-newfile`, `(setq proverid proverid)` was meant to set the buffer-local variable. With lexical binding, it sets the argument to itself and does nothing. Fixed with `(set (make-local-variable 'proverid) proverid)` (917a845).

Same here, except that the need for a namespace prefix is more urgent for buffer-local variable.