New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Void variable: nil-completion-table #388
Comments
Thanks, let me try to reproduce / investigate this |
Seems to be related to the |
OK, I know what the problem is. The package.el installation process goes like this:
That last step is what's causing the issue on the CI. But why only on the CI?
Notice the bit where I wrote But! … except of course if something else loads It's not safe to load PG without choosing a proof assistant first, but Bottom line, it's a mess. The reason why PG installs cleanly on most machines is that there's a bug in package.el that disables an extra loading (which we don't even need…); the bug happens on most machines, but on the ones where it doesn't happen (like on @mrkkrp's CI), PG can't be installed cleanly. To reproduce the bug: run We need to fix this. I've sent an email to the |
I should clarify that this looks non-trivial: PG is full of things like The best solution might be to set the prover's name to |
(Except that's not easy either, because we can't just set one variable; we need to call |
Another solution would be to advise |
This was a bit more alarmist than needed: The easiest way might be to explicitly check whether a proof assistant has been set, using |
Sounds good. But PG is really not made to be used by the emacs session that has compiled it. |
OK I see, compilation breaks. |
The problem isn't just using PG after installing it, it's compiling it through package.el |
So there is no obvious fix for this right now, right? |
What is a workaround if I want to start using proof-general? I am getting this error when I try to install it. |
Just restarting your emacs after installation should be fine. Performance my suffer a bit. Otherwise, there are a few workarounds that should work (I haven't tested them):
Let me know if any of these work |
#386 is fixed, but unfortunately now there is another one:
https://travis-ci.org/mrkkrp/dot-emacs/jobs/423066997#L3052
The text was updated successfully, but these errors were encountered: