Thomas Baruchel (Dec 12 2023 at 09:52): Thomas Baruchel (Dec 12 2023 at 09:52):Hi, I am really a newbie to Emacs, I hope my question will be understandable. I usually use Coq on Vim with the dedicated Coqtail plugin. But since I would like to explore other proof assistants (Isabelle, Agda, Lean, etc.), I would like to get some interface for it. As a Vim user, my first thought was to install Spacemacs rather than VScode.
I understand that I have to install "layers", and I could install (and test) the Coq layer.
But if I understand correctly, this is not Proof General, but rather some standalone Coq interface. Proof General seems to be something more general.
Now my questions are:
a) doest Proof General works on Spacemacs (it is not listed in the official list of Spacemacs layers);
b) should I uninstall Coq layer and install the Cos plugin for Proof General instead?
I tried to search for "Proof General" and Spacemacs but couldn't find much resources.
Yannick Zakowski (Dec 12 2023 at 10:49):No I think you were on the right path: Spacemacs «layers» are just a clever way to setup standard related packages. And the coq layer essentially simply install proof-general and company-coq, the two coq-related emacs packages. You can find the doc and detail here for instance (weirdly it doesn't seem to be listed on the main spacemacs page):
https://github.com/syl20bnr/spacemacs/tree/develop/layers/%2Blang/coq
And so in practice all you should have to do is to add coq to your list of layers in the dotspacemacs-configuration-layers of your .spacemacs file
Last updated: Oct 13 2024 at 01:02 UTC