The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hello,

Thanks a lot for your answers.

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

Confession: I never used these menus. Now that I see that it can be
used to enter sketches of code with holes, I understand that it can be
useful. I need to give it a real try, and see if it increases my
productivity.  But I think I would stick with the abbrevs (either
using auto-complete or the default expand abbrev of proof general).
The insert-stuff seems a bit too much...


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

I am not sure I understand how to use the shortcuts for the tactics.
And I think it would be way too much shortcuts to remember.
Abbreviations are another story though, and it is nice to learn of
that. But in any case, typing tactics is fine for me (no modifier key
presses needed).


> 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 think my current .emacs does that for me each time I press "(".
(Yet, I do not understand the part about the prefix arg.) In any case,
I think my point was that it could be more ergonomic to be able to
write "apply foo bar" rather than "apply (foo bar)" (in the (common)
situation when you need to give more arguments to a lemma, after
trying first the tactic without arguments for the lemma).

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

I am not sure I would use that: most of the time the hypothesis that I
want to introduce at the beginning of a proof are on the left side of
the ":", and in a proof, most of the time, I prefer to pick meaningful
names rather than the one that are displayed.

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

Electric terminator do not work when one uses modules ("apply
Foo.lemma"). BTW, when doing go forward at the end of a line that ends
with a period, pg moves the cursor to the next line, which is most
often not what I want it to do (I want to fill this damn line, not to
use one single tactic per line!).

Which makes we wonder: as (the/a?) developer of the PG Coq mode, have
you thought about gathering statistics about what kind of commands
people use, and which one are never used? This could provide you with
good feedback about what is working well, and what is not working...
(this keyfreq package is really interesting from that point of view).

With best regards,
Thomas