Stream: Nix toolbox devs & users

Topic: home-manager on nixos package management help?

Quinn (Jan 06 2022 at 19:06):

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?

Stefan Malewski (Jan 06 2022 at 22:56):

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.

Quinn (Jan 06 2022 at 23:26):

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.

Stefan Malewski (Jan 06 2022 at 23:34):

nix-direnv works really well. It manages the environments such that each buffer has the correct environment. There is an emacs plugin in melpa.

Stefan Malewski (Jan 07 2022 at 02:44):

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.

Paolo Giarrusso (Jan 07 2022 at 08:12):

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).

Pierre Courtieu (Jan 07 2022 at 08:16):

True. Proofgeneral supports only one running coq process per emacs.

Stefan Malewski (Jan 07 2022 at 16:12):

There is a Nix related stream in this zulip, maybe you can move the topic there.

Karl Palmskog (Jan 07 2022 at 16:13):

I will move this topic to that stream

Notification Bot (Jan 07 2022 at 16:13):

This topic was moved here from #Coq users > home-manager on nixos package management help? by Karl Palmskog

Quinn (Jan 09 2022 at 22:35):

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

Quinn (Jan 09 2022 at 23:05):

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