search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
488 stars 86 forks source link

"I can't find any complete commands to process!" #179

Open jonsterling opened 7 years ago

jonsterling commented 7 years ago

I'm having a strange issue; with a completely fresh install of PG and Coq (8.6), almost every time I try to check a development in Emacs I receive the error "I can't find any complete commands to process!"

For the record, this development parses and compiles fine with Coq. Has this happened to anyone else? I've tried it both with company-coq enabled and disabled, in case there was some weird interaction between the packages.

Thanks for any help you can give!

cpitclaudel commented 7 years ago

An example would help. Does this actually happen with any script?

jonsterling commented 7 years ago

@cpitclaudel Yes, as far as I can tell it happens for any script, even a script of just one line. I'm trying to determine at the moment whether this is being caused by other packages that are loaded, since PG works fine for all my friends...

jonsterling commented 7 years ago

@cpitclaudel OK, I think I have determined the problem (at least at a superficial level). When I disable the package pollen-mode in my Emacs configuration, PG works fine. I bet the bug is in pollen-mode, not PG...

For now, I'll just disable that mode; once I learn more about Emacs hacking, maybe I'll be able to understand what is really going on.

I think you can feel free to close this ticket if you don't think there's anything to be done on PG's side.

cpitclaudel commented 7 years ago

Hmm, surprising. Why should pollen-mode run while PG is active ? Or are you editing Coq snippets inside a pollen file ?

jonsterling commented 7 years ago

@cpitclaudel It's so weird! pollen-mode is not activated, but somehow just having the package loaded in my config causes a problem, as far as I can tell. I wish I could be more precise about what is happening, but I am just a "user" of Emacs and don't really understand how it works yet.

cpitclaudel commented 7 years ago

How do you load the package ?

jonsterling commented 7 years ago

I am using use-package.

cpitclaudel commented 7 years ago

Can you show the full use-package form that you're using ?

jonsterling commented 7 years ago

@cpitclaudel Here's what I had:

(use-package pollen-mode
  :ensure t)

I loaded PG later in the file in the following way:

(let ((proof-site "~/.emacs.d/PG/generic/proof-site.el"))
  (when (file-exists-p proof-site)
    (require 'proof-site proof-site)
    (use-package company-coq
      :ensure t
      :config (add-hook 'coq-mode-hook #'company-coq-mode))))
cpitclaudel commented 7 years ago

Got it, thanks. I'll try to reproduce this.