[Nix-dev] AgdaStdlib Doesn't install

roconnor at theorem.ca roconnor at theorem.ca
Tue Oct 6 03:50:18 CEST 2015


Does

$ nix-store --read-log /run/current-system/sw

say anything interesting?

$ nix-store -q -deriver /run/current-system/sw

will output a filename.  Are there references to AgdaStdlib in that file?

On Sat, 3 Oct 2015, Taeer Bar-Yam wrote:

> Assumption I: Check. Putting in bad syntax to configuration.nix results in an error from nixos-rebuil
> Assumption II: I'm not sure exactly what you mean by "check under test_profile"
> The directory at `nix-build --no-out-link "<nixpkgs>" -A AgdaStdlib` has a share/agda directory, which I think is what you're looking for.
> Assumption III: I have succeeded in installing other packages. (e.g. emacs) With this syntax. There is an emacs folder in /run/current-system/sw/share/
> putting "42" in that same place does result in an error.
> Assumption IV: I'm not sure how this works. Where is all-packages.nix? I switched to the unstable branch with nix-channel, but that should be a user-level change, right? Not system-level.
> Assumption V: nixos-rebuild switch changes what I have installed. That should rule out that problem, no?
> 
> Thanks for the help. Any other things that could be going wrong?
> 
> On Fri, Oct 2, 2015 at 11:41 PM, Bryan Gardiner <bog at khumba.net> wrote:
>       On Fri, 2 Oct 2015 19:40:19 -0700
>       James Cook <james.cook at utoronto.ca> wrote:
>
>       > On 2 October 2015 at 13:12, Taeer Bar-Yam <tb442 at cornell.edu> wrote:
>       > > I recently added pkgs.haskellPackages.Agda and pkgs.AgdaStdlib to my
>       > > environment.systemPackages (in configuration.nix), and Agda still can't find
>       > > the stdlib packages.
>       > >
>       > > I discussed this with someone on IRC for a while, and we discovered that I
>       > > don't have an "agda" folder in /run/current-system/sw/share/ which I am
>       > > supposed to have if pkgs.AgdaStdlib is in environment.systemPackages.
>       > >
>       > > Furthermore, when they put the same line in their configuration.nix, that
>       > > folder did appear in their /run/current-system/sw/share/
>       > >
>       > > I'm sure this will come up, so I'll confirm now: I have `nixos-rebuild
>       > > switch`ed to the new system.
>       > >
>       > > Does anyone have an idea of what's going on here? Is there any other
>       > > diagnostic information that would be helpful?
>       > >
>       > >   --Taeer
>       >
>       > Hi Taeer,
>       >
>       > That's really strange. I think you will have to debug this on your
>       > end. All I can think if is to examine every little step that makes us
>       > think putting pkgs.AgdaStdlib in your configuration should make it
>       > appear under /run/current-system/sw/share/. For example:
>       >
>       > - Assumption: nixos-rebuild is reading your configuration.nix. You
>       > could test this by putting some bad syntax at the start of
>       > configuration.nix and rebuilding.
>       >
>       > - Assumption: pkgs.AgdaStdlib produces a "share/agda" directory with
>       > the version of nixpkgs you are using. You could try installing it with
>       > nix-env -p test_profile -i -A pkgs.AgdaStdlib and checking under
>       > test_profile
>       >
>       > - Assumption: Your syntax for specifying environment.systemPackages is
>       > correct. Try putting other packages there and see if their files show
>       > up under /run/current-system/sw/share/. Try putting something that's
>       > not a package there (e.g. the number 42) and see if nixos-rebuild
>       > complains (it should).
>       >
>       > - Assumption: nixos-rebuild is using the version of nixpkgs you think
>       > it's using. You could test this by messing up your nixpkgs (e.g. by
>       > adding bad syntax to all-packages.nix) and seeing if nixos-rebuild
>       > complains.
> 
> There's also the one that tripped me up:
> 
> - Assumption: NixOS is mounting /boot properly, otherwise new system
>   generations won't take effect on boot but 'switch' will think
>   everything's applied.
> 
> 
> 
>

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''


More information about the nix-dev mailing list