Feedback from Coq Community Survey 2022.

[Zimmi48]

The Coq Community Survey 2022 contained the question "Are there any features of Company-Coq that you find distracting or that you manually disable? Which ones?". Here are the answers to this question:

1. I disabled dynamic completing because it causes emacs to hang.

2. the "hello"

3. Ligatures disabled for teaching

4. I usually disable the spinner manually and am unsure whether this still makes a difference

5. Not really, it's good software. It's auto-completion suggestions are not always helpful.

6. Certain ligatures are bad and I want to turn them off. It’s hard to do it unlike the fstar plugin.

7. Printing unicode version of ascii symbols.

8. Not feature-specific, but sometimes I just disable the entire plugin.

9. The spinner was a huge pain, until it was disabled by default. Symbol prettification gets in the way with Unicode notation (it actually caused a bug at one point).

10. Pretty symbols (I just use Unicode when necessary)

11. modeline icon

12. hello
    outline
    refactorings
    alerts
    prettify-symbols
    spinner
    obsolete-settings

13. In the end most of them except suggestions. The prettifying leads to ugly and badly indented code and it is slows down emacs a lot.

14. ligatures outside of equations

15. Both prettify-symbols and smart-subscripts mess up indentation. Some autocompletion features really slow down the editor.

16. I tend to leave my goals unfolded as it helps me to identify where I need to refactor things, and I initially found it annoying to accidentally fold a bulleted/braced subgoal. While I do use it sparingly during meetings, I am relatively ambivalent about it for my day-to-day work.

17. that it folds proofs when I click on '{' and I don't remember what key to use to unfold it

18. I’m happy company-coq has an easy way of disabling certain features. I find smart-subscripts, company-defaults, prettify-symbols, code-folding, and hello distracting; so I disable them.

19. Slow

20. The indentation is often wrong for ssreflect proof scripts (e.g., "by"). This is so annoying that it's sometimes easier to just give up on it.

21. sometimes I struggle when I don't want autocompletion (i.e., I'm fine with the current prefix, and I just want to exit autocompletion).

22. Snippet insertion and code folding are two features with marginal utility (IMO), yet I find that both are quite easy to trigger accidentally, screwing up my editor state sometimes to the extent that I must restart Emacs to recover.

23. Rendering keywords as Unicode symbols (like forall, exists, etc.)

24. I disabled most of the pop-up completion.

25. No

26. I always disable prettify-symbols-mode (the disconnect between what I read and what I type is distracting), and all ”electricity” (though I don’t remember whether that’s from Company-Coq or core Proof General). I sometimes disable Company-Coq entirely, since over large projects, the autocompletions are often slow to load, which badly impacts responsiveness while typing fast. E.g. while typing “apply my_lemma”, after I’ve typed “ap”, Emacs takes a second or so to load the autocompletion list with many variants of “apply”, before registering the rest of what I’ve typed. This can disrupt coding flow quite badly!

27. • I would prefer default on-demand auto-completion menus
    • I configure prettification manually

28. Automatic indentation and autocompletion of snippets are frequently hindering rather than helping.

29. The documentation showing up all the time. I need to change this but have not found time yet.

30. bad auto-complete suggestions, underscores creating subscripts, automatic unicode-ification messing up indentation

31. numbers as subscripts, all popups, autocomplete

32. Activity spinner

33. Unicode pretty-printing.

34. It is very slow

35. Unicode symbols (prettify-symbols)

36. I do not like autocomplete with popups, it's too invasive for me, so I do not use Company-Coq.

37. I disable coqdoc prettify-symbols smart-subscripts title-comments because I find them distracting.