-
Notifications
You must be signed in to change notification settings - Fork 4.9k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
3 changed files
with
224 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,106 @@ | ||
#+TITLE: Coq layer | ||
|
||
[[file:img/coq.png]] | ||
|
||
* Table of Contents :TOC_4_gh:noexport: | ||
- [[#description][Description]] | ||
- [[#install][Install]] | ||
- [[#layer][Layer]] | ||
- [[#coq][Coq]] | ||
- [[#key-bindings][Key bindings]] | ||
- [[#laying-out-windows][Laying out windows]] | ||
- [[#managing-prover-process][Managing prover process]] | ||
- [[#prover-queries][Prover queries]] | ||
- [[#moving-the-point][Moving the point]] | ||
- [[#inserting][Inserting]] | ||
- [[#faq][FAQ]] | ||
- [[#there-are-empty-square-boxes-in-place-of-math-operators][There are empty square boxes in place of math operators]] | ||
|
||
* Description | ||
This layer adds support for the [[https://coq.inria.fr/][Coq]] proof assistant (adapted from | ||
[[https://github.com/tchajed/spacemacs-coq]]). | ||
|
||
* Install | ||
** Layer | ||
To use this configuration layer, add it to your =~/.spacemacs=. You will need to | ||
add =coq= to the existing =dotspacemacs-configuration-layers= list in this file. | ||
|
||
** Coq | ||
Official installers for MacOS and Windows are available from: | ||
[[https://coq.inria.fr/download]]. | ||
|
||
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 | | ||
|
||
** 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 | | ||
|
||
** 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) | | ||
|
||
** 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 | | ||
|
||
** 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 | | ||
|
||
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 | ||
available =company-coq= keybindings can be accessed at any time using =SPC SPC | ||
company-coq-tutorial=. | ||
|
||
* FAQ | ||
** 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 | ||
font, or disable the feature by adding the following snippet to the your | ||
=dotspacemacs/user-config=. | ||
|
||
#+BEGIN_SRC emacs-lisp | ||
(with-eval-after-load 'company-coq | ||
(add-to-list 'company-coq-disabled-features 'prettify-symbols)) | ||
#+END_SRC |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,118 @@ | ||
;;; packages.el --- coq layer packages file for Spacemacs. | ||
;; | ||
;; Copyright (c) 2012-2016 Sylvain Benner & Contributors | ||
;; | ||
;; Author: Jeremy Bi <bixuanxbi@gmail.com> | ||
;; URL: https://github.com/syl20bnr/spacemacs | ||
;; | ||
;; This file is not part of GNU Emacs. | ||
;; | ||
;;; License: GPLv3 | ||
|
||
;;; Code: | ||
|
||
(setq coq-packages | ||
'( | ||
(company-coq :toggle (configuration-layer/package-usedp 'company)) | ||
(proof-general :location (recipe | ||
:fetcher github | ||
:repo "ProofGeneral/PG" | ||
:files ("*"))) | ||
smartparens | ||
vi-tilde-fringe | ||
)) | ||
|
||
(defun coq/init-company-coq () | ||
(use-package company-coq | ||
:defer t | ||
:init (add-hook 'coq-mode-hook #'company-coq-mode) | ||
:config | ||
(progn | ||
(spacemacs/declare-prefix-for-mode | ||
'coq-mode | ||
"mi" "coq/insert") | ||
(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)))) | ||
|
||
(defun coq/init-proof-general () | ||
(use-package proof-site | ||
:mode ("\\.v\\'" . coq-mode) | ||
:defer t | ||
:init | ||
(progn | ||
(setq coq/proof-general-load-path (concat (spacemacs//get-package-directory 'proof-general) "generic")) | ||
(add-to-list 'load-path coq/proof-general-load-path)) | ||
:config | ||
(progn | ||
(spacemacs|diminish company-coq-mode) | ||
(spacemacs|diminish holes-mode) | ||
(spacemacs|diminish hs-minor-mode) | ||
(spacemacs|diminish outline-minor-mode) | ||
(spacemacs|diminish proof-active-buffer-fake-minor-mode) | ||
(spacemacs|diminish yas-minor-mode " ⓨ" " y") | ||
|
||
(setq company-coq-disabled-features '(hello) | ||
proof-three-window-mode-policy 'hybrid | ||
proof-script-fly-past-comments t | ||
proof-splash-seen t) | ||
|
||
(dolist (prefix '(("ml" . "pg/layout") | ||
("mp" . "pg/prover") | ||
("ma" . "pg/ask-prover") | ||
("mai" . "show-implicits") | ||
("man" . "show-all") ; n is for notation | ||
("mg" . "pg/goto"))) | ||
(spacemacs/declare-prefix-for-mode | ||
'coq-mode | ||
(car prefix) (cdr prefix))) | ||
|
||
;; key bindings | ||
(spacemacs/set-leader-keys-for-major-mode 'coq-mode | ||
;; Basic proof management | ||
"]" 'proof-assert-next-command-interactive | ||
"[" 'proof-undo-last-successful-command | ||
"." 'proof-goto-point | ||
;; Layout | ||
"ll" 'proof-layout-windows | ||
"lc" 'pg-response-clear-displays | ||
"lp" 'proof-prf | ||
;; Prover Interaction | ||
"px" 'proof-shell-exit | ||
"pc" 'proof-interrupt-process | ||
"pr" 'proof-retract-buffer | ||
"pb" 'proof-process-buffer | ||
;; Prover queries ('ask prover') | ||
"af" 'proof-find-theorems | ||
"ap" 'coq-Print | ||
"ac" 'coq-Check | ||
"ab" 'coq-About | ||
"aip" 'coq-Print-with-implicits | ||
"aic" 'coq-Check-show-implicits | ||
"aib" 'coq-About-with-implicits | ||
"anp" 'coq-Print-with-all | ||
"anc" 'coq-Check-show-all | ||
"anb" 'coq-About-with-all | ||
;; Moving the point (goto) | ||
"g." 'proof-goto-end-of-locked | ||
"ga" 'proof-goto-command-start | ||
"ge" 'proof-goto-command-end | ||
;; Insertions | ||
"ie" 'coq-end-Section)))) | ||
|
||
(defun coq/post-init-smartparens () | ||
(spacemacs/add-to-hooks | ||
(if dotspacemacs-smartparens-strict-mode | ||
'smartparens-strict-mode | ||
'smartparens-mode) | ||
'(coq-mode-hook))) | ||
|
||
(defun coq/post-init-vi-tilde-fringe () | ||
(spacemacs/add-to-hooks 'spacemacs/disable-vi-tilde-fringe | ||
'(coq-response-mode-hook | ||
coq-goals-mode-hook))) | ||
|
||
|
||
;;; packages.el ends here |