<ESC> in editing mode triggers Proof General autocomplete

[carlpaten]

Description

Pressing <ESC> to enter normal mode triggers Proof General autocomplete.

Reproduction guide 🪲

• Install Proof General (I used the Ubuntu package)
• Start Emacs
• Open a .v file
• Enter editing mode with i
• Write o
• Press <ESC>

Observed behaviour: 👀 💔
o is autocompleted into omega; editing mode switched to normal mode

Expected behaviour: ❤️ 😄
No autocompletion, just mode switching.

System Info 💻

• OS: gnu/linux
• Emacs: 25.1.1
• Spacemacs: 0.200.9
• Spacemacs branch: master (rev. 8e1af14)
• Distribution: spacemacs
• Editing style: vim
• Completion: helm
• Layers:

(helm emacs-lisp)

• System configuration features: JPEG SOUND GPM DBUS NOTIFY ACL LIBSELINUX GNUTLS LIBXML2 ZLIB

Backtrace 🐾

[carlpaten]

The report above was hand-transcribed, apologies for any errors.

I would love a work-around, I can't figure out what's going on.

[chkl]

I'm experiencing the same problem after a package upgrade.

System Info 💻

• OS: gnu/linux (Archlinux)
• Emacs: 25.2.1
• Spacemacs: 0.200.9
• Spacemacs branch: master (rev. 8e1af14)
• Graphic display: t
• Distribution: spacemacs
• Editing style: vim
• Completion: helm
• Layers:

(javascript html markdown haskell latex coq helm auto-completion evil-commentary emacs-lisp git org spell-checking syntax-checking version-control)

• System configuration features: XPM JPEG TIFF GIF PNG RSVG IMAGEMAGICK SOUND GPM DBUS GCONF GSETTINGS NOTIFY ACL GNUTLS LIBXML2 FREETYPE M17N_FLT LIBOTF XFT ZLIB TOOLKIT_SCROLL_BARS GTK3 X11 MODULES
  y

[sindikat]

I found out that this is Evil's fault, not company-coq's. Solution is to set

(setq evil-want-abbrev-expand-on-insert-exit nil)

before Evil loads (e.g. in Spacemacs this means to put the above line in dotspacemacs/user-init). I recommend to close this issue.

See also:

• <ESC> in editing mode triggers Proof General autocomplete olivierverdier/spacemacs-coq#14 (comment)
• Expansion triggers at unfortunate times when using Evil-mode ProofGeneral/PG#174

[Blaisorblade]

Thanks a lot for the workaround!

1. It looks like this is just the interaction of Evil and Coq — (coq-mode-abbrev-table) is the only table with predefined entries. And that's why the problem seems Coq-related?

I recommend to close this issue.

2. Nobody has to fix this, of course, but I understand Spacemacs wants to work well out-of-the-box, and right now this bit doesn't.

Not sure how to achieve that though, I guess many people rely on the default? Maybe making coq-mode default autocompletions opt-in might be a simple solution with the minimal disruption for other people—not sure though. Or maybe that's silly.

[bmag]

Per a comment in the issue on PG's repo, another workaround is to prevent the abbrev table from being installed, by evaluating this expression before loading coq-abbrev.el:

(setq coq-mode-abbrev-table '())

An option to solve the issue is to add a variable in coq layer's config.el file for opting into using coq's abbreviation table. If the variable is nil, coq layer will call (setq coq-mode-abbrev-table '()), otherwise coq layer won't make that call and coq's abbreviation table will be generated and installed.

[github-actions]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Please let us know if this issue is still valid!