I am using several Coq- and Proofgeneral-Versions at once, in different
shells. The problem is that the proofgeneral-command does not really
work in nix-shells: Emacs complains that
Cannot open load file: no such file or directory,
for example. I tracked this to a variable $PGHOME in the proofgeneral
script. We have, in the corresponding file,
and then some magic that appears that (should?) set PGHOME to
PGHOMEDEFAULT. In the end, we have
exec $EMACS $STARTUP -eval "(or (featurep (quote proof-site)) (load
\"$PGHOME/generic/proof-site.el\"))" -f proof-splash-display-screen "$@"
But this is not correct, because the actual file is in
A workaround is to directly use M-x load-file with the latter file, but
it would be nice to fix this such that the proofgeneral command works
again. Is this possible?
nix-dev mailing list