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 with coq+compcert will not start #74083

Closed
veprbl opened this issue Nov 24, 2019 · 1 comment · Fixed by #74153
Closed

nix-shell with coq+compcert will not start #74083

veprbl opened this issue Nov 24, 2019 · 1 comment · Fixed by #74153
Labels
0.kind: bug 0.kind: regression Something that worked before working no longer 6.topic: coq

Comments

@veprbl
Copy link
Member

veprbl commented Nov 24, 2019

Describe the bug
Shell with coq and compcert will fail to start with a following message:

bash: COQPATH: unbound variable

This is an issue because compcert depends on coq so they would be always included to the shell started by nix-review. I noticed this issue while reviewing #73958.

I suspect this is caused by #72347.

To Reproduce
Steps to reproduce the behavior:

NIXPKGS_ALLOW_UNFREE=1 nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs/archive/814f9104d721dcbf267720d8964095626b45321b.tar.gz -p compcert -p coq

This does not reproduce on release-19.09

Expected behavior
Shell will start, shell prompt will appear.

Metadata
Please run nix run nixpkgs.nix-info -c nix-info -m and paste the result.

Maintainer information:

# a list of nixpkgs attributes affected by the problem
attribute:
# a list of nixos modules affected by the problem
module:

cc @Ericson2314 @thoughtpolice @jwiegley @vbgl

@veprbl veprbl added 0.kind: bug 0.kind: regression Something that worked before working no longer 6.topic: coq labels Nov 24, 2019
@eraserhd
Copy link
Contributor

I'm getting "CLASSPATH: unbound variable" since updating master an hour ago from last Sunday, and @hlolli reports "JAVA_HOME: unbound variable" started happening while working on #72331 eleven hours ago.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
0.kind: bug 0.kind: regression Something that worked before working no longer 6.topic: coq
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants