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

Fix "Bad bounding indices" error on invalid _CoqProject #708

Merged
merged 2 commits into from
Nov 28, 2023

Conversation

gasche
Copy link
Contributor

@gasche gasche commented Oct 3, 2023

Fixes #707.

The first commit is purely the bugfix. (Note: I didn't understand the previous code, as I am no Elisp expert, maybe it is doing something really important besides producing very obscure failure modes?)

The second commit turns warn into message. When testing with only the first commit I did not manage to see the warn string anywhere on my Emacs, so the error is a bit too silent to my taste. (We are noticing that the user _CoqProject is broken and just silently ignoring it.) message is slightly better. I wonder if error wouldn't be even better, but the current code logic is to be resilient and ignore the error, so I kept that.

@gasche
Copy link
Contributor Author

gasche commented Nov 28, 2023

cc @hendriktews : I don't know who to ping on this issue, but it is really simple and fixes a problem which cost me a bit of time

@monnier
Copy link
Contributor

monnier commented Nov 28, 2023

The error in the original code is silly: condition-case has the following syntax (condition-case VAR EXP1 (CONDITION EXP2)) where CONDITION says what errors we're catching. But the code puts directly EXP2 where (CONDITION EXP2) is expected, so warn ends up treated as CONDITION (a category of errors that doesn't actually exist).

Regarding warn vs message, warn is supposed to be less discrete than message, so I'm wondering what's going on. Maybe it gets displayed in a buffer that gets immediately "unshown" because we're displaying some PG buffer instead in that same window. This part should probably be turned into an Emacs bug.

@monnier monnier merged commit 879444c into ProofGeneral:master Nov 28, 2023
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

Successfully merging this pull request may close these issues.

confusing error on incorrect _CoqProject file
2 participants