Tons of warnings when using certain PG features

[RalfJung]

For a few weeks now, the first time I am using certain PG features often leads to tons of warnings. When I do the same thing again, the warnings do not repeat. Feels a bit like some warning deduplication mechanism?

Here's what I just got when clicking "Proof General - Quick Options - Processing - Omit Proofs" (which was enabled, so this click disabled it):

Warning (comp): proof-unicode-tokens.el:46:25: Warning: reference to free variable ‘proof-mode-for-script’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:47:25: Warning: reference to free variable ‘proof-mode-for-response’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:48:25: Warning: reference to free variable ‘proof-mode-for-goals’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:58:49: Warning: reference to free variable ‘proof-assistant-symbol’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:67:4: Warning: reference to free variable ‘proof-assistant-symbol’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:79:28: Warning: reference to free variable ‘proof-mode-for-script’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:111:9: Warning: reference to free variable ‘proof-assistant-symbol’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:119:31: Warning: reference to free variable ‘proof-mode-for-script’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:133:8: Warning: reference to free variable ‘proof-assistant-symbol’ Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:142:6: Warning: the function ‘proof-shell-invisible-command-invisible-result’ might not be defined at runtime. Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:141:15: Warning: the function ‘proof-shell-available-p’ might not be defined at runtime. Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:140:15: Warning: the function ‘proof-shell-live-buffer’ might not be defined at runtime. Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:96:10: Warning: the function ‘proof-unicode-tokens-support-available’ is not known to be defined. Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:80:6: Warning: the function ‘proof-associated-buffers’ might not be defined at runtime. Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:79:6: Warning: the function ‘proof-buffers-in-mode’ might not be defined at runtime. Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:67:4: Warning: the function ‘unicode-tokens-mode’ might not be defined at runtime. Disable showing Disable logging
Warning (comp): proof-unicode-tokens.el:61:4: Warning: the function ‘unicode-tokens-initialise’ might not be defined at runtime. Disable showing Disable logging

[Matafou]

Looks like compilation messages. Probably the first time some file is loaded triggers it's compilation. @hendriktews any idea?

[Matafou]

@erikmd ?

[monnier]

Looks like compilation messages. Probably the first time some file is loaded triggers it's compilation. @hendriktews any idea?

Indeed, it's probably the native compilation: In Emacs≥28, if your Emacs is built with support for native compilation, `.elc` files get (re)compiled lazily (i.e. in response to their first use) to `.eln` files. Stefan

[RalfJung]

I am seeing warnings like this not just from PG but also other emacs plugins. It is quite annoying... but I found the 'native-comp-async-report-warnings-errors' option which will hopefully disable this behavior.

[Matafou]

@RalfJung Please let us know if this solved the annoyance.

@monnier is there something else we can do except fix each and every warning in the code?

[RalfJung]

So far it seems to have worked. Hard to tell though since this is non-reproducible -- it only happens the first time a feature is used (the first time a file is loaded, I guess).

[monnier]

So far it seems to have worked. Hard to tell though since this is non-reproducible -- it only happens the first time a feature is used (the first time a file is loaded, I guess).

You should be able to reproduce it at will if you remove the corresponding `.eln` file(s) which should be somewhere underneath ~/.emacs.d/eln-cache/

[RalfJung]

I deleted the cache and got no warnings. So, looking good!

[monnier]

@monnier is there something else we can do except fix each and every warning in the code?

Not really, no. Often most warnings are linked to problems of "missing `require`" so the warnings can be fixed more than one at a time, but it may necessitate significant reorganization.

[Matafou]

OK let us have this on our todo list then. I suspect in 6 months everybody will have switched to emacs 28 so we should at least reduce the warnings to a few ones before that...

[chdoc]

I just encountered this. FYI, the last release of Fedora to ship an emacs older than 28 went EOL in December. ^^

[Matafou]

Should we close this? The problem exists, but we won't fix it soon.