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.

Sign up for GitHub

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

Jump to bottom

Feedback Tuning #108

Closed
ejgallego opened this issue Dec 22, 2022 · 4 comments · Fixed by #113
Closed

Feedback Tuning #108

ejgallego opened this issue Dec 22, 2022 · 4 comments · Fixed by #113
Milestone
0.1.1

Comments

@ejgallego
Copy link
Owner

All the "foo is defined" messages should not be displayed by default, that is too noisy; turn it into a server option.
@ejgallego ejgallego added this to the 0.1.1 milestone Dec 22, 2022
@Alizter
Copy link
Collaborator

Alizter commented Dec 23, 2022 •
edited
Loading

Will this require some message refactoring upstream?

@ejgallego
Copy link
Owner Author

ejgallego commented Dec 24, 2022 •
edited
Loading

Hopefully not, I think we can just drop (or better make an option) Info level messages and still have things working fine.

This issue is really a reminder to do this easy change. WDYT?

Note that Maxime fixed a lot of cases where Info vs Notice was used incorrectly in coq/coq#10612

@Alizter
Copy link
Collaborator

Alizter commented Dec 24, 2022

@ejgallego In that case, that seems fine.

@ejgallego
Copy link
Owner Author

I think so but indeed lots of fine tuning likely to be done here.

ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[diagnostics] Don't convert Coq "Info" messages to feedbacks
0f632ed 
We stop displaying messages such as "Foo is defined" as feedback by
default; users willing to see them can set the corresponding option.

Closes #108
ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[diagnostics] Don't convert Coq "Info" messages to feedbacks
cb5b688 
We stop displaying messages such as "Foo is defined" as feedback by
default; users willing to see them can set the corresponding option.

Closes #108
@ejgallego ejgallego mentioned this issue Dec 26, 2022
Merged
ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[diagnostics] Don't convert Coq "Info" messages to feedbacks
1b76793 
We stop displaying messages such as "Foo is defined" as feedback by
default; users willing to see them can set the corresponding option.

Closes #108
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
0.1.1
Development

Successfully merging a pull request may close this issue.

[diagnostics] Don't convert Coq "Info" messages to feedbacks ejgallego/coq-lsp
2 participants
@ejgallego @Alizter