[Nix-dev] Proofgeneral in nix-Shell not working

[Christoph-Simon Senjak]

Hi.

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,

PGHOMEDEFAULT=/nix/store/44v7r61fx96avicggc1wdckch7fa42r9-ProofGeneral-4.2/share/emacs/site-lisp/ProofGeneral

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

/nix/store/44v7r61fx96avicggc1wdckch7fa42r9-ProofGeneral-4.2/share/emacs/site-lisp/site-start.d/pg-init.el

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