Proof General under spacemacs

extensions.el

(defvar coq-pre-extensions
  '(
    proof-general
    ))

(defun coq/init-proof-general ()
  "Initialize Proof General"
  (use-package proof-site
    :defer t
    :mode ("\\.v\\'" . coq-mode)
    :load-path
    "~/.nix-profile/share/emacs/site-lisp/ProofGeneral/generic"))

packages.el

(defvar coq-packages
  '(
    company-coq
    ))

(defun coq/init-company-coq ()
  (use-package company-coq
    :defer t
    :config
    (add-hook 'coq-mode-hook #'company-coq-initialize)))

Could you please be more specific to which files to add these lines? There are many of the two in various subdirectories.

I've put that layer in a basic repo. Install with

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

You may have to modify the location of proof-general, though.

Of course when I go looking for coq/spacemacs integration it turns out to be a fellow Nix user... 👍

I can't figure out how this works. I cloned as above and modified it to point to the correct proof general location, but opening Test.v treats it as a Verilog file. Can you help?