ProofGeneral
Void variable: nil-completion-table
#386 is fixed, but unfortunately now there is another one:
https://travis-ci.org/mrkkrp/dot-emacs/jobs/423066997#L3052
Debugger entered--Lisp error: (void-variable nil-completion-table)
OK, I know what the problem is.
The package.el installation process goes like this:
- Unpack proof-general.xyz.tar
- Reload any proof-general files found in load-history
- Compile all unpacked files (this adds a bunch of things to load-history)
- Reload any proof-general files found in load-history (this reloads all the files that were
required during compilation)
That last step is what's causing the issue on the CI. But why only on the CI? The reason is that the code implementing that last step is broken:
(mapcar
(lambda (x) (let* ((file (file-relative-name x dir))
;; Previously loaded file, if any.
(previous
(ignore-errors ;; ← !!
(file-name-sans-extension
(file-truename (find-library-name file)))))
(pos (when previous (member previous history))))
;; Return (RELATIVE-FILENAME . HISTORY-POSITION)
(when pos
(cons (file-name-sans-extension file) (length pos)))))
(directory-files-recursively dir "\\`[^\\.].*\\.el\\'")))))
Notice the bit where I wrote ;; ← !!. That ignore-errors call is supposed to catch errors raised by find-library-name when it doesn't find the corresponding library.
But! find-library-name is defined in find-func… and package.el never loads that library. Hence find-library-name is never defined, and the find-library-name call always raises an unbound function error.
… except of course if something else loads find-func. Something like compiling another package, for example. Plenty of packages (e.g. flycheck) explicitly (require 'find-func), which causes it to be loaded when these packages are compiled.
It's not safe to load PG without choosing a proof assistant first, but package.el does exactly this. Or, more precisely, package.el does that if something else has loaded find-func before package.el gets to installing proof-general.
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 M-: (require 'find-func) before M-x package-install proof-general. This will crash.
We need to fix this. I've sent an email to the emacs-devel list to ask if we can bypass the reload, but if not we need to make sure that all files in PG can be loaded safely even without a proof assistant set.
cc @erikmd, @Matafou.
We need to fix this. I've sent an email to the emacs-devel list to ask if we can bypass the reload, but if not we need to make sure that all files in PG can be loaded safely even without a proof assistant set.
I should clarify that this looks non-trivial: PG is full of things like (defpgcustom completion-table …, which defined a variable called <proof-assistant>-completion-table, which don't get run by the byte-compiler, but do get run by load and will create the wrong variables if the prover isn't preemptively set.
The best solution might be to set the prover's name to coq by default (instead of nil), and tell people to restart Emacs after installing PG if they want to use it with something other than Coq?
The best solution might be to set the prover's name to coq by default (instead of nil), and tell people to restart Emacs after installing PG if they want to use it with something other than Coq?
(Except that's not easy either, because we can't just set one variable; we need to call proof-ready-for-assistant for that, and if we do that unconditionally it won't be possible to use other proof assistants, even after a restart)
Another solution would be to advise package--load-files-for-activation. We'd force it to return nil for poof-general if a proof-assistant symbol hasn't been set.
I should clarify that this looks non-trivial: PG is full of things like (defpgcustom completion-table …, which defined a variable called
-completion-table, which don't get run by the byte-compiler, but do get run by load and will create the wrong variables if the prover isn't preemptively set.
This was a bit more alarmist than needed: pg-custom isn't required when compiling, so the issue is more circumscribed that I thought. package.el will only reload files that have been required by compilation, and these files already have risky chunks marked using (bound-and-true-p byte-compile-current-file). We need to make sure that none of these forms are run when package.el loads us, either.
The easiest way might be to explicitly check whether a proof assistant has been set, using (bound-and-true-p proof-assistant-symbol)
Sounds good. But PG is really not made to be used by the emacs session that has compiled it. Does compilation fail? Or is it just when loading a prover file? Maybe the only thing we need to do is warn that one should restart emacs after installing pg? Not very satisfying though.
Maybe the only thing we need to do is warn that one should restart emacs after installing pg? Not very satisfying though.
The problem isn't just using PG after installing it, it's compiling it through package.el
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):
- Start emacs, run
M-: (fmakunbound 'find-library-name), then install the package and restart Emacs. - Temporarily disable most of your config, install, then reenable the rest of your config; if you use plain Emacs, starting with
emacs -qand installing might work. - Add a call to
(package-install 'proof-general)early in your init file.
Let me know if any of these work