Stream: Nix toolbox devs & users

Topic: nix environment for mathcomp PRs


view this post on Zulip Christian Doczkal (Jun 07 2021 at 12:35):

I finally got around to installing nix and I would like to use it to build my local git clone of some repository in an environment that corresponds to an existing PR (in order to create an overlay). Is this the right place to ask these questions? Can someone point me in the right direction?

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 12:40):

Hi @Christian Doczkal, I can help / guide you through this process.

view this post on Zulip Christian Doczkal (Jun 07 2021 at 14:54):

@Théo Zimmermann Sorry, I was called away. So where do I start?

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 14:54):

No problem, I happen to be available again. The starting point should be https://github.com/coq-community/coq-nix-toolbox.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 14:55):

In particular, follow the Standalone instructions since you already have Nix.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 14:56):

Is this repository a new thing or some existing package?

view this post on Zulip Christian Doczkal (Jun 07 2021 at 14:56):

I'm talking about a PR for mathcomp with an overlay for fourcolor

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 14:57):

Oh OK, I misunderstood then :smile:

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 14:57):

Let me reboot (figuratively).

view this post on Zulip Christian Doczkal (Jun 07 2021 at 14:57):

Well, my initial messages was (purposefully) more generic than that, but possibly too generic nonetheless.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 14:58):

The most important missing point from your initial message is that you are trying to use Nix somewhere where the toolbox is already installed.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:01):

OK, I have an issue though, which is that @Cyril Cohen made this kind of workflow so simple in the latest version of the toolbox but apparently, he didn't yet update the version that is used on math-comp.

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:02):

I currently have a local clone of math-comp and I'm on a branch that corresponds to the PR I want to create/update. Now I want to compile another package in the resulting environment. That is, the equivalent of creating a new switch and pinning mathcomp to the local version.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:04):

OK so first, in order to avoid rebuilding what CI has already built, it would help if you did the Cachix setup step described here: https://github.com/math-comp/math-comp/wiki/Nix-Example:-Instantenously-work-on-a-branch#setup-cachix-once-and-for-all--if-not-already-done

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:06):

Yes, I did not install the latest toolbox for mathcomp yet... it's here: ready to merge once we release the toolbox: math-comp/math-comp#726

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:09):

So I will defer to @Cyril Cohen to explain how you can do this in the version currently available on math-comp.

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:11):

Well, I did the cachix use math-comp, but the PR is currently not up to date anyway. So the cache won't have anything useful this time around.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:11):

I'm a bit lost: you want to build which project with which versions of what?

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:12):

IIUC that's the same use case as https://github.com/coq-community/coq-nix-toolbox/issues/24 but for math-comp instead of Coq.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:12):

yes, but if one installs the toolbox in their own project, they can have the full support of the toolbox

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:13):

That's why I'm asking

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:14):

I am trying to build coq-fourcolor against a PR for mathcomp. ^^

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:14):

Christian Doczkal said:

I am trying to build coq-fourcolor against a PR for mathcomp. ^^

for working in fourcolor or outside (e.g. the graph library) ?

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:15):

In order to prepare the overlay for coq-fourcolor that this PR requires. Théo had it right, see above.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:17):

ok

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:17):

I can make a PR in fourcolor to add the toolbox and you can take it from there?

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:17):

OK, for this time, it works.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:19):

We're in a pre-release state. For July 1st I will tidy mathcomp as well and you will be able to use coq-community/coq-nix-toolbox#24

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:23):

I will soon merge math-comp/fourcolor#33, but you could already use it

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:23):

I wasn't aware that you also need to install the toolbox in the reverse dependencies.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:24):

Christian Doczkal said:

I wasn't aware that you also need to install the toolbox in the reverse dependencies.

you don't have to... but since the last version of the toolbox is not installed in mathcomp (and I do not want to do it right now), it's easier to just install the toolbox in the reverse deps

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:25):

It's not necessary, but it's sufficient

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:25):

Well, I can also do things manually for now and you install the toolbox in mathcomp and fourcolor once it's actually stable.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:26):

Now you only need to add the line

"8.13".coqPackages.mathcomp.override.version = "brancheName/#yourPR";

in .nix/config.nix

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:30):

You're talking of the one on the four-color side, right?

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:31):

Wait, so I should update the PR first, then let CI run (and fail)? Also, in which version of this file on which branch (of which repository) do I add the line?

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:31):

No need.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:31):

I think Cyril was talking of the four-color repo.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:32):

But you can also do this on the command-line with nix-shell --arg override '{mathcomp = "#yourPR";}'

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:33):

However, you will need first to checkout this version of the repo: https://github.com/math-comp/fourcolor/pull/33

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:34):

I am also updating the toolbox of mathcomp, I think it runs under 1h and after that you can rebase the mathcomp PR as well, you'll have "l'embarras du choix"

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:34):

So, I should update the PR (in the mathcomp repository), but I do not need to wait for CI to finish before I can do the override nix shell from the (patched) four-color clone?

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:34):

You do not need to update the PR on the mathcomp side AFAICT.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:35):

and you do not need to wait for the CI to finish either

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:35):

bit how does #yourPR do the right thing, if the PR with that number does not ...

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:36):

yes, the overloading instruction does not depend on the toolbox being installed in the dependencies

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:36):

Ah! I got it. Then yes, if your local version is not the same as the one on the math-comp repo, you'll have to push.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:37):

(Although it is also supported to point to a local version.)

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:37):

Well, I think I will wait for Cyril to merge the new toolbox (on mathcomp), then do the rebase/push and then bug you again tomorrow ;)

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:38):

That's fine with me.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:39):

I'm lost

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 15:39):

With respect to what?

view this post on Zulip Cyril Cohen (Jun 07 2021 at 15:40):

as to why @Christian Doczkal could not use math-comp/fourcolor#33 right now

view this post on Zulip Christian Doczkal (Jun 07 2021 at 15:42):

I can, but maybe I want to learn how to do the normal/regular way, and I used the time I budgeted for this today.

view this post on Zulip Cyril Cohen (Jun 07 2021 at 16:21):

ok this was a mistake from me not to merge the experimental toolbox in mathcomp, I just detected two missing overlays (one in coqeal and one in abel) that we will have to fix before releasing the next mc release...

view this post on Zulip Cyril Cohen (Jun 08 2021 at 10:24):

@Christian Doczkal FTR I merged math-comp/math-comp#726 yesterday so you can rebase your mathcomp PR, then type nix-shell --argstr job fourcolor from the root of your workdir for the PR, then cd to fourcolor and you can make -j8 -k from there :)

view this post on Zulip Christian Doczkal (Jun 08 2021 at 10:28):

Well, I saw the merge, and updated the PR, but I had forgotten the rebase. Consequently, CI failed terribly. Let's see what happens after the rebase. ^^

view this post on Zulip Christian Doczkal (Jun 08 2021 at 10:30):

There also seems to be an issue with GitHub, because I don't get any progress or information on the CI run. Only a turning circle above the comment text field.

view this post on Zulip Cyril Cohen (Jun 08 2021 at 10:36):

Yep, github looks fishy right now, maybe it's being hacked

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 10:40):

That's not the only thing that looks down. cache.nixos.org too

view this post on Zulip Cyril Cohen (Jun 08 2021 at 10:41):

oO

view this post on Zulip Cyril Cohen (Jun 08 2021 at 10:41):

not on my side...

view this post on Zulip Christian Doczkal (Jun 08 2021 at 10:42):

Théo Zimmermann said:

That's not the only thing that looks down. cache.nixos.org too

I also get an "Error 503 Service Unavailable"

view this post on Zulip Cyril Cohen (Jun 08 2021 at 10:42):

@Christian Doczkal you do not need to rely on precompilation of anything... you can run the nix-shell on your computer right now... in worst case scenario you should be set in 7 min

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 10:42):

Christian Doczkal said:

Théo Zimmermann said:

That's not the only thing that looks down. cache.nixos.org too

I also get an "Error 503 Service Unavailable"

I get HTTP 502 errors

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 10:49):

I've also got a GitLab pipeline failing to reach deb.debian.org!

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 10:50):

https://www.dailysabah.com/world/global-news-websites-down-amid-internet-outage/news

view this post on Zulip Cyril Cohen (Jun 08 2021 at 12:35):

@Christian Doczkal did you have the opportunity to try?

view this post on Zulip Christian Doczkal (Jun 10 2021 at 11:55):

@Cyril Cohen Yes, I did try the nix-shell --argstr job fourcolor variant after locally rebasing (yet again) to the latest state of mathcomp. This works really well, although I am a bit bewildered by the huge amount of packages that are being copied from the cache, which even included systemd? :grimacing:

view this post on Zulip Théo Zimmermann (Jun 10 2021 at 12:23):

Yes, that's the deal. Every dependency of a Nix package is pinned to a specific version and fetched to the store.

view this post on Zulip Théo Zimmermann (Jun 10 2021 at 12:23):

But once you have it there, you won't pull it again until its version changes, so not for a good while.

view this post on Zulip Christian Doczkal (Jun 10 2021 at 15:34):

Just out of curiosity, what's up with time in Nix? This is what I get from Coq in a nix-shell (mathcomp default)

$ coqc --version
The Coq Proof Assistant, version 8.13.1 (January 1980)
compiled on Jan 1 1980 0:00:00 with OCaml 4.10.2

view this post on Zulip Théo Zimmermann (Jun 10 2021 at 15:55):

Nix is all about reproducible builds. Sticking the time at which a program was compiled in the binary makes the build non-reproducible. So Nix patches that.

view this post on Zulip Théo Zimmermann (Jun 10 2021 at 15:55):

But in future versions of Coq, this info is removed anyway.

view this post on Zulip Enrico Tassi (Jun 10 2021 at 17:54):

Funny, why Jan 1 1980 and not Jan 1 1970?

view this post on Zulip Enrico Tassi (Jun 10 2021 at 17:54):

that would be the zero for unix

view this post on Zulip Théo Zimmermann (Jun 10 2021 at 18:01):

It used to be the latter. I don't know why it changed to the former.


Last updated: Jan 29 2023 at 16:02 UTC