search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

Default keybindings may cause serious strain in long proof sessions #399

Open ejgallego opened 5 years ago

ejgallego commented 5 years ago

It is not a secret that emacs default keybindings can cause serious problems to users; IMHO Proof General is not an exception and the default C-c C-n can create serious problems in the pinky due to C-c fixation.

I'd suggest we change the keybinding by default, or at least we provide an option and warn users about the perils of the defaults.

My current set of keybindings to make PG comfortable to use is:

(eval-after-load 'proof-script
    '(progn
       (define-key proof-mode-map "\M-n" 'proof-assert-next-command-interactive)
       (define-key proof-mode-map "\M-p" 'proof-undo-last-successful-command)
       (define-key proof-mode-map (kbd "M-RET") 'proof-goto-point)
       (define-key proof-mode-map (kbd "M-;") 'coq-About)))

This is just so much better.

cc: @JasonGross , have you experienced hand strain due to PG?

JasonGross commented 5 years ago

No, I haven't. Most of my strain comes from pressing down too hard with my wrists. But also I almost exclusively use C-c C-RET(proof-goto-point`), and I guess I spend long enough waiting for Coq slowness that it doesn't become a strain?

ejgallego commented 5 years ago

Yeah I guess your style of proof is highly automated. I have seen people suffer in software foundations and also math-comp style devs, where it is far more common to go back and forth I'd say.

Matafou commented 5 years ago

I do agree with your opinion about pg keybindings but actually almost all short keystroke are already bound globally. It is considered bad practice for a major mode to override them by default. We can provide an optional “default ergonomical config” but I guess 95% of the users won’t like it and complain... For instance I have seen people map assert-next to F1 and undo-last to F2. But probably a lot of people bound this already to something else. I have ctrl-click for Print a constant under mouse cursor. And ctrl-rightclick for Check, but again these keybindings correspond to global emacs keybindings and it is considered bad practice to override them by default. We could provide template configurations maybe?

anton-trunov commented 5 years ago

FWIW, I switched to Spacemacs because of this issue. Nowadays, I bind ,. to proof-goto-point in normal mode.