TakeV/spacemacs
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
This repository has been archived on 2024-10-22. You can view files and clone it, but cannot push or open issues or pull requests.
spacemacs/layers/+lang/coq/packages.el

121 lines
4 KiB
EmacsLisp
Raw Normal View History

Add coq layer
2016-08-25 04:38:03 +00:00
;;; packages.el --- coq layer packages file for Spacemacs.
;;
bump year in the copyright headers Folks, this time of year has come. We can bump year in the copyright headers. Let's celebrate!
2018-10-13 17:44:50 +00:00
;; Copyright (c) 2012-2018 Sylvain Benner & Contributors
Add coq layer
2016-08-25 04:38:03 +00:00
;;
;; 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
'(
Rename :depends to :requires
2017-07-03 07:52:54 +00:00
(company-coq :requires company)
proof-general is added in MELPA
2018-09-02 03:19:09 +00:00
proof-general
Add coq layer
2016-08-25 04:38:03 +00:00
smartparens
vi-tilde-fringe
))
(defun coq/init-company-coq ()
(use-package company-coq
Revert "Defer packages by default using use-package-always-defer" This reverts commit 29c78ce841ee5a99bb4077a2862afc96c8136107 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.
2018-03-04 04:37:53 +00:00
:defer t
coq: update key bindings and README README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
2017-02-13 03:08:36 +00:00
:init
(progn
(add-hook 'coq-mode-hook #'company-coq-mode)
(add-to-list 'spacemacs-jump-handlers-coq-mode
coq: fix some configuration - delete some diminish expressions which are not related to PG and user spacemacs|hide-lighter instead of spacemacs|diminish - move company related configuration to the correct place - move setq expressions to :init blocks to allow users to easily change them
2017-02-13 04:45:56 +00:00
'company-coq-jump-to-definition)
(setq company-coq-disabled-features '(hello)))
Add coq layer
2016-08-25 04:38:03 +00:00
:config
(progn
coq: fix some configuration - delete some diminish expressions which are not related to PG and user spacemacs|hide-lighter instead of spacemacs|diminish - move company related configuration to the correct place - move setq expressions to :init blocks to allow users to easily change them
2017-02-13 04:45:56 +00:00
(spacemacs|hide-lighter company-coq-mode)
coq: add keybindings for company-coq's documentation functions
2018-08-09 18:06:46 +00:00
(dolist (prefix '(("mi" . "coq/insert")
("mh" . "coq/document")))
(spacemacs/declare-prefix-for-mode
'coq-mode
(car prefix) (cdr prefix)))
Add coq layer
2016-08-25 04:38:03 +00:00
(spacemacs/set-leader-keys-for-major-mode 'coq-mode
"il" 'company-coq-lemma-from-goal
"im" 'company-coq-insert-match-construct
coq: add keybindings for company-coq's documentation functions
2018-08-09 18:06:46 +00:00
"ao" 'company-coq-occur
"he" 'company-coq-document-error
"hE" 'company-coq-browse-error-messages
"hh" 'company-coq-doc))))
Add coq layer
2016-08-25 04:38:03 +00:00
(defun coq/init-proof-general ()
(use-package proof-site
:mode ("\\.v\\'" . coq-mode)
Revert "Defer packages by default using use-package-always-defer" This reverts commit 29c78ce841ee5a99bb4077a2862afc96c8136107 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.
2018-03-04 04:37:53 +00:00
:defer t
Add coq layer
2016-08-25 04:38:03 +00:00
:init
(progn
(setq coq/proof-general-load-path
(concat (configuration-layer/get-elpa-package-install-directory
coq: fix some configuration - delete some diminish expressions which are not related to PG and user spacemacs|hide-lighter instead of spacemacs|diminish - move company related configuration to the correct place - move setq expressions to :init blocks to allow users to easily change them
2017-02-13 04:45:56 +00:00
'proof-general) "generic")
Add coq layer
2016-08-25 04:38:03 +00:00
proof-three-window-mode-policy 'hybrid
proof-script-fly-past-comments t
proof-splash-seen t)
coq: fix some configuration - delete some diminish expressions which are not related to PG and user spacemacs|hide-lighter instead of spacemacs|diminish - move company related configuration to the correct place - move setq expressions to :init blocks to allow users to easily change them
2017-02-13 04:45:56 +00:00
(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
Add coq layer
2016-08-25 04:38:03 +00:00
(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
coq: update key bindings and README README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
2017-02-13 03:08:36 +00:00
"ll" 'proof-layout-windows
Add coq layer
2016-08-25 04:38:03 +00:00
"lp" 'proof-prf
;; Prover Interaction
coq: update key bindings and README README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
2017-02-13 03:08:36 +00:00
"pi" 'proof-interrupt-process
"pp" 'proof-process-buffer
"pq" 'proof-shell-exit
Add coq layer
2016-08-25 04:38:03 +00:00
"pr" 'proof-retract-buffer
;; Prover queries ('ask prover')
coq: update key bindings and README README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
2017-02-13 03:08:36 +00:00
"aa" 'coq-Print
"aA" 'coq-Print-with-all
Add coq layer
2016-08-25 04:38:03 +00:00
"ab" 'coq-About
coq: update key bindings and README README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
2017-02-13 03:08:36 +00:00
"aB" 'coq-About-with-all
"ac" 'coq-Check
"aC" 'coq-Check-show-all
"af" 'proof-find-theorems
Add coq layer
2016-08-25 04:38:03 +00:00
"aib" 'coq-About-with-implicits
coq: update key bindings and README README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
2017-02-13 03:08:36 +00:00
"aic" 'coq-Check-show-implicits
"aii" 'coq-Print-with-implicits
Add coq layer
2016-08-25 04:38:03 +00:00
;; Moving the point (goto)
"ge" 'proof-goto-command-end
coq: update key bindings and README README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
2017-02-13 03:08:36 +00:00
"gl" 'proof-goto-end-of-locked
"gs" 'proof-goto-command-start
Add coq layer
2016-08-25 04:38:03 +00:00
;; Insertions
lang/coq: more insertion keybindings
2018-08-03 00:24:54 +00:00
"ic" 'coq-insert-command
"ie" 'coq-end-Section
"ii" 'coq-insert-intros
"ir" 'coq-insert-requires
"is" 'coq-insert-section-or-module
"it" 'coq-insert-tactic
Add a new binding for the Coq layer. This binding toggles the electric terminator setting of Proof General. Also describe the new binding in the README and add a note to the change log.
2020-02-11 20:46:39 +00:00
"iT" 'coq-insert-tactical
;; Options
"Te" 'proof-electric-terminator-toggle))))
Add coq layer
2016-08-25 04:38:03 +00:00
Revert "Defer packages by default using use-package-always-defer" This reverts commit 29c78ce841ee5a99bb4077a2862afc96c8136107 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.
2018-03-04 04:37:53 +00:00
(defun coq/post-init-smartparens ()
(spacemacs/add-to-hooks (if dotspacemacs-smartparens-strict-mode
'smartparens-strict-mode
'smartparens-mode)
'(coq-mode-hook)))
Add coq layer
2016-08-25 04:38:03 +00:00
(defun coq/post-init-vi-tilde-fringe ()
(spacemacs/add-to-hooks 'spacemacs/disable-vi-tilde-fringe
'(coq-response-mode-hook
coq-goals-mode-hook)))
Reference in a new issue Copy permalink