Moving to Doom Emacs!

.emacs.d/modules/lang/coq/README.org

@@ -0,0 +1,6 @@
+#+TITLE: :lang coq
+
+This module adds [[https://coq.inria.fr][coq]] support, powered by [[https://proofgeneral.github.io][Proof General]].
+
++ Code completion ([[https://github.com/cpitclaudel/company-coq][company-coq]])
++ [[https://github.com/hlissner/doom-snippets/tree/master/coq-mode][Snippets]]

.emacs.d/modules/lang/coq/config.el

@@ -0,0 +1,96 @@
+;;; lang/coq/config.el -*- lexical-binding: t; -*-
+
+;;;###package proof-general
+;; HACK `proof-general' ascertains its own library path at compile time in its
+;; autoloads file using `byte-compile-current-file' (and stores it in
+;; `pg-init--script-full-path'). This means that when
+;; `doom-package-autoload-file' is created and byte-compiled,
+;; `pg-init--script-full-path' will be wrong, causing file-missing errors as it
+;; tries to load `proof-site'. We prevent this by defining these two variables
+;; early, in our own autoloads file.
+(setq pg-init--script-full-path (locate-library "proof-general")
+      pg-init--pg-root (file-name-directory pg-init--script-full-path)
+      proof-splash-enable nil)
+
+
+;;;###package coq
+;; Doom syncs other indent variables with `tab-width'; we trust major modes to
+;; set it -- which most of them do -- but coq-mode doesn't, so...
+(setq-hook! 'coq-mode-hook tab-width proof-indent)
+
+;; We've replaced coq-mode abbrevs with yasnippet snippets (in the snippets
+;; library included with Doom).
+(setq coq-mode-abbrev-table '())
+
+(map! :after coq-mode
+      :map coq-mode-map
+      :localleader
+      "]"  #'proof-assert-next-command-interactive
+      "["  #'proof-undo-last-successful-command
+      "."  #'proof-goto-point
+      (:prefix ("l" . "layout")
+        "c" #'pg-response-clear-displays
+        "l" #'proof-layout-windows
+        "p" #'proof-prf)
+      (:prefix ("p" . "proof")
+        "i" #'proof-interrupt-process
+        "p" #'proof-process-buffer
+        "q" #'proof-shell-exit
+        "r" #'proof-retract-buffer)
+      (:prefix ("a" . "about/print/check")
+        "a" #'coq-Print
+        "A" #'coq-Print-with-all
+        "b" #'coq-About
+        "B" #'coq-About-with-all
+        "c" #'coq-Check
+        "C" #'coq-Check-show-all
+        "f" #'proof-find-theorems
+        (:prefix ("i" . "implicits")
+          "b" #'coq-About-with-implicits
+          "c" #'coq-Check-show-implicits
+          "i" #'coq-Print-with-implicits))
+      (:prefix ("g" . "goto")
+        "e" #'proof-goto-command-end
+        "l" #'proof-goto-end-of-locked
+        "s" #'proof-goto-command-start)
+      (:prefix ("i" . "insert")
+        "c" #'coq-insert-command
+        "e" #'coq-end-Section
+        "i" #'coq-insert-intros
+        "r" #'coq-insert-requires
+        "s" #'coq-insert-section-or-module
+        "t" #'coq-insert-tactic
+        "T" #'coq-insert-tactical))
+
+
+;; This package provides more than just code completion, so we load it whether
+;; or not :completion company is enabled.
+(use-package! company-coq
+  :hook (coq-mode . company-coq-mode)
+  :config
+  (set-popup-rule! "^\\*\\(?:response\\|goals\\)\\*" :ignore t)
+  (set-lookup-handlers! 'company-coq-mode
+    :definition #'company-coq-jump-to-definition
+    :references #'company-coq-grep-symbol
+    :documentation #'company-coq-doc)
+
+  (setq company-coq-disabled-features '(hello company-defaults))
+
+  (if (featurep! :completion company)
+      (map! :map coq-mode-map [remap company-complete-common]
+            #'company-indent-or-complete-common)
+    ;; `company-coq''s company defaults impose idle-completion on folks, so
+    ;; we'll set up company ourselves.
+    ;; See https://github.com/cpitclaudel/company-coq/issues/42
+    (add-to-list 'company-coq-disabled-features 'company))
+
+  (map! :map coq-mode-map
+        :localleader
+        "ao" #'company-coq-occur
+        (:prefix "i"
+          "l" #'company-coq-lemma-from-goal
+          "m" #'company-coq-insert-match-construct)
+        (:prefix ("h" . "help")
+          "e" #'company-coq-document-error
+          "E" #'company-coq-browse-error-messages
+          "h" #'company-coq-doc)))

.emacs.d/modules/lang/coq/packages.el

@@ -0,0 +1,6 @@
+;; -*- no-byte-compile: t; -*-
+;;; lang/coq/packages.el
+
+(package! proof-general)
+
+(package! company-coq)