Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

nix-shell -p agda fails #55964

Closed
karljs opened this issue Feb 17, 2019 · 7 comments
Closed

nix-shell -p agda fails #55964

karljs opened this issue Feb 17, 2019 · 7 comments
Labels
6.topic: agda "A dependently typed programming language / interactive theorem prover"

Comments

@karljs
Copy link

karljs commented Feb 17, 2019

Issue description

Opening a nix-shell with the agda package fails.

Steps to reproduce

nix-shell -p agda

Technical details

The error message is:

error: while evaluating the attribute 'buildInputs' of the derivation 'shell' at /nix/store/w8cnxvdyd3ngwn71pb1vdpiz3vj2xhv0-nixpkgs-19.03pre169106.1a88aa9e0cd/nixpkgs/pkgs/build-support/trivial-builders.nix:7:14:
cannot coerce a set to a string, at /nix/store/w8cnxvdyd3ngwn71pb1vdpiz3vj2xhv0-nixpkgs-19.03pre169106.1a88aa9e0cd/nixpkgs/pkgs/build-support/trivial-builders.nix:7:14

Please run nix-shell -p nix-info --run "nix-info -m" and paste the
results.

 - system: `"x86_64-linux"`
 - host os: `Linux 4.20.7-200.fc29.x86_64, Fedora, 29 (Workstation Edition)`
 - multi-user?: `no`
 - sandbox: `yes`
 - version: `nix-env (Nix) 2.2.1`
 - channels(karl): `"nixpkgs-19.03pre169106.1a88aa9e0cd"`
 - nixpkgs: `/home/karl/.nix-defexpr/channels/nixpkgs`
@davidak
Copy link
Member

davidak commented Feb 18, 2019

It also fails on NixOS:

[davidak@ethmoid:~]$ nix-shell -p agda
error: cannot coerce a set to a string, at /nix/store/yqhfqlplypysidkvqq3vfi5jf2qxd33l-nixos-18.09.2203.9bd45dddf81/nixos/pkgs/stdenv/generic/make-derivation.nix:177:11

  • system: "x86_64-linux"
  • host os: Linux 4.14.101, NixOS, 18.09.2203.9bd45dddf81 (Jellyfish)
  • multi-user?: yes
  • sandbox: yes
  • version: nix-env (Nix) 2.1.3
  • channels(root): "nixos-18.09.2203.9bd45dddf81, nixos-hardware, nixos-unstable-19.03pre169108.36f31600749"
  • nixpkgs: /nix/var/nix/profiles/per-user/root/channels/nixos

@arianvp
Copy link
Member

arianvp commented Feb 18, 2019

That's because agda is not a package but a set containing functions like mkDerivation to create agda packages. Agda itself is under haskellPackages.Agda

I don't think the agda stuff is documented anywhere. I found it confusing too.

@davidak
Copy link
Member

davidak commented Feb 18, 2019

That's because agda is not a package but a set containing functions

Maybe the error should say that?

@arianvp
Copy link
Member

arianvp commented Feb 18, 2019

The error says that. "Cannot coerce set to a string" suggests that it's not a package but a set.

Same thing occurs, I think , if you try:

nix-shell -p haskellPackages

Im not sure if it's possible to customise error messages like that. Maybe someone else can chime in on that.

But the best way (apart from a better error message) to fix this issue is to add a section in the manual about how agda language support works; as it's currently undocumented

@arianvp
Copy link
Member

arianvp commented Feb 18, 2019

Related: #39318

It would make more sense I think to expose agda under the agda attribute, and move the current agda attribute to something like agdaPackages. That would maybe also clear confusion.

@karljs
Copy link
Author

karljs commented Feb 19, 2019

Thanks for explaining this. I like the idea of changing to agdaPackages to make this more self-documenting.

@turion
Copy link
Contributor

turion commented May 15, 2020

This has recently been fixed by #76653: nix-shell -I nixpkgs=channel:nixpkgs-unstable -p agda works.

@veprbl veprbl closed this as completed May 15, 2020
@veprbl veprbl added the 6.topic: agda "A dependently typed programming language / interactive theorem prover" label Feb 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
6.topic: agda "A dependently typed programming language / interactive theorem prover"
Projects
None yet
Development

No branches or pull requests

5 participants