Hi, I am trying to follow the instructions on this page so as to use nix-shell
for managing the dependencies of the analysis
library. The first thing to do is to execute sh <(curl https://nixos.org/nix/install)
. I did so, but nothing happens:
$ sh <(curl https://nixos.org/nix/install)
% Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0
(instantaneous, and no sudo
invocation triggered)
The nixos.org
webpage advertises a slightly different command : sh <(curl -L https://nixos.org/nix/install)
, which seems to work better.
Is this what I should do?
Then the following sentence says: "You need to set several environment variables before you proceed to step 2. The simplest way to do so is to log out from your session and log in again. "
But there is nothing called step 2
in this documentation (I guess this refers to the next section, about using mathcomp). Unfortunately, logging out and in again does not give me access to the nix-shell
command:
$ nix-shell
nix-shell : commande introuvable
But the last step of the installation procedure for nix said:
Installation finished! To ensure that the necessary environment
variables are set, either log in again, or type
. /home/assia/.nix-profile/etc/profile.d/nix.sh
in your shell.
Executing the nix.sh
script works fine, but how can I make this persistent? I quick look at the documentation on nix's website did not help me for this.
Hi @Assia Mahboubi ! I wasn't involved in writing these instructions (I do use Nix, though), so I may be wrong , but I don't see any reason why the command to run would be different from the one on the Nix website.
About the sudo invocation, I wouldn't be surprised if this changed on the Nix side, that would not require it anymore.
hmmm, no it seems to still require it
can you give a pointer to the nixos.org page you saw?
The one I found shows a different command than the one you wrote
I found: https://nixos.org/download.html, where the command is: curl -L https://nixos.org/nix/install | sh
that page says to run the command "as a user other than root with sudo permission", was it your case?
Hi @Maxime Dénès Thanks for your answer! Indeed, the command curl -L https://nixos.org/nix/install | sh
works better, and prompts for a sudoer password.
so just to understand the source of the pb, what was the nixos page where you saw the "wrong" command?
But then my problem is that I can only have access to the nix-shell
command in a terminal where I execute the . /home/assia/.nix-profile/etc/profile.d/nix.sh
even after restarting your X session?
The "wrong command"(the one which did not work for me) is on this page
Yes but you wrote:
The nixos.org webpage advertises a slightly different command : sh <(curl -L https://nixos.org/nix/install), which seems to work better.
I couldn't find that one
I'm asking because it may be worth reporting / updating on the nixos side, if an outdated command stayed somewhere there
This one works, so it is fine (and I cannot find again the page where I found it).
But now I think I understand my problem, from the mathcomp page I thought that it was a terminal session (not the X) to be restarted. The nix documentation seems fine.
Maxime Dénès said:
I couldn't find that one
But again, that one worked as well.
I see, I don't know how that page relate to the other
seems a bit strange indeed
Once again, many thanks, now I think I know which changes I should propose for the mathcomp nix page.
No pb, feel free to ask if you have other Nix issues, I'm also interested in getting some feedback
(about using Nix for Coq developments)
Cool! I will do so.
Even if it works fine, btw :)
Thanks @Maxime Dénès and @Assia Mahboubi for your contributions to this doc :smile:
hmm, is the doc supposed to talk about "1.11.0+beta1"? (at the end)
I thought the agreed version naming format was 1.1X+betaY (and also the stable "1.11.0" is probably what you want)
finally, would be great to have sanctioned boilerplate for stating dependencies on ssreflect and mathcomp in default.nix
. For example, the following is the only way I know to depend on master
:
let
ssreflect =
coqPackages.ssreflect.overrideAttrs(_: rec {
name = "coq-${coq.coq-version}-ssreflect-${version}";
version = "dev";
src = fetchTarball "https://github.com/math-comp/math-comp/tarball/master";
})
and I have no idea whether this is idiomatic
Last updated: Mar 29 2024 at 15:02 UTC