[emacs] fix theoreom proving stuff for 21st c.

1 files changed, 66 insertions, 76 deletions

diff --git a/emacs/inits/25-theorems.el b/emacs/inits/25-theorems.el
index b87b0ed..490758a 100644
--- a/emacs/inits/25-theorems.el
+++ b/emacs/inits/25-theorems.el
@@ -1,4 +1,4 @@
-;; Time-stamp: <2021-09-29 21h40 EDT (bison)>
+;; Time-stamp: <2024-02-19 14h02 CET (29b31490)>
 
 ;; -----------------------------------------------------------------------------
 ;; Coq
@@ -32,18 +32,16 @@
 ;;       (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"
+                     :topdir "~/theorems/UniMath/"
+                     :binary "/usr/bin/coqtop"
+                     :args ("-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" "PRCats"))
+                            "-Q" "/home/tslil/theorems/UniMath/UniMath" "UniMath"
+                            "-Q" "/home/tslil/typeset/proof_relevant_cats/formalisation" "PRCats"))
                     ("HoTT"
-                     :topdir "~/theorems/coq/HoTT/"
-                     :binary "hoqtop"
-                     :args nil)))
+                     :topdir "~/theorems/Coq-HoTT/"
+                     :binary "/usr/bin/coqtop"
+                     :args ("-noinit" "-indices-matter"))))
 
 (defvar use-coq-env "UniMath")
 
@@ -68,6 +66,50 @@
       (re-search-forward "(\\|{")
       (backward-char 1))))
 
+(defun coq-local-environment ()
+  (require 'corral)
+  (bind-keys :map coq-mode-map
+             ("M-i" . mike-implicify)
+             ("M-a" . forward-sexp)
+             ("M-e" . backward-sexp)
+             ("M-/" . lh-matching-delim)
+             ("M-(" . corral-parentheses-forward)
+             ("M-)" . corral-parentheses-backward)
+             ("M-{" . corral-braces-forward)
+             ("M-}" . corral-braces-backward)
+             ("M-[" . corral-brackets-forward)
+             ("M-]" . corral-brackets-backward)
+             ("C-(" . lh-slurp-forward)
+             ("C-)" . lh-slurp-backward)
+             ("C-s" . isearch-forward))
+  (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)))
+    (dolist (var '(coq-use-project-file coq-prog-args coq-prog-name))
+      (make-local-variable var))
+    (setq coq-use-project-file t
+          coq-prog-args args
+          coq-prog-name binary)
+    ;; TAGS
+    (visit-tags-table (concat topdir "TAGS")))
+  ;; Formatting
+  (setq fill-column 70)
+  (visual-line-mode 1)
+  (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")
+  ;; Use agda input method
+  ;; (agda-input-setup)
+  ;; (activate-input-method "Agda")
+  )
+
 (use-package proof-general
   :ensure t
   :defer t
@@ -79,82 +121,30 @@
   ;; numbers and the like
   (defadvice proof-layout-windows (after resize-window-properly activate)
     (let ((ww (window-width)))
-      (when (< ww (+ 7 fill-column))
-        (enlarge-window-horizontally (- (+ 7 fill-column) ww)))))
-  (defun coq-local-environment ()
-    (require 'corral)
-    (bind-keys :map coq-mode-map
-               ("M-i" . mike-implicify)
-               ("M-a" . forward-sexp)
-               ("M-e" . backward-sexp)
-               ("M-/" . lh-matching-delim)
-               ("M-(" . corral-parentheses-forward)
-               ("M-)" . corral-parentheses-backward)
-               ("M-{" . corral-braces-forward)
-               ("M-}" . corral-braces-backward)
-               ("M-[" . corral-brackets-forward)
-               ("M-]" . corral-brackets-backward)
-               ("C-(" . lh-slurp-forward)
-               ("C-)" . lh-slurp-backward)
-               ("C-s" . isearch-forward))
-    (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)
-      (visual-line-mode 1)
-      (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")))
+      (when (< ww (+ 5 fill-column))
+        (enlarge-window-horizontally (- (+ 5 fill-column) ww)))))
   :mode ("\\.v$" . coq-mode)
   :hook (coq-mode . (lambda ()
                       (programming-setup)
                       (coq-local-environment)
-		      ;; (company-coq-mode)
                       (auto-fill-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")))
+(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)))
+(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))
+(use-package lean-mode
+  :ensure t
+  :defer t
+  :mode ("\\.lean$" . lean-mode))