Spacemacs config for Proof General

Setup.md

Tutorial

This is a Spacemacs config, I only use it for Coq + Proof General.

Instalation

• Make sure you have Emacs & Coq installed
• Install Proof General

cd ~/.emacs.d/private/local
git clone [email protected]:ProofGeneral/PG.git ProofGeneral
cd ProofGeneral
make

• Install Spacemacs layer

cd ~/.emacs.d/private
git clone [email protected]:mbrcknl/spacemacs-coq coq

• Change ~/.spacemacs and add Coq to it's layers.

(.....)
   dotspacemacs-configuration-layers
   '(
     ;; ----------------------------------------------------------------
     ;; Example of useful layers you may want to use right away.
     ;; Uncomment some layer names and press <SPC f e R> (Vim style) or
     ;; <M-m f e R> (Emacs style) to install them.
     ;; ----------------------------------------------------------------
     helm
     ;; auto-completion
     ;; better-defaults
     emacs-lisp
     ;; git
     ;; markdown
     ;; org
     ;; (shell :variables
     ;;        shell-default-height 30
     ;;        shell-default-position 'bottom)
     ;; spell-checking
     ;; syntax-checking
     ;; version-control
     coq
     )
(.....)

If you're having trouble with autocomplete

Add this to yout .spacemacs config

 (setq coq-mode-abbrev-table '())

Thanks for this guide, but I got the following error after these steps:

I do executed cd ProofGeneral && make and it succeed (with a few warnnings).
Is there any suggestion?

I have solved this problem referencing this post.

The key point is set the pg path yourself:

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

I have solved this problem referencing this post.

The key point is set the pg path yourself:

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

Thanks! It's been a while since I've used Coq, so I'll try to set it up again and see what's goes wrong with the new version of PG.