coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] CoqIDE upgrade on macOS caused a keyboard binding problem

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] CoqIDE upgrade on macOS caused a keyboard binding problem
Date: Tue, 02 May 2017 15:36:02 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f170.google.com
Ironport-phdr: 9a23:X0pmjRRVwQl8199wd3lTMr19pdpsv+yvbD5Q0YIujvd0So/mwa69YBaN2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27ZisNyjKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMM/hYr47noFsBtRixBQipBOPq1DBInHr20rc80+QnDArL2xAgH9IQv3TTttn0NaYSUeWwzKnJ1jjDYPZW1i386IjMaBwuvfaMXbdpfMfX1EIhGQTFjlCKpozkOTOYzuUNs26B7+phT+2jkWAnqxt3rzOyxckskpHEipwJxl3A7yl0w4Y4KcemREJmYNOoCoZcuiOGO4ZwX8gsWXtnuDwgxb0DoZO7fDYFyJAgxxPHbvyIaYmI4hb6WOaIPTd0mGtpeLyiixuw7USs0OL8Vs6z0FZFqipKjMPAuWwK1xzW8sSHS/198Vm92TuXyQzf9uVJLVo3mKfbMZIt3KM8m5sJvUjeHCL6hF36jKqMeUUl/uio5f7nYrLjppKEK490ih/xMqM0ls2+AOQ4Nw0OX2mA9OSz0b3s50z5QLFQgvIqlanZtYjWJd4Hqa6hHw9VzoEj5g6jADehydQUhGUILFZYeB2clIXpIFHPIPXgDfilmViskTFrx+rHPrL7GJnNIGLDw//deuN27FcZww4ux/he4YhVA/cPOqHdQEj04eDYjxgOAQ2xxuv9Ddx70MtKRWKCBemLMabXsHeH4+suJ6+HY4pD62W1EOQs+/O71SxxolQaZ6T8hZY=

Hi,

Thanks for reporting.

One of my students (under MacOS Sierra as well) had a similar problem. A few keys triggered shortcuts instead of writing into the editor, and he also couldn't produce the | symbol.

In his case, I think he had installed CoqIDE from the MacOS package, then coqtop from Mac ports.

The fix that you suggested worked for him.

Best,

Théo

PS: it seems that this error has also been reported on Bugzilla https://coq.inria.fr/bugs/show_bug.cgi?id=5367

Le ven. 21 avr. 2017 à 18:25, Miikka Koskinen <miikka.koskinen AT iki.fi> a écrit :

Dear Coq Club,

I just upgraded from CoqIDE 8.5pl1 to 8.6 on macOS Sierra and something went wrong. I managed to solve the problem, but since I couldn't find anything by googling, I'll post this here. Hopefully the next person having the same problem finds this.

Problem:
Pressing keys without any modifiers triggered shortcuts. For example, pressing `s` ran `simpl` and pressing `d` inserted a template for Definition. This means I was unable to type practically anything in the editor. I went back to 8.5pl1 but now it had the same problem!

Solution:
Close CoqIDE, move away (or remove) the CoqIDE configuration files in ~/Library/Application Support/coq and start CoqIDE again. You'll have to redo the configuration, but at least the editor works again.

Best regards,
Miikka Koskinen

Re: [Coq-Club] CoqIDE upgrade on macOS caused a keyboard binding problem, Théo Zimmermann, 05/02/2017