coq: update key bindings and README
README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
This commit is contained in:
parent
8b72130fc5
commit
fe168f07b3
|
@ -32,60 +32,58 @@ Official installers for MacOS and Windows are available from:
|
|||
Linux users can build from source or consult with their own package managers.
|
||||
|
||||
* Key bindings
|
||||
All Coq specific bindings are prefixed with the major-mode leader ~SPC m~.
|
||||
|
||||
** Laying out windows
|
||||
|
||||
| Key Binding | Description |
|
||||
|-------------+-----------------------|
|
||||
| ~ll~ | Re-layout windows |
|
||||
| ~lc~ | Clear response buffer |
|
||||
| ~lp~ | Show current proof |
|
||||
| ~SPC m l c~ | Clear response buffer |
|
||||
| ~SPC m l l~ | Re-layout windows |
|
||||
| ~SPC m l p~ | Show current proof |
|
||||
|
||||
** Managing prover process
|
||||
|
||||
| Key Binding | Description |
|
||||
|-------------+-----------------------------------------------------------------|
|
||||
| ~pc~ | Interrupt prover |
|
||||
| ~px~ | Quit prover |
|
||||
| ~pr~ | Retract buffer - rewinds and moves point to beginning of buffer |
|
||||
| ~pb~ | Process buffer - processes and moves point to end of buffer |
|
||||
| ~SPC m p i~ | Interrupt prover |
|
||||
| ~SPC m p p~ | Process buffer - processes and moves point to end of buffer |
|
||||
| ~SPC m p q~ | Quit prover |
|
||||
| ~SPC m p r~ | Retract buffer - rewinds and moves point to beginning of buffer |
|
||||
|
||||
** Prover queries
|
||||
The mnemonic for =a= is "ask".
|
||||
|
||||
| Key Binding | Description |
|
||||
|-------------+---------------------------------------------|
|
||||
| ~af~ | Search (mnemonic: "find theorems") |
|
||||
| ~ao~ | Show an outline of the current proof script |
|
||||
| ~ap~ | Print |
|
||||
| ~ac~ | Check |
|
||||
| ~ab~ | About |
|
||||
| ~aip~ | Print (showing implicits) |
|
||||
| ~aic~ | Check (showing implicits) |
|
||||
| ~aib~ | About (showing implicits) |
|
||||
| ~anp~ | Print (showing all) |
|
||||
| ~anc~ | Check (showing all) |
|
||||
| ~anb~ | About (showing all) |
|
||||
| Key Binding | Description |
|
||||
|---------------+---------------------------------------------|
|
||||
| ~SPC m a a~ | Print |
|
||||
| ~SPC m a A~ | Print (showing all) |
|
||||
| ~SPC m a b~ | About |
|
||||
| ~SPC m a B~ | About (showing all) |
|
||||
| ~SPC m a c~ | Check |
|
||||
| ~SPC m a C~ | Check (showing all) |
|
||||
| ~SPC m a f~ | Search (mnemonic: "find theorems") |
|
||||
| ~SPC m a i b~ | About (showing implicits) |
|
||||
| ~SPC m a i c~ | Check (showing implicits) |
|
||||
| ~SPC m a i i~ | Print (showing implicits) |
|
||||
| ~SPC m a o~ | Show an outline of the current proof script |
|
||||
|
||||
** Moving the point
|
||||
|
||||
| Key Binding | Description |
|
||||
|-------------+---------------------------------|
|
||||
| ~g.~ | Go to last processed command |
|
||||
| ~ga~ | Go to start of command at point |
|
||||
| ~ge~ | Go to end of command at point |
|
||||
| ~gd~ | Go to definition at point |
|
||||
| ~SPC m g e~ | Go to end of command at point |
|
||||
| ~SPC m g g~ | Go to definition at point |
|
||||
| ~SPC m g l~ | Go to last processed command |
|
||||
| ~SPC m g s~ | Go to start of command at point |
|
||||
|
||||
** Inserting
|
||||
|
||||
| Key Binding | Description |
|
||||
|-------------+-----------------------------------------------------------------|
|
||||
| ~il~ | Extract lemma from current goal - exit with ~C-RET~ (not ~C-j~) |
|
||||
| ~im~ | Insert =match= on a type |
|
||||
| ~ie~ | Insert =End <section-name>= |
|
||||
| ~M-RET~ | Insert regular match branch |
|
||||
| ~M-S-RET~ | Insert =match goal with= branch |
|
||||
| Key Binding | Description |
|
||||
|-----------------+-----------------------------------------------------------------|
|
||||
| ~SPC m M-RET~ | Insert regular match branch |
|
||||
| ~SPC m M-S-RET~ | Insert =match goal with= branch |
|
||||
| ~SPC m i e~ | Insert =End <section-name>= |
|
||||
| ~SPC m i l~ | Extract lemma from current goal - exit with ~C-RET~ (not ~C-j~) |
|
||||
| ~SPC m i m~ | Insert =match= on a type |
|
||||
|
||||
Note the last two are regular =company-coq= bindings, left alone since they are
|
||||
most useful in insert mode. The full =company-coq= tutorial showcasing all
|
||||
|
@ -96,7 +94,7 @@ company-coq-tutorial=.
|
|||
** There are empty square boxes in place of math operators
|
||||
Math symbols present in your buffer (e.g. forall exists) will attempt to be
|
||||
prettified, if you are seeing empty square boxes this means an appropriate math
|
||||
symbol cannot be found in your font. You can either install a appropriate math
|
||||
symbol cannot be found in your *font*. You can either install a appropriate math
|
||||
font, or disable the feature by adding the following snippet to the your
|
||||
=dotspacemacs/user-config=.
|
||||
|
||||
|
|
|
@ -0,0 +1,14 @@
|
|||
;;; packages.el --- Coq Layer configuration File for Spacemacs
|
||||
;;
|
||||
;; Copyright (c) 2012-2017 Sylvain Benner & Contributors
|
||||
;;
|
||||
;; Author: Sylvain Benner <sylvain.benner@gmail.com>
|
||||
;; URL: https://github.com/syl20bnr/spacemacs
|
||||
;;
|
||||
;; This file is not part of GNU Emacs.
|
||||
;;
|
||||
;;; License: GPLv3
|
||||
|
||||
;; variables
|
||||
|
||||
(spacemacs|define-jump-handlers coq-mode)
|
|
@ -25,7 +25,11 @@
|
|||
(defun coq/init-company-coq ()
|
||||
(use-package company-coq
|
||||
:defer t
|
||||
:init (add-hook 'coq-mode-hook #'company-coq-mode)
|
||||
:init
|
||||
(progn
|
||||
(add-hook 'coq-mode-hook #'company-coq-mode)
|
||||
(add-to-list 'spacemacs-jump-handlers-coq-mode
|
||||
'company-coq-jump-to-definition))
|
||||
:config
|
||||
(progn
|
||||
(spacemacs/declare-prefix-for-mode
|
||||
|
@ -34,8 +38,7 @@
|
|||
(spacemacs/set-leader-keys-for-major-mode 'coq-mode
|
||||
"il" 'company-coq-lemma-from-goal
|
||||
"im" 'company-coq-insert-match-construct
|
||||
"ao" 'company-coq-occur
|
||||
"gd" 'company-coq-jump-to-definition))))
|
||||
"ao" 'company-coq-occur))))
|
||||
|
||||
(defun coq/init-proof-general ()
|
||||
(use-package proof-site
|
||||
|
@ -78,29 +81,29 @@
|
|||
"[" 'proof-undo-last-successful-command
|
||||
"." 'proof-goto-point
|
||||
;; Layout
|
||||
"ll" 'proof-layout-windows
|
||||
"lc" 'pg-response-clear-displays
|
||||
"ll" 'proof-layout-windows
|
||||
"lp" 'proof-prf
|
||||
;; Prover Interaction
|
||||
"px" 'proof-shell-exit
|
||||
"pc" 'proof-interrupt-process
|
||||
"pi" 'proof-interrupt-process
|
||||
"pp" 'proof-process-buffer
|
||||
"pq" 'proof-shell-exit
|
||||
"pr" 'proof-retract-buffer
|
||||
"pb" 'proof-process-buffer
|
||||
;; Prover queries ('ask prover')
|
||||
"af" 'proof-find-theorems
|
||||
"ap" 'coq-Print
|
||||
"ac" 'coq-Check
|
||||
"aa" 'coq-Print
|
||||
"aA" 'coq-Print-with-all
|
||||
"ab" 'coq-About
|
||||
"aip" 'coq-Print-with-implicits
|
||||
"aic" 'coq-Check-show-implicits
|
||||
"aB" 'coq-About-with-all
|
||||
"ac" 'coq-Check
|
||||
"aC" 'coq-Check-show-all
|
||||
"af" 'proof-find-theorems
|
||||
"aib" 'coq-About-with-implicits
|
||||
"anp" 'coq-Print-with-all
|
||||
"anc" 'coq-Check-show-all
|
||||
"anb" 'coq-About-with-all
|
||||
"aic" 'coq-Check-show-implicits
|
||||
"aii" 'coq-Print-with-implicits
|
||||
;; Moving the point (goto)
|
||||
"g." 'proof-goto-end-of-locked
|
||||
"ga" 'proof-goto-command-start
|
||||
"ge" 'proof-goto-command-end
|
||||
"gl" 'proof-goto-end-of-locked
|
||||
"gs" 'proof-goto-command-start
|
||||
;; Insertions
|
||||
"ie" 'coq-end-Section))))
|
||||
|
||||
|
|
Loading…
Reference in New Issue