Completion becomes slower over time

[anton0xf]

How to reproduce

Use proof-general with company-coq for a long time. Wait a few seconds for auto-completion of any tactic or command. And this delay becomes bigger over time.

Then restart coq, disable company-coq and enable it again, open new empty test.v file and type "Def". Wait quite a few seconds.

Then edit company--begin-new function from comapany.el to print candidates in *Messages*:

(setq company-prefix (company--prefix-str prefix)
      company-backend backend
      c (company-calculate-candidates company-prefix ignore-case))
(message ">> backend: %s, candidates: %S" backend c) ;; <--- show candidates
(cond ...

Full function code here Then type "Defini" again and get (my emacs stuck here for a long time) something like this (I added some newlines):

>> backend: company-coq-master-backend, candidates: (#("Definition ident := term." 0 11
 (match-end 6 match-beginning 0 source man anchor ("11" . 11) insert 
"Definition @{ident} := @{term}." num-holes 2 company-coq-original-backend 
company-coq-refman-vernac-abbrevs-backend) 11 16 (match-end 6 match-beginning 0 
source man anchor ("11" . 11) insert "Definition @{ident} := @{term}." face 
(company-coq-snippet-hole-face company-tooltip company-tooltip company-tooltip 
company-tooltip company-tooltip company-tooltip company-tooltip company-tooltip 
company-tooltip company-tooltip company-tooltip company-tooltip default default default
 default default default default default default default default default company-tooltip 
company-tooltip company-tooltip company-tooltip company-tooltip company-tooltip 
company-tooltip company-tooltip company-tooltip company-tooltip company-tooltip 
company-tooltip default default default default default default default default default 
default default default company-tooltip company-tooltip company-tooltip company-tooltip
company-tooltip company-tooltip company-tooltip company-tooltip company-tooltip ...

It seems there are too many default and company-tooltip here.

Versions

• Ubuntu 20.04 - Linux 5.4.0-77-generic 86-Ubuntu SMP Thu Jun 17 02:35:03 UTC 2021 x86_64 x86_64 GNU/Linux
• GNU Emacs 26.3 (build 2, x86_64-pc-linux-gnu, GTK+ Version 3.24.14) of 2020-03-26, modified by Debian (But I had same issue with 25)
• The Coq Proof Assistant, version 8.13.2 (from nix)
• Coq Proof General Version 4.5-git. (proof-general-20210607.1422 from melpa)
• company-20210618.2105 from melpa
• company-coq-20210420.215 from melpa

[anton0xf]

Simpler way to see the "leak" is just

1. start emacs
2. open some *.v file
3. type "Def"
4. and see the value of variable company-coq--refman-vernac-abbrevs-cache

   
   company-coq--refman-vernac-abbrevs-cache is a variable defined in ‘company-coq.el’.
   Its value is shown below.

Documentation: Cache of parsed Coq vernac abbrevs taken from the RefMan.

Value: (#("Abort." 0 6 (num-holes 0 insert "Abort." anchor ("5x" . 335) source man))

("Abort ident." 0 6

(num-holes 1 insert #2="Abort @{ident}." anchor #1=("5x" . 337)
           source man)
6 11
(num-holes 1 face
           (company-coq-snippet-hole-face company-tooltip company-tooltip company-tooltip company-tooltip company-tooltip company-tooltip company-tooltip  ...

[full text](https://github.com/cpitclaudel/company-coq/files/6814719/company-coq--refman-vernac-abbrevs-cache.txt)

[anton0xf]

I did some research, and now I think that the problem is in combination of facts:

1. company-coq backends return candidates with some faces from their caches
2. company-mode calls add-face-text-property on strings obtained from candidates every time when it shows completion list
3. when you call add-face-text-property to add face to interval, which already have some face, it always extend face list (even if it already contains same face) and do it destructively
4. substrings and results of concatenation share faces lists with original string(s)

So faces lists of candidates in caches becomes very huge over time.

Some examples of 3 and 4: first and second

All of the above is right for both emacs 26.3 and 27.2 But in 27.2 results of concatenation don't share faces lists and (more important) add-face-text-property doesn't modify existing face list but creates new one. So I am going to test emacs 27.2.

Disclaimer: I didn't dig into the C sources of add-face-text-property and did all conclusions from my tests (see above), so things may be more complicated.

[anton0xf]

Issue #188 may be related

[anton0xf]

On emacs 27.2 this issue is not reproduced