Stream: Proof General users

Topic: tactic completion scaling in company-coq

Karl Palmskog (Oct 18 2021 at 14:19):

I'm assuming it's OK to ask company-coq questions here.

I'm hitting a lot of scaling issues with tactic completion, specifically apply <blah> gets slower the further down in a (multi-hundred-lines) file I am in. Does anyone know how to fix this or completely turn off the company-coq tactic completion in some easy oneliner?

Pierre Courtieu (Oct 20 2021 at 14:54):

I think it is the best place to ask.
You can turn off hypothesis lookup in completion with this in your .emacs
(add-to-list 'company-coq-disabled-features 'context-backend)
and you can do M-x company-coq-features/context-backend tot oggle it at any time if I am not mistaken.
The slowing down is surprising though.

Pierre Courtieu (Oct 20 2021 at 14:55):

cc @Clément Pit-Claudel

Karl Palmskog (Oct 20 2021 at 15:29):

I usually use "hipster-completion", which tends to be enough for my needs, and there it scales well to 3000+ lines in a file

Clément Pit-Claudel (Oct 20 2021 at 20:35):

Long file with lots of imports? I'm guessing the slower completion is due to more identifiers being in context. Customize company-coq-disabled-features and remove the "dynamic" backends.

Karl Palmskog (Oct 20 2021 at 20:53):

yeah it's probably not uncommon for there to be hundreds (thousands) of identifiers in context after a while

Emilio Jesús Gallego Arias (Oct 21 2021 at 13:19):

@Clément Pit-Claudel since a few versions Coq has an API for "efficient" prefix matching, maybe that could help company-coq?

Clément Pit-Claudel (Oct 23 2021 at 02:58):

@Emilio Jesús Gallego Arias Is it enough? Company-coq doesn't do prefix matching, it does prefix matching modulo periods(so x.y.z matches xx.yy.zz)

Emilio Jesús Gallego Arias (Oct 23 2021 at 12:12):

@Clément Pit-Claudel not sure I understand that example, you mean instead xyz will match foo.xyz ?

Emilio Jesús Gallego Arias (Oct 23 2021 at 12:14):

I guess you could provide some feedback on https://github.com/coq/coq/issues/7164 ? Also, if you want an API to get the list of all identifiers and process it client side that's also doable

Clément Pit-Claudel (Oct 23 2021 at 18:51):

Emilio Jesús Gallego Arias said:

Clément Pit-Claudel not sure I understand that example, you mean instead xyz will match foo.xyz ?

Sorry, not sure how that message got in that state, I fixed it. xyz will not match foo.xyz, but f.xy will.

Clément Pit-Claudel (Oct 23 2021 at 18:51):

if you want an API to get the list of all identifiers and process it client side that's also doable

That's what I I do today (with Search), but it's too slow (and it would be worse accounting for aliases)

Clément Pit-Claudel (Oct 23 2021 at 18:54):

Emilio Jesús Gallego Arias said:

I guess you could provide some feedback on https://github.com/coq/coq/issues/7164 ?

Sure, but is there a description of the new API?

Last updated: Oct 13 2024 at 01:02 UTC