1 files changed, 124 insertions, 0 deletions
diff --git a/emacs/inits/25-theorems.el b/emacs/inits/25-theorems.el
new file mode 100644
index 0000000..ed3619d
--- /dev/null
+++ b/emacs/inits/25-theorems.el
@@ -0,0 +1,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))