Yannick Zakowski (Sep 26 2021 at 16:36): Yannick Zakowski (Sep 26 2021 at 16:36):Hey everyone,
After some infidelities in the vscoq realm, I've been trying to setup a new fresh spacemacs installation. However the trivial use of the coq layer seems to silently fail to install company-coq, I only get PG, and I fail to understand why. Would anyone have any idea by any chance?
I'm on Mac, emacs 27.2, Spacemacs's develop branch.
Pierre Courtieu (Oct 18 2021 at 06:59):Hi! I suggest you ask this on the brand new proofgeneral-users stream. cc @Clément Pit-Claudel anyway.
Notification Bot (Oct 18 2021 at 13:53):This topic was moved here from #User interfaces devs & users > Spacemacs's coq layer not installing company-coq? by Théo Zimmermann
Clément Pit-Claudel (Oct 20 2021 at 04:54):Sorry, i missed that message … and I have no idea what magic spacemacs does that would break things. Can you install the package manually? (And did you figure things out since the OP?)
Yannick Zakowski (Dec 03 2021 at 02:08):Oh my turn to have missed your message, sorry about that. I actually did not manage to solve the issue, albeit I did not try very hard. I just gave a new clean shot Today restarting from scratch: by just adding the coq layer from master, I get a clean install of PG out of the box, but company-coq does not get installed, and the associated bindings of course to not get bound.
Looking at the layer (here : https://github.com/syl20bnr/spacemacs/blob/develop/layers/%2Blang/coq/packages.el ) it is as if the coq/init-company-coq is never run, but I do not know enough emacs or spacemacs for that matter to understand why that it is the case.
I should probably simply add company-coq to the list of packages to install out of the wrapping of any layer, but I feel like I must be missing something obvious -- and plus that would mean defining the extra bindings locally, which is not a big deal, but my lack of comprehension of the whole thing frustrates me :)
Yannick Zakowski (Dec 03 2021 at 17:06):Ok it is resolved: one simply needs to have the auto-completion layer on, then everything works.
I do not quite understand if there was an easy way to infer this on my own.
Notification Bot (Dec 03 2021 at 17:06):Yannick Zakowski has marked this topic as resolved.
Clément Pit-Claudel (Dec 04 2021 at 21:46):I do not quite understand if there was an easy way to infer this on my own.
Neither do I, unfortunately... Spacemacs can be opaque. Glad you solved it :)
Last updated: Oct 13 2024 at 01:02 UTC