forked from olivierverdier/spacemacs-coq
-
Notifications
You must be signed in to change notification settings - Fork 6
/
packages.el
133 lines (125 loc) · 4.47 KB
/
packages.el
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
;;; packages.el --- coq Layer packages File for Spacemacs
;;
;; Copyright (c) 2016 Tej Chajed
;;
;; Based on original version by Olivier Verdier
;;
;; Author: Tej Chajed <tchajed@mit.edu>
;; URL: https://github.com/tchajed/spacemacs-coq
;;
;; This file is not part of GNU Emacs.
;;
;;; License: GPLv3
(setq coq-packages
'(
company-coq
(proof-general :location (recipe
:fetcher github
:repo "ProofGeneral/PG"
:files ("*")))
))
(setq coq-excluded-packages '())
(defun setup-coq-keys-for-map (state)
(evil-define-key state coq-mode-map
(kbd "<f3>") #'proof-assert-next-command-interactive)
(evil-define-key state coq-mode-map
(kbd "<f4>") #'company-coq-proof-goto-point)
(evil-define-key state coq-mode-map
(kbd "<f2>") #'proof-undo-last-successful-command))
(defun setup-coq-keys ()
(setup-coq-keys-for-map 'normal)
(setup-coq-keys-for-map 'insert))
(defun hide-mode-statuses ()
(diminish 'company-mode)
(diminish 'hs-minor-mode)
(diminish 'outline-minor-mode)
(diminish 'company-mode)
(diminish 'holes-mode))
(defun coq/init-company-coq ()
(use-package company-coq
:defer t
:init
(add-hook 'coq-mode-hook #'company-coq-mode)
(add-hook 'coq-mode-hook #'setup-coq-keys)
(add-hook 'coq-mode-hook #'hide-mode-statuses)
(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)))
(defun coq/init-proof-general ()
"Initialize Proof General."
;; Setup from Proof General README, using a Homebrew path. Proof General
;; lazily loads from proof-site, so there's no need to use-package it.
;; (load "/usr/local/share/emacs/site-lisp/proof-general/generic/proof-site")
(use-package proof-site
:mode ("\\.v\\'" . coq-mode)
:defer t
:init
(progn
(setq coq/proof-general-load-path
(concat (configuration-layer/get-elpa-package-install-directory
'proof-general) "generic")
proof-three-window-mode-policy 'hybrid
proof-script-fly-past-comments t
proof-splash-seen t)
(add-to-list 'load-path coq/proof-general-load-path))
(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)))
(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)
;; Workaround for evil performance bug (see
;; https://github.com/olivierverdier/spacemacs-coq/issues/6 for details).
;; Essentially the cursor color is changed rapidly when navigating the proof
;; in insert mode. This ensures the insert and normal mode colors are the
;; same, which generally avoids this problem.
(add-hook 'coq-mode-hook
(lambda ()
(setq-local
evil-insert-state-cursor
(cons
(car evil-normal-state-cursor)
(cdr evil-insert-state-cursor)))))
(add-hook 'coq-mode-hook
(lambda ()
(purpose-add-user-purposes
:modes
'((proof-response-mode . response)
(proof-goals-mode . goals)))))))