Stream: math-comp users

Topic: Nix for mathcomp


view this post on Zulip Assia Mahboubi (Oct 23 2020 at 07:34):

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)

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 07:35):

The nixos.org webpage advertises a slightly different command : sh <(curl -L https://nixos.org/nix/install), which seems to work better.

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 07:37):

Is this what I should do?

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 07:39):

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. "

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 07:41):

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

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 07:42):

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.

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 07:44):

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.

view this post on Zulip Maxime Dénès (Oct 23 2020 at 08:12):

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.

view this post on Zulip Maxime Dénès (Oct 23 2020 at 08:12):

About the sudo invocation, I wouldn't be surprised if this changed on the Nix side, that would not require it anymore.

view this post on Zulip Maxime Dénès (Oct 23 2020 at 08:13):

hmmm, no it seems to still require it

view this post on Zulip Maxime Dénès (Oct 23 2020 at 08:13):

can you give a pointer to the nixos.org page you saw?

view this post on Zulip Maxime Dénès (Oct 23 2020 at 08:14):

The one I found shows a different command than the one you wrote

view this post on Zulip Maxime Dénès (Oct 23 2020 at 08:14):

I found: https://nixos.org/download.html, where the command is: curl -L https://nixos.org/nix/install | sh

view this post on Zulip Maxime Dénès (Oct 23 2020 at 08:16):

that page says to run the command "as a user other than root with sudo permission", was it your case?

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:04):

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.

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:05):

so just to understand the source of the pb, what was the nixos page where you saw the "wrong" command?

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:05):

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

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:06):

even after restarting your X session?

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:07):

The "wrong command"(the one which did not work for me) is on this page

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:07):

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.

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:08):

I couldn't find that one

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:10):

I'm asking because it may be worth reporting / updating on the nixos side, if an outdated command stayed somewhere there

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:10):

This one works, so it is fine (and I cannot find again the page where I found it).

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:11):

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.

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:14):

Maxime Dénès said:

I couldn't find that one

Here

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:14):

But again, that one worked as well.

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:15):

I see, I don't know how that page relate to the other

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:16):

seems a bit strange indeed

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:16):

Once again, many thanks, now I think I know which changes I should propose for the mathcomp nix page.

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:16):

No pb, feel free to ask if you have other Nix issues, I'm also interested in getting some feedback

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:18):

(about using Nix for Coq developments)

view this post on Zulip Assia Mahboubi (Oct 23 2020 at 09:18):

Cool! I will do so.

view this post on Zulip Maxime Dénès (Oct 23 2020 at 09:18):

Even if it works fine, btw :)

view this post on Zulip Cyril Cohen (Oct 25 2020 at 12:17):

Thanks @Maxime Dénès and @Assia Mahboubi for your contributions to this doc :smile:

view this post on Zulip Karl Palmskog (Oct 25 2020 at 12:49):

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)

view this post on Zulip Karl Palmskog (Oct 25 2020 at 12:55):

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: Feb 08 2023 at 08:02 UTC