Turn warnings into code suggestions

[Alizter]

This will be a big project, but we should implement a way to check for specific warnings and give code suggestions when they are encountered. A general mechanism for doing so needs to be designed first, and then we can add them on as we go.

[ejgallego]

Maybe we should make this issue broader and include errors too?

Actually this is not hard to implement, see #29 , the difficult part is to get a maintainable architecture. For this to work, the suggestion itself has to come from Coq, so each time an error is updated the suggestion is updated too.

So there are two parts here:

• coq-lsp part, where we add the infra for the code suggestions / fixes which looks into a table + context
• Coq part, where we build the error + context -> edit function

For the last part, see the effort on introducing a proper error registration API in rocq-prover/rocq#12602

[ejgallego]

There was a recent PR in Coq proposing to add this information to the warnings; if that PR is accepted, we can implement quickfixes quite easily following the standard.

[Alizter]

@ejgallego What is the PR?

[ejgallego]

I think it is 19147