Stream: Nix toolbox devs & users

Topic: home-manager on nixos package management help?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Pierre Courtieu (Jan 07 2022 at 08:16):

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

view this post on Zulip Stefan Malewski (Jan 07 2022 at 16:12):

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

view this post on Zulip Karl Palmskog (Jan 07 2022 at 16:13):

I will move this topic to that stream

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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