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, /nix/store/44v7r61fx96avicggc1wdckch7fa42r9-ProofGeneral-4.2/generic/proof-site.el

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?

Best Regards,
Christoph-Simon Senjak
nix-dev mailing list

Reply via email to