Add coq layer

[bixuanzju]

I've been using this layer for quite a time now, maybe it's time to share with everyone!

• Most of the keybindings are stolen from https://github.com/tchajed/spacemacs-coq.
• Proof General is an indispensable tool for programming in Coq, but it is not on MELPA, so I am not sure what is the appropriate way to instruct users to download and install it. For now, I assume it is installed under ~/.emacs.d/private(see the Install section in README).

Suggestions are welcome!

PS: calling @NJBS for help and test :)

Edit:

Thanks due to @vic, now we use quelpa to help fetch the source of proof-general and install.

[NJBS]

Thanks for this! ❤️

In regards to Proof General, since they are hosted on a git repository we are be able to use the MELPA github fetcher to grab their package. Additionally I believe compilation for Proof General only involves optionally byte compiling the elisp files, so the package should be usable even without running make.

Normally it would be trivial to fetch and compile an elisp package from github but unfortunately Proof General doesn't follow the MELPA package format yet so hacking around it would be running into the same problem as #2880 😟 . Luckily, there has been recent activity in trying to port the package into MELPA format melpa/melpa#3454.

The current workaround seems fine 😄, with my only suggestion being that a small note should be added stating that the make step is recommended but optional since Proof General has been known to fail to compile on Windows. [1] [2]

I love the use of the new Proof General mascot for the layer logo 😄 , could you possibly resize it so its height is below 200 pixels whilst maintaining the aspect ratio such that it conforms with spacemacs conventions?

Considering the amount of issues spacemacs gets related to incompatible fonts I've gone ahead and added an FAQ entry about disabling symbol prettification to the README. I've also disabled the welcoming message that company-coq gives you when opening a coq file and added a note to the docs about manually invoking the tutorial.

Lastly, I have diminished a few more useless modes that simply clutter the mode-line and updated a couple of small things in the layer so it's more inline with spacemacs conventions.

The patch can be found here.

Thanks again for submitting this! ❤️

[bixuanzju]

@NJBS Thanks very much for you detailed suggestions! I've merged your changes and resized the image :)

[bixuanzju]

@syl20bnr ping the boss

[tarsius]

Luckily, there has been recent activity in trying to port the package into MELPA format melpa/melpa#3454.

Looks like this isn't really progressing. @NJBS maybe you could lend them a hand?

[langston-barrett]

@syl20bnr @bixuanzju Is there anything stopping this PR?

[aroig]

I like this layer quite a lot, thanks! One problem I found is that interacts badly with the new purpose stuff. Both company-coq and proof-general like to handle their own windows, and that breaks.

When window-purpose is enabled (it is by default on develop), company-coq opens the documentation buffer in place of the coq buffer, not on the side. proof-general breaks even worse: when trying to validate a coq file step by step (SPC m ]). proof-general opens a couple of windows reporting on the current state of the proof. On my tests, that just closed my emacs frame ?!.

I don't know whether this can be solved by configuring window-purpose or the packages would need fixing. I have ended up disabling window-purpose anyway, since I found it annoying...

[aroig]

The following fixes the interaction with window-purpose, as suggested by @bmag in the discussion after this comment

diff --git a/layers/+lang/coq/packages.el b/layers/+lang/coq/packages.el
index 4aa1748..2c25e51 100644
--- a/layers/+lang/coq/packages.el
+++ b/layers/+lang/coq/packages.el
@@ -17,6 +17,7 @@
         (proof-general :location local)
         smartparens
         vi-tilde-fringe
+        window-purpose
         ))

 (defun coq/init-company-coq ()
@@ -108,5 +109,11 @@
                           '(coq-response-mode-hook
                             coq-goals-mode-hook)))

+(defun coq/post-init-window-purpose ()
+  (purpose-add-user-purposes :modes
+                             '((proof-response-mode . response)
+                               (proof-goals-mode . goals))
+                             :regexps
+                             '(("^\\*company-coq" . help))))

 ;;; packages.el ends here

[bixuanzju]

@aroig Thank you! I was curious why I don't have such problem as you described, until I found I have some similar config in my .spacemacs

  (setq purpose-user-mode-purposes '((coq-mode . edit)
                                     (tuareg-mode . edit)))
  (setq purpose-user-name-purposes '(("*goals*" . display)
                                     ("*response*" . display)
                                     ("*utop*" . repl)))

[bixuanzju]

@syl20bnr any plan when this can be merged? Thanks!

[vic]

@bixuanzju Have you tried to use the github fetcher instead of relying on the user to have already downloaded and compiled proof-general

      (proof-general :location (recipe
                        :fetcher github
                        :repo "ProofGeneral/PG"
                        :files ("*")))

Only issue here would be you still need to add at least generic, lib and coq directories with something like (concat (spacemacs//get-package-directory 'proof-general) "generic") to the load-path

Another option would be to define two packages like:

      ;; note that the name of the provided feature by generic/ is 'proof not 'proof-general
      (proof :location (recipe
                        :fetcher github
                        :repo "ProofGeneral/PG"
                        :files ("generic/*.el" "lib/*.el")))
      (coq :location (recipe
                        :fetcher github
                        :repo "ProofGeneral/PG"
                        :files ("coq/*.el")))

then compilation would be automatic and you would not to have to mess with the loadpath.

Thanks for all your effort on this layer :)

[rgrinberg]

I would love to have this in spacemacs as well.

[bixuanzju]

@vic Thanks! I adapted your first approach. Now the layer seems more robust.

[xnning]

I like this layer too. this is useful.

[vic]

BTW, yesterday I just had time to install this layer, and coq-mode worked fine.

Only issue was, after adding the coq layer to my spacemacs and reloading, lots of compiler warning/errors were displayed on the compilation buffer, it turned my emacs unusable (could not even change to other buffer), but after restarting emacs everything was working again (including the coq mode), so I don't know if this is related to the elisp installed by this packages or if it was something wrong with spacemacs itself.

[vic]

Haven't tested the layer with this, but as far as I remember, you'd have to add generic, lib and coq subdirectories as well, not really sure, does having just generic works for you?

[bixuanzju]

Oh yes, I've used it for some time without any problems.

[vic]

just for the record, here's the list of errors/warnings when fresh-installing this layer.

https://gist.github.com/vic/e30b8bf2579e8b93a25c69e59abf3243

as I said previously, once emacs is restarted everything seems to work ok.

[bixuanzju]

@vic I've checked again the official site of PG (https://github.com/ProofGeneral/PG), it says users only need to add the following:

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

So I think adding generic is enough perhaps.

[rgrinberg]

Seems to work great except for company-coq:

company-coq: Parsing of tactic grammar failed with error (error "Tactic parsing failure [(tactic:auto_using (quote AND) ))]").

[bixuanzju]

@rgrinberg This is probably related to incompatibility between company-coq and Coq v8.6. cpitclaudel/company-coq#126

[langston-barrett]

I can reproduce both the warnings and the company-coq issues, but otherwise this layer works very well for me. I'd love to see it integrated into the mainline!

For other folks who want to use this while it's unmerged:

cd ~/.emacs.d
git remote add coq https://github.com/bixuanzju/spacemacs
git fetch --all
git merge coq/coq-layer

then just enable the coq layer 😄

[gambogi]

@siddharthist:s/git add remote/git remote add/

[rgrinberg]

@bixuanzju Please apply the following patch:

diff --git a/layers/+lang/coq/packages.el b/layers/+lang/coq/packages.el
index 72d8dba7..8664ef0e 100644
--- a/layers/+lang/coq/packages.el
+++ b/layers/+lang/coq/packages.el
@@ -43,7 +43,9 @@
     :defer t
     :init
     (progn
-      (setq coq/proof-general-load-path (concat (spacemacs//get-package-directory 'proof-general) "generic"))
+      (setq coq/proof-general-load-path
+            (concat (configuration-layer/get-elpa-package-install-directory
+                     'proof-general) "generic"))
       (add-to-list 'load-path coq/proof-general-load-path))
     :config
     (progn

[bixuanzju]

@rgrinberg Thanks! I've already have had this change in my local machine.

[ajrouvoet]

Works quite nicely mostly. I have some trouble with opening buffers. If somehow the coq goal window has been closed then opening coq new coq files/window-move commands will make the file buffer dissapear.

Another problem I'm observing is that when I use this on a emacs daemon instance, it tends to "crash", i.e. the client closes regularly. Haven't investigated yet into what exactly happens.

[rgrinberg]

@syl20bnr Would you having a look at this? coq is a pretty important programming language and having a layer for it would be very useful for everyone. The layer itself has already been tested by me and other people in this thread so it seems to be ready for prime time.

[syl20bnr]

Yep I will merge it soon, I'm focusing on the language layers. Recently I need to work on a java project for work so I'm into this language layer for now, but I'll try to check coq this week-end 👀

[syl20bnr]

Thank you ! 💜

❗️ Watch out I made some changes to the key bindings to better fit the whole Spacemacs experience (still subjective though :-D), read carefully the commit message: fe168f0

I would prefer to have showing implicits keys on C-a, C-b, C-c but I don't know how frequent they are so I let the SPC m a i prefix. Another possibility is to drop the showing all key bindings since SPC u SPC m a a is the same as SPC m a A and then we could use the shifted keys for showing implicits.

I hope the key bindings changes won't be too much controversial, they have almost all a raison d'être. For instance the capital for all is inspired by bindings for tests in python (although there they are to activate debugging): https://github.com/syl20bnr/spacemacs/blob/develop/layers/+lang/python/funcs.el#L191-L204

Cherry-picked into develop branch, you can safely delete your branch.

[syl20bnr]

See also commit 8f1a5d6 where I cleaned up a bit the configuration.

Forgot to close this PR, closing it now :-)

[bixuanzju]

@syl20bnr Many thanks!

[cpitclaudel]

Thanks everyone for all the work on this! Plenty of exciting stuff in there, and I'm glad to see there's now an official Spacemacs layer for Coq (context: I wrote company-coq, and I co-maintain PG).

Some questions and nitpicks (apologies if any of this is obvious: I don't use Spacemacs myself):

• Could any of the Spacemacs bindings be added to Proof General/Company-Coq directly? I don't use evil-mode myself, but I understand that there are people that use it without using spacemacs. Wouldn't they benefit from these keybindings being in PG directly?

• We're working hard on getting PG ready for inclusion in MELPA. Is anyone interested in helping us beta-test this? If so, please see [WIP] ELPA/MELPA support ProofGeneral/PG#157 . I think we're very close, so help with testing would be most welcome, and this thread seems full of Coq+Emacs hackers :)

• About the implementation:

  • (company-coq :toggle (configuration-layer/package-usedp 'company)): I don't know if I understand this right, but company-coq has a lot more than company-mode backends; does this code mean that company-coq won't be enabled if company isn't?
  • :defer t, (add-to-list 'load-path coq/proof-general-load-path), and :mode ("\\.v\\'" . coq-mode) These three things look wrong: they are all handled by proof-site (that's what proof-site is for, in fact: autoloads, load path setup, and auto-mode-alist setup — all of which is needed because package.el is bad at multi-directory packages). require-ing proof-site just loads a bunch of autoloads; it doesn't load all of Proof General.
  • (spacemacs|diminish company-coq-mode): Company-coq's mode line icon is animated to show whether Coq is currently busy or not. Does this snippet disable the mode-line icon? If so, then this isn't the best way to do it, as company-coq will still compute updates and update the mode-line, despite it being hidden. You probably want to add 'spinner to the list of disabled features, but even better you could just show the icon as intended.
  • proof-splash-seen t: The original development of PG was part of a research project; some of the current development is funded by research institutions. Unless this strongly goes against spacemacs' policies, I think it would be better to leave the splash screen on, possibly with a note to use on how to disable this.
  • company-coq-disabled-features '(hello): I'd rather this wasn't disabled by default (it tells people about the existence of the company-coq tutorial). Maybe we should discuss whether to retain it on company-coq's issue tracker (I don't think this is Spacemacs-specific), but I added it because people didn't otherwise go through the tutorial, and I was frequently responding to private email requests for existing features. I'd be happy to add a note to the tutorial about disabling the greeting message, if that helps?
  • proof-three-window-mode-policy 'hybrid, proof-script-fly-past-comments t: If you think these are better defaults that the current ones, we'd be happy to merge them into PG; I don't think they are spacemacs-specific.

• A link to PG's manual and to company-coq's README in this layer's README would be appreciated.

• The PG logo is CC-BY-SA; I should be ok to use it in this layer's README, but the original author should be credited for his work.

• The README for this layer says that it was derived from work by @tchajed, but he doesn't seem to be credited in the source file (nor @olivierverdier, who IIUC wrote the original layer). Speaking of which, maybe @tchajed, @olivierverdier, and @mbrcknl have extra comments on the implementation? In any case, it could be useful to update their respective repos to point out that Spacemacs now has an official layer for Coq that supersedes the three existing ones.

Thanks for the cool work on this! Hopefully we can put PG in MELPA soon, and then update this layer to depend on PG instead of fetching it from Github :)

Clément.

(btw, is there a way for me to follow updates to this without following all Spacemacs updates? I only found out about it through the link to a now-fixed company-coq issue)

[rgrinberg]

I'll address the things that I can:

* Could any of the Spacemacs bindings be added to Proof General/Company-Coq directly? I don't use evil-mode myself, but I understand that there are people that use it without using spacemacs. Wouldn't they benefit from these keybindings being in PG directly?

I'm not sure what you mean here. All the original proof general/company coq bindings are still available directly.

- `(company-coq :toggle (configuration-layer/package-usedp 'company))`: I don't know if I understand this right, but company-coq has a lot more than company-mode backends; does this code mean that company-coq won't be enabled if company isn't?

That's correct. Is company-coq useful for auto-complete users for example? If that's the case it would be good to improve the layer to help users that don't use company.

(btw, is there a way for me to follow updates to this without following all Spacemacs updates? I only found out about it through the link to a now-fixed company-coq issue)

I don't think there's a way. But I would welcome you being cc'd on any changes to the coq layer.

[cpitclaudel]

That's correct. Is company-coq useful for auto-complete users for example? If
that's the case it would be good to improve the layer to help users that don't
use company.

The completion parts are company-specific, but company-coq does a lot more than completion (mainly prettification, subscripts, jumping to a definition, documentation, highlighting special comments, code folding, notifications, refactoring "require"s, notifications, etc.). All of these are available independently of company. The name of the package is a bit of a historical accident :)

I'm not sure what you mean here. All the original proof general/company coq bindings are still available directly.

Sorry for being unclear. I meant to ask whether I should merge part of the spacemacs keybindings to improve the experience of non-spacemacs evil users.

[tchajed]

Thanks for the work everyone! In case you're interested, I created issue #8450 to discuss configuration in this layer. I'd appreciate your feedback, especially if you use Coq!