coq-lsp
coq-lsp copied to clipboard
Completion
Code completion gives suggestions about what the user might want to type. We need to investigate groups of objects and priorities.
Yup, there is already basic support in #41 , but needs more work before merge, and upstream thanks to https://github.com/coq/coq/pull/8766
Some more concrete TODOs here:
- we need to refine how to select the completion token from a position. Here we have two cases:
- the ast for the position at point is available, then we can actually build an interval map and use a fancy heuristic.
- parsing failed and only a text span is available. Maybe we can still call Coq's tokenizer on that span, but OMMV.
- completion of notations need to build a (cached) prefix map
- map objects to their kinds
Also there is the possibility to integrate the work on smart tactic completion that we started in this branch
https://github.com/jscoq/jscoq/commits/v8.15%2Bbernard_tactic_info
Basically that allows to understand what tactics like destruct
or inversion
may produce, and then complete for the user.
Implementation needs two steps:
- add support for speculative execution to Flèche (that's kind of easy)
- understand the results from the speculative tactic execution
Maybe we can move this to its own issue?
I cc @corwin-of-amber as this may be of his interest.