blob: ed3619d7d7c72ed7ab2578643488d4c1971f10db (
plain)
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
|
;; Time-stamp: <2019-09-11 13:59:30 (tslil@basingstoke)>
;; -----------------------------------------------------------------------------
;; Coq
;; (defvar pg-inserted-newline nil)
;; (defconst pg-whitespace-match "[ \\t]")
;; (defconst pg-subgoal-match "[*+\\-]")
;; (defun pg-move-point-dwim ()
;; (interactive)
;; ;; Did we move to a blank new line?
;; (when (= (point) (point-at-bol))
;; ;; If there's nothing here, lets add another line below
;; (when (looking-at-p (concat pg-whitespace-match "*$"))
;; (save-excursion (newline))
;; (setq pg-inserted-newline t))
;; ;; Now let's work out where the point should go
;; (previous-line)
;; (beginning-of-line)
;; ;; Is the previous line essentially a subgoal marker?
;; (if (looking-at-p (concat pg-whitespace-match "*"
;; pg-subgoal-match "+"
;; pg-whitespace-match "*$"))
;; ;; If so, trim the line and put the point in after the subgoal marker
;; (progn
;; (delete-trailing-whitespace (point-at-bol) (point-at-eol))
;; (end-of-line)
;; (insert-char ? ))
;; ;; If not, go back to where we were and indent
;; (next-line)
;; (indent-for-tab-command))))
(defconst coq-env '(("UniMath"
:topdir "~/theorems/coq/UniMath/"
:binary "sub/coq/bin/coqtop"
:args ("-coqlib" "/home/tslil/theorems/coq/UniMath/sub/coq/"
"-emacs" "-noinit"
"-indices-matter"
"-type-in-type" "-w" "-notation-overridden"
"-Q" "/home/tslil/theorems/coq/UniMath/UniMath" "UniMath"
"-Q" "/home/tslil/academic/proof_relevant_cats/formalisation" "wCats"))
("HoTT"
:topdir "~/theorems/coq/HoTT/"
:binary "hoqtop"
:args nil)))
(defvar use-coq-env "UniMath")
(use-package proof-general
:ensure t
:defer t
:functions coq-local-environment
:init (setq proof-splash-enable nil
proof-follow-mode 'followdown)
;; It's really annoying to have the code truncated due to equal
;; division ratios of the windows. The 5 is to accomodate line
;; numbers and the like
(defadvice proof-layout-windows (after resize-window-properly activate)
(let ((ww (window-width)))
(when (< ww (+ 5 fill-column))
(enlarge-window-horizontally (- (+ 5 fill-column) ww)))))
(defun coq-local-environment ()
(bind-key "C-s" #'isearch-forward proof-mode-map)
(let* ((data (alist-get use-coq-env coq-env nil nil #'string-equal))
(topdir (expand-file-name (plist-get data :topdir)))
(binary (plist-get data :binary))
(args (plist-get data :args)))
;; TAGS
(visit-tags-table (concat topdir "TAGS"))
;; Formatting
(setq fill-column 70)
(set-fringe-mode 0)
(make-local-variable 'before-save-hook)
(add-hook 'before-save-hook 'delete-trailing-whitespace)
(setq proof-three-window-mode-policy 'hybrid
proof-layout-windows-on-visit-file t
proof-shrink-windows-tofit t
proof-script-fly-past-comments t)
;; Tweak syntax table
;; (modify-syntax-entry ?' "w")
;; Coq binary related
(dolist (var '(coq-use-project-file coq-prog-args coq-prog-name))
(make-local-variable var))
(setq coq-use-project-file nil
coq-prog-args args
coq-prog-name (concat topdir binary))
(agda-input-setup)
(activate-input-method "Agda")))
:mode ("\\.v$" . coq-mode)
:hook (coq-mode . (lambda ()
(programming-setup)
(coq-local-environment)
(auto-fill-mode)
(company-coq-mode))))
(use-package company-coq
:after proof-general
:ensure t
:bind (:map company-coq-map
("M-." . xref-find-references)
("M-*" . pop-tag-mark))
:init
(setq company-coq-disabled-features '(hello)))
;; -----------------------------------------------------------------------------
;; Agda
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
(add-hook 'agda2-mode
(lambda ()
(subword-mode 1)
(auto-fill-mode)
(aggressive-indent-mode -1)))
;; -----------------------------------------------------------------------------
;; Lean
;; (use-package lean-mode
;; :ensure t
;; :defer t
;; :mode ("\\.lean$" . lean-mode))
|
