I'm wondering if anyone uses home-manager
on nixos
.
My home.nix
includes:
home.packages = with pkgs; [
...
# Coq
coq
coqPackages.coq-ext-lib
coqPackages.ITree
coqPackages.VST
coqPackages.QuickChick
...
];
seems to install coq to /home/qd/.nix-profile/bin
, so I tell proof general to load that up:
(custom-set-variables
`(coq-prog-name "/home/qd/.nix-profile/bin/coqtop")
)
And the coq session runs. But lines like
From QuickChick Require Import QuickChick
or
Require Import VST.veric.version.
all fail.
How do I ensure that packages are talking to my coq install?
You shouldn't install libraries in home.nix only applications. What you need is a shell environment for your project.
Create a shell.nix
file at the root of your project with the following expression:
let
pkgs = import <nixpkgs> {};
in
pkgs.mkShell {
buildInputs = with pkgs.coqPackages; [ coq coq-ext-lib ITree VST QuickChick ];
}
Then, nix-shell
will create an environment with the necessary environment variables, but no emacs support.
For that, install nix-direnv and follow the instructions.
Feels like a hack but what I could do is make a nix-shell
like you describe and then type which coqtop
and set coq-prog-name
to that, to get emacs support. I've done something like that before.
nix-direnv
works really well. It manages the environments such that each buffer has the correct environment. There is an emacs plugin in melpa.
Forgot to mention that for this setup to work you need to set coq-prog-name
to coqtop
instead of an absolute path, that way can find the one sourced by nix-shell.
and (please tell me if it’s obvious for everybody) I guess you can’t use emacsclient
but you need a separate emacs per folder (and you must stop Spacemacs or similar from reloading the environment at boot).
True. Proofgeneral supports only one running coq process per emacs.
There is a Nix related stream in this zulip, maybe you can move the topic there.
I will move this topic to that stream
This topic was moved here from #Coq users > home-manager on nixos package management help? by Karl Palmskog
nix-direnv works really well. It manages the environments such that each buffer has the correct environment. There is an emacs plugin in melpa.
I'm not finding nix-direnv
on melpa, just direnv
Just a note--- a major problem I had turned out to be .direnv
caching stuff, and I was unable to get it to work for a while-- rm -rf .direnv
fixed it.
Last updated: Dec 05 2023 at 05:01 UTC