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
_______________________________________________
nix-dev mailing list
nix-dev@lists.science.uu.nl
http://lists.science.uu.nl/mailman/listinfo/nix-dev

Reply via email to