ebe4c60264
This reverts commit 29c78ce841 and all other fixes
that have been made afterwards.
The motivation is that use-package is seen by many as a replacement for
`require`. Is use-package always defer the loading of packages then is breaks
this use case, this does not respect POLA so even if it was making Spacemacs
loading faster (up to 3s faster on some startup on my machine) we just cannot
use it, it would be irresponsible. Spacemacs should be easy to use, loading
performance will come with time but it is not a priority.
109 lines
3.6 KiB
EmacsLisp
109 lines
3.6 KiB
EmacsLisp
;;; packages.el --- coq layer packages file for Spacemacs.
|
|
;;
|
|
;; Copyright (c) 2012-2016 Sylvain Benner & Contributors
|
|
;;
|
|
;; Author: Jeremy Bi <bixuanxbi@gmail.com>
|
|
;; URL: https://github.com/syl20bnr/spacemacs
|
|
;;
|
|
;; This file is not part of GNU Emacs.
|
|
;;
|
|
;;; License: GPLv3
|
|
|
|
(setq coq-packages
|
|
'(
|
|
(company-coq :requires company)
|
|
(proof-general :location (recipe
|
|
:fetcher github
|
|
:repo "ProofGeneral/PG"
|
|
:files ("*")))
|
|
smartparens
|
|
vi-tilde-fringe
|
|
))
|
|
|
|
(defun coq/init-company-coq ()
|
|
(use-package company-coq
|
|
:defer t
|
|
:init
|
|
(progn
|
|
(add-hook 'coq-mode-hook #'company-coq-mode)
|
|
(add-to-list 'spacemacs-jump-handlers-coq-mode
|
|
'company-coq-jump-to-definition)
|
|
(setq company-coq-disabled-features '(hello)))
|
|
:config
|
|
(progn
|
|
(spacemacs|hide-lighter company-coq-mode)
|
|
(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
|
|
"ao" 'company-coq-occur))))
|
|
|
|
(defun coq/init-proof-general ()
|
|
(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))
|
|
:config
|
|
(progn
|
|
(spacemacs|hide-lighter holes-mode)
|
|
(spacemacs|hide-lighter proof-active-buffer-fake-minor-mode)
|
|
;; key bindings
|
|
(dolist (prefix '(("ml" . "pg/layout")
|
|
("mp" . "pg/prover")
|
|
("ma" . "pg/ask-prover")
|
|
("mai" . "show-implicits")
|
|
("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
|
|
"lc" 'pg-response-clear-displays
|
|
"ll" 'proof-layout-windows
|
|
"lp" 'proof-prf
|
|
;; Prover Interaction
|
|
"pi" 'proof-interrupt-process
|
|
"pp" 'proof-process-buffer
|
|
"pq" 'proof-shell-exit
|
|
"pr" 'proof-retract-buffer
|
|
;; Prover queries ('ask prover')
|
|
"aa" 'coq-Print
|
|
"aA" 'coq-Print-with-all
|
|
"ab" 'coq-About
|
|
"aB" 'coq-About-with-all
|
|
"ac" 'coq-Check
|
|
"aC" 'coq-Check-show-all
|
|
"af" 'proof-find-theorems
|
|
"aib" 'coq-About-with-implicits
|
|
"aic" 'coq-Check-show-implicits
|
|
"aii" 'coq-Print-with-implicits
|
|
;; Moving the point (goto)
|
|
"ge" 'proof-goto-command-end
|
|
"gl" 'proof-goto-end-of-locked
|
|
"gs" 'proof-goto-command-start
|
|
;; Insertions
|
|
"ie" 'coq-end-Section))))
|
|
|
|
(defun coq/post-init-smartparens ()
|
|
(spacemacs/add-to-hooks (if dotspacemacs-smartparens-strict-mode
|
|
'smartparens-strict-mode
|
|
'smartparens-mode)
|
|
'(coq-mode-hook)))
|
|
|
|
(defun coq/post-init-vi-tilde-fringe ()
|
|
(spacemacs/add-to-hooks 'spacemacs/disable-vi-tilde-fringe
|
|
'(coq-response-mode-hook
|
|
coq-goals-mode-hook)))
|