Christian Doczkal (Jun 07 2021 at 12:35): 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?
Théo Zimmermann (Jun 07 2021 at 12:40):Hi @Christian Doczkal, I can help / guide you through this process.
Christian Doczkal (Jun 07 2021 at 14:54):@Théo Zimmermann Sorry, I was called away. So where do I start?
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.
Théo Zimmermann (Jun 07 2021 at 14:55):In particular, follow the Standalone instructions since you already have Nix.
Théo Zimmermann (Jun 07 2021 at 14:56):Is this repository a new thing or some existing package?
Christian Doczkal (Jun 07 2021 at 14:56):I'm talking about a PR for mathcomp with an overlay for fourcolor
Théo Zimmermann (Jun 07 2021 at 14:57):Oh OK, I misunderstood then :smile:
Théo Zimmermann (Jun 07 2021 at 14:57):Let me reboot (figuratively).
Christian Doczkal (Jun 07 2021 at 14:57):Well, my initial messages was (purposefully) more generic than that, but possibly too generic nonetheless.
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.
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.
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.
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
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
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.
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.
Cyril Cohen (Jun 07 2021 at 15:11):I'm a bit lost: you want to build which project with which versions of what?
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.
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
Cyril Cohen (Jun 07 2021 at 15:13):That's why I'm asking
Christian Doczkal (Jun 07 2021 at 15:14):I am trying to build coq-fourcolor against a PR for mathcomp. ^^
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) ?
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.
Cyril Cohen (Jun 07 2021 at 15:17):ok
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?
Théo Zimmermann (Jun 07 2021 at 15:17):OK, for this time, it works.
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
Cyril Cohen (Jun 07 2021 at 15:23):I will soon merge math-comp/fourcolor#33, but you could already use it
Christian Doczkal (Jun 07 2021 at 15:23):I wasn't aware that you also need to install the toolbox in the reverse dependencies.
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
Cyril Cohen (Jun 07 2021 at 15:25):It's not necessary, but it's sufficient
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.
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
Théo Zimmermann (Jun 07 2021 at 15:30):You're talking of the one on the four-color side, right?
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?
Théo Zimmermann (Jun 07 2021 at 15:31):No need.
Théo Zimmermann (Jun 07 2021 at 15:31):I think Cyril was talking of the four-color repo.
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";}'
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
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"
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?
Théo Zimmermann (Jun 07 2021 at 15:34):You do not need to update the PR on the mathcomp side AFAICT.
Cyril Cohen (Jun 07 2021 at 15:35):and you do not need to wait for the CI to finish either
Christian Doczkal (Jun 07 2021 at 15:35):bit how does #yourPR do the right thing, if the PR with that number does not ...
Cyril Cohen (Jun 07 2021 at 15:36):yes, the overloading instruction does not depend on the toolbox being installed in the dependencies
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.
Théo Zimmermann (Jun 07 2021 at 15:37):(Although it is also supported to point to a local version.)
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 ;)
Théo Zimmermann (Jun 07 2021 at 15:38):That's fine with me.
Cyril Cohen (Jun 07 2021 at 15:39):I'm lost
Théo Zimmermann (Jun 07 2021 at 15:39):With respect to what?
Cyril Cohen (Jun 07 2021 at 15:40):as to why @Christian Doczkal could not use math-comp/fourcolor#33 right now
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.
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...
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 :)
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. ^^
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.
Cyril Cohen (Jun 08 2021 at 10:36):Yep, github looks fishy right now, maybe it's being hacked
Théo Zimmermann (Jun 08 2021 at 10:40):That's not the only thing that looks down. cache.nixos.org too
Cyril Cohen (Jun 08 2021 at 10:41):oO
Cyril Cohen (Jun 08 2021 at 10:41):not on my side...
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"
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
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
Théo Zimmermann (Jun 08 2021 at 10:49):I've also got a GitLab pipeline failing to reach deb.debian.org!
Théo Zimmermann (Jun 08 2021 at 10:50):https://www.dailysabah.com/world/global-news-websites-down-amid-internet-outage/news
Cyril Cohen (Jun 08 2021 at 12:35):@Christian Doczkal did you have the opportunity to try?
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:
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.
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.
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
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.
Théo Zimmermann (Jun 10 2021 at 15:55):But in future versions of Coq, this info is removed anyway.
Enrico Tassi (Jun 10 2021 at 17:54):Funny, why Jan 1 1980 and not Jan 1 1970?
Enrico Tassi (Jun 10 2021 at 17:54):that would be the zero for unix
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: Oct 08 2024 at 15:02 UTC