Coq Emacs (Spacemacs) 开发环境准备指南

coq-spacemacs-install.md

Coq Emacs (Spacemacs) Develop Environment Prepare Guide

main reference:

https://gist.github.com/mtrsk/10a03927490f9edb1f7a2cd72792b0ec

The Dependencies Graph

Spacemacs Coq Layer (a configuration of spacemacs)
   Spacemacs (a configuration of emacs)
      Emacs
   Proof General
      Coq

Steps

Ubuntu for example:

Install latest Emacs

http://ubuntuhandbook.org/index.php/2019/04/gnu-emacs-26-2-released-install-in-ubuntu-18-04/

sudo add-apt-repository ppa:kelleyk/emacs
sudo apt update
sudo apt install emacs26
emacs --version

Install latest Spacemacs

http://spacemacs.org/#

git clone git@github.com:syl20bnr/spacemacs.git ~/.emacs.d

Install Coq

sudo apt install coq
coqtop --version

Install Proof General

Via package manager apt (the package proofgeneral contains emacs25 will is not necessary)

sudo apt search proofgeneral
sudo apt install proofgeneral
cd /usr/share/emacs/site-lisp/proofgeneral

Or manually clone and build (suggested)

cd ~/.emacs.d/private/local
git clone git@github.com:ProofGeneral/PG.git ProofGeneral
cd ProofGeneral
make

Install Spacemacs Coq layer

cd ~/.emacs.d/private
git clone git@github.com:olivierverdier/spacemacs-coq.git ~/.emacs.d/private/coq

Configure your ~/.spacemacs

add coq to layers

(.....)
   dotspacemacs-configuration-layers
   '(
     ;; ----------------------------------------------------------------
     ;; Example of useful layers you may want to use right away.
     ;; ----------------------------------------------------------------
     helm
     ;; auto-completion
     ;; better-defaults
     emacs-lisp
     ;; git
     ;; markdown
     ;; org
     coq
     )
(.....)

You probably need to specify the ProofGeneral path yourself:

(defun dotspacemacs/user-init ()
  (setq proof-general-path "/your/local/git/ProofGeneral/generic/proof-site"))

Set a shortcut (key mapping):

(defun dotspacemacs/user-config ()
  (define-key evil-motion-state-map (kbd "C-j") 'proof-assert-next-command-interactive)
  (define-key evil-motion-state-map (kbd "C-k") 'proof-undo-last-successful-command-1)
  (define-key evil-normal-state-map ";" 'proof-assert-next-command-interactive)
  (define-key evil-normal-state-map "'" 'proof-undo-last-successful-command-1)
  )