The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hello,

Le mardi 28 août 2012, Thomas Braibant 
<thomas.braibant AT gmail.com>
 a écrit :
> Dear List,
> ....
> - 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)

On this one notice that in pg there are already abbreviations for
almost all vernacular commands (I never type capital letters in pg).
The default "expand abbrev"  shortcut (c-x ') is cumbersome but you
can remap it to some f key. The default abbreviations use "holes" to
jump to next interesting places (another shortcut to map) which saves
you some cursor moving. Please give it a try and let me know what you
think of it. Abbrevs are displayed in the Coq/insert... menus.


You also have a way to enter commands or tactics interactively
(inspired by auctex mode). You have minibuffer completion there too
with tab. I think I am the only one to use it but maybe it is because
I never advertised these features. See the Coq/insert...menus for
shortcuts.


> - 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".

Do you know the shortut M-( ? And more important it's prefix arg? Once
used to it adding parenthesis afterward is a bit eased.


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

Here are some easy suggestions. I am open to ideas to add to pg.

A must: Use smart intros (c-c c-a c-i, or remap it :-)). You won't be
typing hypothesis names in intros anymore. I plan to have something
similar for "as H" namings too.

Use electric terminator? I hate it but it will save you typing some
"go forward" commands.



Even if this post is more about pg than Coq, this looks like a users
poll to me. I suggest we let it on Coq-club

Regards

Pierre Courtieu

2012/8/28 Thomas Braibant 
<thomas.braibant AT gmail.com>:
> 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