The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

I responded to your second point in #coq, but for the benefit of the list, 
here it is.

(defun switch-hyphen ()
  (interactive)
  (define-key coq-mode-map (kbd "-") '(lambda () (interactive) (insert "_")))
  (define-key coq-mode-map (kbd "_") '(lambda () (interactive) (insert "-"))))
(add-hook 'coq-mode-hook 'switch-hyphen)

For those confused why this might be helpful, consider the popular naming 
convention of separating words with _ in Coq. I like the Scheme convention of 
using -, but that's not valid for identifier syntax in Coq.

-Ian

----- Original Message -----
From: "Thomas Braibant" 
<thomas.braibant AT gmail.com>
To: "coq-club" 
<coq-club AT inria.fr>
Sent: Tuesday, August 28, 2012 11:50:37 AM GMT -05:00 US/Canada Eastern
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