Stream: Coq users

Topic: Spacemacs and company-coq

view this post on Zulip Andrés Goens (Aug 11 2021 at 12:37):

Does anyone here who use spacemacs with the coq layer (spacemacs develop) also have had the issue that it does not load company-coq? For some reason, my spacemacs only installs and loads proofgeneral (and the very annoying smartparens), but company-coq won't get installed. I can manually install it from MELPA and it will then consider it orphaned and delete it the next time! Even though the coq-packages variable clearly has company-coq listed. I was hoping someone else has had this issue and can enlighten me as to what I'm doing wrong here :sweat_smile:

view this post on Zulip Paolo Giarrusso (Aug 13 2021 at 23:08):

Spacemacs lets you force installing/uninstalling packages overriding its computations...

view this post on Zulip Paolo Giarrusso (Aug 13 2021 at 23:11):

Can you try adding company-coq to dotspacemacs-additional-packages and make sure it's not in dotspacemacs-excluded-packages? This should work around your issue:

(defun dotspacemacs/layers ()
   dotspacemacs-additional-packages '(company-coq)

   dotspacemacs-excluded-packages '(foo bar ...)

view this post on Zulip Paolo Giarrusso (Aug 13 2021 at 23:12):

I haven't seen your problem, but I also haven't upgraded Spacemacs recently, since it's not running into critical bugs.

view this post on Zulip Andrés Goens (Aug 16 2021 at 08:15):

Thanks for the suggestion! I had already tried that (to no avail). The variable dotspacemacs-additional-packages is for adding packages that are not part of any layer, but company-coq is part of the coq layer, yet it won't get installed. I might ask around in the spacemacs community, just thought maybe someone here could have the issue as well, since it happens pretty straightforward for a new install (I could reproduce it with a fresh install).

Last updated: Feb 06 2023 at 12:04 UTC