Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tons of warnings when using certain PG features #686

Open
RalfJung opened this issue Jan 31, 2023 · 12 comments
Open

Tons of warnings when using certain PG features #686

RalfJung opened this issue Jan 31, 2023 · 12 comments

Comments

@RalfJung
Copy link

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
Copy link
Contributor

Matafou commented Jan 31, 2023

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

@Matafou
Copy link
Contributor

Matafou commented Jan 31, 2023

@erikmd ?

@monnier
Copy link
Contributor

monnier commented Jan 31, 2023 via email

@RalfJung
Copy link
Author

RalfJung commented Feb 1, 2023

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
Copy link
Contributor

Matafou commented Feb 2, 2023

@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
Copy link
Author

RalfJung commented Feb 2, 2023

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
Copy link
Contributor

monnier commented Feb 2, 2023 via email

@RalfJung
Copy link
Author

RalfJung commented Feb 2, 2023

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

@monnier
Copy link
Contributor

monnier commented Feb 3, 2023 via email

@Matafou
Copy link
Contributor

Matafou commented Feb 4, 2023

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
Copy link

chdoc commented Feb 24, 2023

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

@Matafou
Copy link
Contributor

Matafou commented Sep 5, 2024

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants