Skip to content

Lexical autoloads#846

Merged
Matafou merged 2 commits intoProofGeneral:masterfrom
iwahbe:lexical-autoloads
Jan 7, 2026
Merged

Lexical autoloads#846
Matafou merged 2 commits intoProofGeneral:masterfrom
iwahbe:lexical-autoloads

Conversation

@iwahbe
Copy link
Contributor

@iwahbe iwahbe commented Sep 23, 2025

This PR makes 2 changes:

Fixes #845

@iwahbe iwahbe mentioned this pull request Sep 23, 2025
Closed
@Matafou
Copy link
Contributor

Matafou commented Jan 6, 2026

Hi. Thanks for this PR. Some test fail:

 FAILED  test-coq-par-job-needs-compilation-quick

with message:

create files with same time stamp failed

@hendriktews @monnier do you have an idea? Why would autoloads mess with this?

@hendriktews
Copy link
Collaborator

hendriktews commented Jan 6, 2026

@hendriktews @monnier do you have an idea? Why would autoloads mess with this?

The test test-coq-par-job-needs-compilation-quick now and then fails sporadically. Here it tries to create 2 files with the same timestamp in order to check a corner case in the old style quick (vio) compilation. The test gave up after 8 attempts to create the setting for this corner case failed. So this one is an error in the test.
But there are other, different errors, but to me they also look like spurious failures. Can you restart all the failing tests? (I did this in the past, but today I can't find the button for this.)
(I tried to write all these tests in a way such that execution speed does not matter for the test. But sometimes this is very hard or impossible, therefore we have a number of tests that fail if the execution speed is very slow.)

@Matafou
Copy link
Contributor

Matafou commented Jan 6, 2026

Neither can I re-run the CI. Probably because it is more than 30 days old. We should definitely be more reactive :-(.
@iwahbe can you rebase your branch and force push please? This should trigger the CI again.

iwahbe added 2 commits January 6, 2026 10:55
@iwahbe
Add -*- lexical-binding: t; -*- to generic/proof-autoloads.el
7567fb1 
Fixes ProofGeneral#845
@iwahbe
Explicitly require 'autoload for generating autoloads
2b1f289 
Without this, Emacs 31 fails to apply `make autoloads` with the following error.

	$ make autoloads
	***** MAKING AUTOGENERATED AUTOLOADS  ****
	emacs -batch -q -no-site-file -eval '(setq autoload-package-name "proof" generated-autoload-file "/Users/ianwahbe/.emacs.d/.cache/elpaca/repos/PG/generic/proof-autoloads.el")' -f 	batch-update-autoloads  generic/ lib/ coq/ qrhl/

	Error: void-function (batch-update-autoloads)
	  batch-update-autoloads()
	  command-line-1(("-eval" "(setq autoload-package-name \"proof\" generated-autoload-file \"/Users/ianwahbe/.emacs.d/.cache/elpaca/repos/PG/generic/proof-autoloads.el\")" "-f" "batch-update-autoloads" 	"generic/" "lib/" "coq/" "qrhl/"))
	  command-line()
	  normal-top-level()

	debug-early-backtrace...done
	Symbol’s function definition is void: batch-update-autoloads
	gmake: *** [Makefile.devel:249: autoloads] Error 255
@iwahbe iwahbe force-pushed the lexical-autoloads branch from d20009c to 2b1f289 Compare January 6, 2026 18:56
@iwahbe
Copy link
Contributor Author

iwahbe commented Jan 6, 2026

Rebased and waiting approval.

@Matafou
Copy link
Contributor

Matafou commented Jan 6, 2026

Indeed the rerun went well.
The goal of having lexical binding everywhere in PG is still uncertain, but I guess we can merge this one. @hendriktews do you agree?

@hendriktews
Copy link
Collaborator

hendriktews commented Jan 7, 2026

Thanks for this contribution! Yes, please go ahead!

@Matafou Matafou merged commit c3895ab into ProofGeneral:master Jan 7, 2026
140 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Emacs 31 warns on missing lexical bindings for generic/proof-autoloads.el

3 participants

@iwahbe @Matafou @hendriktews