Add coq layer

layers/+lang/coq/README.org

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

layers/+lang/coq/packages.el

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