Add coq layer

layers/+lang/coq/README.org

@@ -0,0 +1,105 @@
+#+TITLE: Coq layer
+
+[[file:img/coq.png]]
+
+* Table of Contents                                        :TOC_4_gh:noexport:
+ - [[#description][Description]]
+ - [[#install][Install]]
+   - [[#layer][Layer]]
+   - [[#coq][Coq]]
+   - [[#proof-general][Proof General]]
+ - [[#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]]
+
+* 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.
+
+** Proof General
+[[https://github.com/ProofGeneral/PG][Proof General]] provides a powerful, generic environment for using interactive
+proof assistants.
+
+To install, run the following commands:
+
+#+BEGIN_SRC sh
+git clone https://github.com/ProofGeneral/PG ~/.emacs.d/private/PG
+cd ~/.emacs.d/private/PG
+make
+#+END_SRC
+
+*Note*: This layer assumes you have installed Proof General to
+=~/.emacs.d/private/=.
+
+* 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.

layers/+lang/coq/packages.el

@@ -0,0 +1,113 @@
+;;; 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
+      '(
+        (proof-general :location local)
+        (company-coq :toggle (configuration-layer/package-usedp 'company))
+        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
+    :load-path "~/.emacs.d/private/PG/generic"
+    :config
+    (progn
+      (spacemacs|diminish outline-minor-mode)
+      (spacemacs|diminish holes-mode)
+      (spacemacs|diminish hs-minor-mode)
+
+      (setq proof-splash-seen t)
+
+      (setq proof-three-window-mode-policy 'hybrid)
+
+      ;; I don't know who wants to evaluate comments
+      ;; one-by-one, but I don't.
+      (setq proof-script-fly-past-comments 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