The Coq mailing list

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

Hello, as your answer is probably representative of a lot of pg users,
let me answer your mail by giving some examples illustrating some of
the features.

For the examples below I have this in my .emacs:

(global-set-key [f1]  'expand-abbrev)
(global-set-key [f2]  'holes-set-point-next-hole-destroy)
(global-set-key [f3]  'coq-insert-command)
(global-set-key [f4]  'coq-insert-tactic)
(setq completion-ignore-case t)


2012/8/29 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.

I too never use the menus. Actually they are useful to learn the
shortcuts and abbrevs than for real use (who would click on 3 menus
instead of typing "intros"?). They are there also to help if you don't
remember the syntax of a command.

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

Please do and tell me. I use it all the time (in ocaml too). I am
planning to replace my implementation of holes by something more
"mainstream emacs" like "skeletons". But I wonder if it is worth the
effort.

To jump to the next hole hit f2 (see .emacs above).

> But I think I would stick with the abbrevs (either
> using auto-complete or the default expand abbrev of proof general).

This *is* the default expand abbrev (with holes). Example:

fix<f1>

inserts:

Fixpoint # (#:#) {struct arg} : # :=
                 #.

where  "arg" and the #s are holes.

> The insert-stuff seems a bit too much...

Mmmh give it a try for the tactics you don't remember the abbrev. Here
again you don't need menus:

Example: let us say I don't remember the exact syntax of the Scheme
command. I just hit f3 and start typing the command in the minibuffer
*with completion*.

<f3>sch<TAB><space>I<TAB><return>

This is 9 keys instead of "Scheme # := Induction for # Sort #.". And
you see the possible completions when hitting <TAB>.

I use it less often than abbrevs but still sometimes.

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

I was not clear. You have only one shortcut to remember there: f4.
After that you type the tactic name in the minibuffer with completion.
Like the example above with f3 and commands.

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

I agree that this would be more ergonomic. Maybe an exception to the
parsing of apply  arguments could be hacked in Ltac, but then we would
ask the same for rewrite etc.

Just for the example, the prefix argument of M-( tells how many words
(forward or backward if negative) to enclose in the parenthesis. Here
after foo we need to give argument -1 (or just "-"):

apply foo<ESC>-<M-(> foo.

This is not perfect but useful.

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

Ha true.

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

Actually I am on a much more egocentric mode: I implement what I need
and what people ask me.

Suggestions very welcome.

regards,
Pierre

> With best regards,
> Thomas