The Coq mailing list

[Jonas Buhrkal Jensen <jobr AT itu.dk>]

With the risk of sounding like a troll, I must say that the best cure for 
Emacs pinky is Vim. The good news is that you can get Vim keybindings inside 
Emacs, and Proof General still works. Of the many vi/Vim emulators, it seems 
the most complete one is Evil:

http://emacswiki.org/emacs/Evil

I find Vim keys to be much more ergonomic since most commands are accessed 
with a-z or A-Z. Just be sure to remap ESC to Caps Lock. For the best 
results, learn the mappings in command mode well -- know what every ASCII 
character does, essentially.

Cheers,
Jonas

________________________________________
From: 
coq-club-request AT inria.fr
 
[coq-club-request AT inria.fr]
 on behalf of Thomas Braibant 
[thomas.braibant AT gmail.com]
Sent: Tuesday, August 28, 2012 5:50 PM
To: coq-club
Subject: [Coq-Club] Coq and RSI

Dear List,

I recently noticed that I started to develop an "emacs pinky" (a
particular kind of RSI) [1]. It is likely to be due to too many hours
of use of Proof General on a (mac) laptop keyboard, that put some
strain on my left hand side fingers (it is very difficult for me to
use the modifiers key on the right hand side of a mac book pro
keyboard).

This is not too bad for now, but I took some steps to improve my
condition [2], that I would like to share on this list (I hope that it
can help other people, and that maybe someone will have other ideas).
And, maybe assess if there are other people with the same  kind of
ergonomics problem, and try to improve things for everyone.

# What I should have done earlier
- remap caps lock to control on my MBP keyboard, and avoid using a
laptop keyboard in every day use

# What I have done so far
- borrowed an ergonomic keyboard (a Kinesis). My typing speed took an
heavy toll, but at least it forces me to adopt a good typing posture.
(Contra: I wonder what kind of strain this will put on my thumbs, and
it seems that I currently type only a few words per minute, but at
least this is for my own good)
- stopped using fancy moving-point macros (move forward one word, and
so forth, because it required too many modifiers uses).
- installed some emacs package to track the command I use the most [3]
and map them on function keys (f1 for check, f2 for print, f3 for
"insert match", f5 and f6 to go forward and backward in a proof
script), but this does not give precise information about what are the
"most common words/sequence key presses/patterns"...
- installed auto-complete [4], an emacs auto completion package that
makes it possible to complete Coq vernaculars (ever noticed that all
these start with a capital letter? you would certainly rant about it
if you were fumbling all your simultaneous key presses). That is,
auto-complete "def" into "Definition", and so on so forth. (I wish I
could have some semantic auto completion mechanism)

# What I could/would like to do
- try out CoqIDE (anyone that would like to bruise  his pinky and ring
finger on the left hand, and see if they can still work on CoqIde?)
- find an emacs way to exchange _ and - in my keyboard layout (a
particular instance of the following point)
- find out what would be a good keyboard layout (i.e., apply the
scientific/statistical method to pick/design a keyboard layout knowing
that most of my work implies writing Coq/OCaml programs). I have long
thought that there could be ergonomics improvements on that part, and
I am quite willing to pay the cost...
- find a way to shorten the number of key presses required to write
proof scripts (this is not relevant to my pinky condition, but since I
am trying to improve things, let's be broad); meaning that the average
workflow for me seems to involve too many "write something like [apply
foo.], fail, move the cursor, add parenthesis and arguments [apply
(foo bar).], try again, rework the indentation of the code by hand".

I would be glad to know of any other advices/experiences of people on this 
list.

Regards,
Thomas
[1] http://en.wikipedia.org/wiki/Emacs#Emacs_pinky
[2] (beside the obvious "improve work posture, take breaks, think
before you type, write proofs on paper")
[3] http://ergoemacs.org/emacs/command-frequency.html
[4] http://cx4a.org/software/auto-complete/index.html