Identifier Completion API

[ejgallego]

A key step in building a useful language server for Coq is to provide "code completion", which is usually a function of the form completion_candidates : string -> string list [other approaches are often possible and desirable].

#7156 reminded me to open this issue. As of today, Coq's particular name resolution design makes non-trivial to implement this feature if I am correct. SerAPI doesn't even try to provide completion, and company-coq uses a quite heavy-handed approach (a search in the global namespace).

As of today, thanks to #608 some internal bits of the namespace API are exposed, but I am not sure we would like to mess with that. What would a sensible roadmap to expose a convenient completion API? Some other points to consider:

• we may want to allow efficient prefix-search,
• completion may happen in different contexts, and involve also goal/proofs variables,

[herbelin]

I don't know what would be a sensible roadmap wrt completion, but I'm rather happy with the "search in the global namespace" in company-coq and CoqIDE.

I'm otherwise missing being able to write things like Def^T to mean Definition, and so on.

Getting used to dynamic spell-checking with smartphones, I wonder how difficult would it be to have fixes for standard kinds of mispelling (e.g. mathc instead of match) automatically proposed?

Completion could indeed also involve goal/proofs variables.

[ejgallego]

I'm rather happy with the "search in the global namespace" in company-coq and CoqIDE.

Well, the only problem is that such global search takes several seconds [or even minutes sometimes], so it is not a very snappy interface to use for interactive typing. Not to say of the battery drain this incurs in laptops. That won't work at all for protocols such as the VSCode one that pings the API quite often.

One of my students in fact had to disable company-coq because of large battery drain due to this.

So IMHO we want to provide prefix-efficient access to the identifiers somehow.

[ejgallego]

cc to @cpitclaudel , as the company-coq maintainer he may want to comment on the design of this.

[cpitclaudel]

Why do you think searching in the global namespace is slow? And how did you measure the battery drain?
What's slow is getting the list of all identifiers, but then completion itself is rather fast.

[ejgallego]

Why do you think searching in the global namespace is slow?

It is O(n) where n is the size of all the required modules; usually with the context we work n > 30.000. See Declaremods.iter_all_segments.

And how did you measure the battery drain?

It was reported by my student [unfortunately he doesn't have a GH account], and we tracked it down to the Search calls, but my memory is not fully precise. Disabling company-coq solved the issue.

We could improve library to have a better indexing, however that still doesn't help a lot due to namespace constraints; so IMHO it is better to work at the Nametab level.

[cpitclaudel]

Sorry, were miscommunicating. It's pretty clear that the way company coq fetches identifiers from Coq is slow. But that doesn't mean that completion itself should be, or even is.

IOW, loading the completion list is slow, but after that completion doesn't have to be. With a proper API, there would be no need to load the completion list.

Also, did you actually observe minutes-long waits? On the full stdlib, loading identifiers takes around a second for me (which is way too much, of course, but nowhere near minutes)

[cpitclaudel]

Also, did you try disabling just the dynamic completion source in company-coq? Rather than the whole thing?

[ejgallego]

Also, did you try disabling just the dynamic completion source in company-coq? Rather than the whole thing?

I dunno, I'll ask my student to provide more details.

It's pretty clear that the way company coq fetches identifiers from Coq is slow. But that doesn't mean that completion itself should be, or even is.

Yeah, I was talking about the refresh mechanism indeed, but indeed that's a necessary part of the completion.

Also, did you actually observe minutes-long waits?

I don't recall if "minutes", but more than let's say 15-20 seconds with the very heavy environment sure; we use pretty old laptops tho :)

[cpitclaudel]

but indeed that's a necessary part of the completion.

No, it's not :)

[ejgallego]

Anyways, detaching the issue back from company-coq specifics, to me, the current Coq API to query identifiers is O(n) in the size of the module and that is not acceptable to me.

[Note that it iterates over all contents of the module]

[ejgallego]

No, it's not :)

Oh, then how do you query Coq for the list of identifiers?

[ejgallego]

Being a necessary part of the completion doesn't mean that the operation is run on every completion. But AFAICS you cannot do any completion at all unless you perform this operation once. Thus, it is a necessary part.

[cpitclaudel]

You don't. You query it for completions given a prefix. Then Coq uses proper data structures to answer that query efficiently.

[ejgallego]

You don't. You query it for completions given a prefix. Then Coq uses proper data structures to answer that query efficiently.

Ah oh, I meant "as of today".

[cpitclaudel]

You can build these data structures lazily at the same time as you populate the nametab, so every time you add a new identifier to the context you also add it to a trie of completion candidates.

[cpitclaudel]

Ah, yes, of course.

[cpitclaudel]

I don't think you can beat company-coq's approach today, but it's horrible indeed.

[ejgallego]

You can build these data structures lazily at the same time as you populate the nametab, so every time you add a new identifier to the context you also add it to a trie of completion candidates.

So indeed that's the idea this issue proposes, however, the way the nametab works makes implementation a bit tricky.

[ejgallego]

So the main question is what the ML-level API should be. The straightforward complete : string -> string list is OK, however there are many other possibilities that could be done.

[ejgallego]

I got something working nicely, will refine and submit a PR soon.