Feature request: Interactive gallina hole filling

[Alizter]

When writing Gallina code, it is very common to leave a hole for a yet to be filled term. Coq will provide an error saying that a hole could not be inferred. We should be able to interactively display such errors as goals to the user when the cursor is over them. That way we could develop an Agda-style hole filling approach.

This idea has a lot of potential future directions, such as copying many of Agda's features, integration with equations etc. I feel like it is something that could be easily implemented in coq-lsp, and be very useful for users over existing UIs.

• Support for the obligations system added in: #262

[ejgallego]

Yes, that'd be great!

Some Coq packages would indeed greatly benefit from that, like Equations I understand.

There are some issues to overcome with Coq's current Declare.Proof API; at some point we took some notes about having such hole API in Coq but I think the pandemic got in the way, but I think there are some notes already in Coq wiki.

But indeed the main challenge to achieve this is difficulty of implementation, how do you think we can do this without quite significant changes to Coq?

This is also related to #97

[Alizter]

@ejgallego I can describe a hack to achieve something similar. For things like Fixpoint it won't work since proof and gallina environments have subtle differences with respect to implicit variables.

Definition bar := foo _.

Then coq-lsp internally changes it to:

Definition bar : _. Proof. refine (foo _).

And suggests that as a goal for the user. Then when the user fills in the hole a little bit, it will repeat this. We could also use program for this too.

All this is possible without changes to Coq. We could add proper hole support for Coq however, and I think that is a better long term direction.

[ejgallego]

Then coq-lsp internally changes it to:

How does coq-lsp detect that case?

Then when the user fills in the hole a little bit, it will repeat this.

What would the repeat yield?

We could also use program for this too.

That would produce a very different Coq script tho, and importing program could break even unrelated proofs.

[ejgallego]

We could add proper hole support for Coq however, and I think that is a better long term direction.

Actually there is something interesting that can be done today, as I exposed the obligation state in the Coq API on purpose.

You can think indeed about the obligations as holes, and explore some UI choices here.

But indeed the thing we never got to do what to discuss with Matthieu more about how to associate obligations with true holes in terms, but that is actually doable (but requires some changes in Coq itself)

Once the API is reworked, then pretyper and other parts of the system can easily generate holes, but Coq has what seems to me like a bad design flaw which is to identify goal with hole. That design error is later fixed using a "Shelve", which nobody knows what its rules really are, TTBOMK.

[Alizter]

How does coq-lsp detect that case?

Worst case we lex the error, or catch it earlier from Coq.

What would the repeat yield?

Not really repeat, but when the user has filled the hole in a bit more, then the error message will be new, and the process will repeat.

That would produce a very different Coq script tho, and importing program could break even unrelated proofs.

Yes, that is a problem.

Actually there is something interesting that can be done today, as I exposed the obligation state in the Coq API on purpose.

I was imagining having something like better control on obligations to achieve this also. I guess this would be the correct implementation we would eventually aim for. In the short term, we could experiment with some hacks.

[ejgallego]

For obligations control, everything you need is mostly in place, see Vernacstate.t

Worst case we lex the error, or catch it earlier from Coq.

Lexing seems tricky, in the end you are better catching indeed the right exception, but for a proof of concept that shouldn't matter a lot.

[TDiazT]

I think the hole filling/transformation part you're mentioning @Alizter should probably live on a separate presentation layer, rather than mixing it directly inside the LSP server, no? It might be more appropriate to include it in the VSCode plugin, although it loses generality (wrt. other editors). Otherwise I feel you start mixing some other responsibilities and it could introduce some unexpected terms for the user, making it harder to debug, print proper errors messages, etc.