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

[Christoph-Simon Senjak]

Hi

On 22.09.2016 19:32, Pavel Chuprikov wrote:
> Hi,
>
> I think that the problem is that the patch
> <https://github.com/NixOS/nixpkgs/blob/7475728593a49f09c4b7b959b15513aee38ab4b4/pkgs/applications/editors/emacs-modes/proofgeneral/pg.patch> from
> nixpkgs is not applied for version 4.2 of proofgeneral, but only for
> version 4.3pre. Due to this PGHOME is incorrectly set to MYDIR, instead
> of nix-provided PGHOMEDEFAULT.

Ok, 4_3_pre works, thx.

regards,
CSS

> Regards,
> Pavel
>
>
> чт, 22 сент. 2016 г. в 16:01, Christoph-Simon Senjak
> <christoph.senjak at googlemail.com <mailto:christoph.senjak at googlemail.com>>:
>
>     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 at lists.science.uu.nl <mailto:nix-dev at lists.science.uu.nl>
>     http://lists.science.uu.nl/mailman/listinfo/nix-dev
>