The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello,

Le mardi 28 août 2012, Thomas Braibant <thomas.braibant AT gmail.com> a écrit :
> Dear List,

> # 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)

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