Stream: Nix toolbox devs & users

Topic: 404 for coq archive


view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 14:54):

I'm having trouble with the following command. Any suggestion on what I'm doing wrong (running on a Mac, with no problem using 8.15 and 1.13 with a similar command)?

MacBook-Pro:mech.v pierre$ nix-shell --arg withEmacs true --arg override '{coq = "8.17"; mathcomp = "2.0";}'
warning: Git tree '/Users/pierre/Desktop/ownCloud/Github/pierre/mech.v' is dirty
error: unable to download 'https://github.com/coq/coq/archive/8.17.tar.gz': HTTP error 404 ('')

       response body:

       404: Not Found
(use '--show-trace' to show detailed location information)
MacBook-Pro:mech.v pierre$

view this post on Zulip Ali Caglayan (Jun 06 2023 at 14:58):

Is your nixpkgs too old to have 8.17?

view this post on Zulip Pierre Roux (Jun 06 2023 at 15:00):

I guess mathcomp = "2.0" should be mathcomp = "2.0.0" and maybe coq = "8.17" should be coq = "8.17.0"

view this post on Zulip Ali Caglayan (Jun 06 2023 at 15:07):

That link definitely isn't correct. Weird that there is no validation on your params tho.

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 15:07):

Ali Caglayan said:

Is your nixpkgs too old to have 8.17?

@Ali Caglayan How do I update those?

view this post on Zulip Ali Caglayan (Jun 06 2023 at 15:08):

I don't think that's it actually since the link that is being tried is bogus.

view this post on Zulip Ali Caglayan (Jun 06 2023 at 15:08):

The correct link is https://github.com/coq/coq/archive/refs/tags/V8.17.0.tar.gz

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 15:08):

Pierre Roux said:

I guess mathcomp = "2.0" should be mathcomp = "2.0.0" and maybe coq = "8.17" should be coq = "8.17.0"

Unfortunately, I still get a similar message.... with ".0" added :smile:

view this post on Zulip Ali Caglayan (Jun 06 2023 at 15:09):

Maybe @Théo Zimmermann can understand what needs to be done.

view this post on Zulip Ali Caglayan (Jun 06 2023 at 15:10):

I don't know tbh since I am not too familiar with how the toolbox works

view this post on Zulip Ali Caglayan (Jun 06 2023 at 15:10):

I'm guessing your default.nix is the one generated by the toolbox?

view this post on Zulip Pierre Roux (Jun 06 2023 at 15:11):

Indeed, the correct link is "V8.17.0" (found there: https://github.com/coq/coq/releases)

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 15:17):

Pierre Jouvelot said:

Ali Caglayan said:

Is your nixpkgs too old to have 8.17?

Ali Caglayan How do I update those?

For the record, I found the following command to update the nixpkgs:

nix-channel --update; nix-env --install --attr nixpkgs.nix nixpkgs.cacert

but that doesn't fix the problem, and the same error message occurs.

view this post on Zulip Pierre Roux (Jun 06 2023 at 15:19):

Could you provide your default.nix file so that we could reproduce?

view this post on Zulip Pierre Roux (Jun 06 2023 at 15:24):

Note that I usually don't do override like that on the command line but rather use the toolbox ( https://github.com/coq-community/coq-nix-toolbox ), define bundles in a .nix/config.nix file ( here is the one from mathcomp for instance: https://github.com/math-comp/math-comp/blob/master/.nix/config.nix ) and then just nix-shell --arg withEmacs true --argstr bundle coq-8.17 --argstr job mathcomp-ssreflect (for instance)

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 15:28):

I ran

nix-shell --arg withEmacs true --arg override '{coq = "V8.17.0"; mathcomp = "mathcomp-2.0.0";}'

which asked for export NIXPKGS_ALLOW_BROKEN=1 to be executed (something with elpi broken). Once done, the process ran but failed on

build flags: -j8 -l8 SHELL=/nix/store/vssrny41k0mr33jclrrn67rxhbdpwrr0-bash-5.1-p12/bin/bash revision coq coqide
make: *** No rule to make target 'revision'.  Stop.
error: builder for '/nix/store/aaxvy2rf5liym98h0jh3jlp7imwvzzps-coq-dev.drv' failed with exit code 2
error: build of '/nix/store/a3b2dnybdiqxix8abcrx3g8fsa6gc076-coqdev-algebra-tactics-1.0.0.drv', '/nix/store/aaxvy2rf5liym98h0jh3jlp7imwvzzps-coq-dev.drv', '/nix/store/fv1jgdng9qvch8ca8j54l5vksfp75dij-coqdev-mathcomp-fingroup-dev.drv', '/nix/store/m0nqfilp8yqqmln66s2pxsvpdfd1gpbg-coqdev-mathcomp-algebra-dev.drv' failed

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 15:30):

Pierre Roux said:

Note that I usually don't do override like that on the command line but rather use the toolbox ( https://github.com/coq-community/coq-nix-toolbox ), define bundles in a .nix/config.nix file ( here is the one from mathcomp for instance: https://github.com/math-comp/math-comp/blob/master/.nix/config.nix ) and then just nix-shell --arg withEmacs true --argstr bundle coq-8.17 --argstr job mathcomp-ssreflect (for instance)

Here is my default.nix file:

{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
  update-nixpkgs ? false, ci-matrix ? false,
  override ? {}, ocaml-override ? {}, global-override ? {},
  bundle ? null, job ? null, inNixShell ? null, src ? ./.,
}@args:
let auto = fetchGit {
  url = "https://github.com/coq-community/coq-nix-toolbox.git";
  ref = "master";
  rev = import .nix/coq-nix-toolbox.nix;
};
in
import auto ({inherit src;} // args)

view this post on Zulip Pierre Roux (Jun 06 2023 at 15:43):

With that default.nix, the following command works for me nix-shell --arg withEmacs true --arg override '{coq = "8.17"; mathcomp = "2.0.0";}' so I guess your .nix/coq-nix-toolbox.nix is outdated, mine contains "721d4a5e7a4db115f7576828c354d62a84d7055b" (those are git commit hashes that you can find for instance here: https://github.com/coq-community/coq-nix-toolbox (on top right of file list, below the "Go to file" button for me))

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 15:58):

This one is still failing for me, and my coq-nix-toolbox.nixfile contains "e1aff54cab66816b900f6b1aa29b5b34ce791a6c". I try to update the toolbox, then.

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 15:58):

Is there a recommended way to do that?

view this post on Zulip Pierre Roux (Jun 06 2023 at 16:04):

Just edit the .nix/coq-nix-toolbox.nix file.

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 16:37):

I did just that and ran the command you suggested: nix-shell --arg withEmacs true --arg override '{coq = "8.17"; mathcomp = "2.0.0";}'. This took quite a while to compile many files, but then unfortunately this failed with the following message:

New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
File "./theories/ssrZ.v", line 5, characters 0-74:
Warning:
New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
File "./theories/ssrZ.v", line 44, characters 22-28:
Error: The reference EqType was not found in the current environment.

make[2]: *** [Makefile.coq:830: theories/ssrZ.vo] Error 1
make[2]: *** [theories/ssrZ.vo] Deleting file 'theories/ssrZ.glob'
make[1]: *** [Makefile.coq:409: all] Error 2
make: *** [Makefile:31: invoke-coqmakefile] Error 2
error: builder for '/nix/store/vzjh50nvf6kcbnbymj5pdcpmvv3x7gsi-coq8.17-mathcomp2.0-zify-1.3.0+1.12+8.13.drv' failed with exit code 2
error: 1 dependencies of derivation '/nix/store/xsk2d8vy08nvgyzdzpkw8pr8896x8pi6-coq8.17-algebra-tactics-1.0.0.drv' failed to build

Any suggestion?

view this post on Zulip Pierre Roux (Jun 06 2023 at 16:42):

I didn't compile mathcomp-zify so I did not experienced that issue but indeed mathcomp2.0-zify-1.3.0+1.12+8.13 looks wrong, according to https://github.com/math-comp/mczify/releases one should use version 1.4.0+2.0+8.16, I guess the toolbox needs updating. Meanwhile you can add something like mathcomp-zify = "1.4.0+2.0+8.16" or mathcomp-zify = "master" to your set of overrides.

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 17:04):

Thanks @Pierre Roux. The override with "master" cleared this problem, but a similar problem occurs later on:

File "./theories/ring.v", line 695, characters 0-44:
Warning: The syntax 'Elpi Accumulate File "path"' is deprecated, use 'Elpi
Accumulate File "path" From logpath' [elpi.accumulate-syntax,elpi.deprecated]
File "./theories/ring.v", line 695, characters 0-44:
Error:
File "/private/tmp/nix-build-coq8.17-algebra-tactics-1.0.0.drv-0/source/theories/common.elpi", line 143, column 46, character 5463::
The reference GRing.Ring.zmodType was not found in the current environment.

make[2]: *** [Makefile.coq:830: theories/ring.vo] Error 1
make[2]: *** [theories/ring.vo] Deleting file 'theories/ring.glob'
make[1]: *** [Makefile.coq:409: all] Error 2
make: *** [Makefile:31: invoke-coqmakefile] Error 2
error: builder for '/nix/store/5l21pk0w1qbhz1mpn7yq7wvxvvw1c3m5-coq8.17-algebra-tactics-1.0.0.drv' failed with exit code 2
MacBook-Pro:mech.v pierre$

I tried a similar trick with mathcomp-algebra = "master"; (just guessing), but this failed too. Which part should I override this time?

view this post on Zulip Pierre Roux (Jun 06 2023 at 19:28):

The algebra-tactics overlay for mathcomp2 is not yet merged: https://github.com/math-comp/algebra-tactics/pull/71 you can try mathcomp-algebra-tactics = "proux01:hierarchy-builder" but it might very well be broken.

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 20:07):

Pierre Roux said:

The algebra-tactics overlay for mathcomp2 is not yet merged: https://github.com/math-comp/algebra-tactics/pull/71 you can try mathcomp-algebra-tactics = "proux01:hierarchy-builder" but it might very well be broken.

It seems broken, indeed. I guess I'll stick to the previous version of mathcomp for the time being. Thanks a lot @Pierre Roux

view this post on Zulip Pierre Jouvelot (Jun 06 2023 at 20:25):

Oops! I can go back to mathcomp 1.17 with no problem, but now, with all these manipulations, dune seems to be gone AWOL when I run nix-shell:

MacBook-Pro:mech.v pierre$ nix-shell --arg withEmacs true --arg override '{coq = "8.17"; mathcomp = "1.17";}'
warning: Git tree '/Users/pierre/Desktop/ownCloud/Github/pierre/mech.v' is dirty

[nix-shell:~/Desktop/ownCloud/Github/pierre/mech.v]$ make all
dune build
make: dune: No such file or directory
make: *** [Makefile:8: all] Error 127

How can I add dune back?

view this post on Zulip Pierre Roux (Jun 07 2023 at 06:42):

I would expect mathcomp = "1.17" to be mathcomp = "1.17.0". For dune, no idea as I'm not using it but I guess you should declare it in the dependencies of your package, much like you seem to have mczify and algebra-tactics somewhere in some nix file.

view this post on Zulip Cyril Cohen (Jun 07 2023 at 09:40):

Hi, I skimmed quickly through this conv:

view this post on Zulip Pierre Jouvelot (Jun 07 2023 at 10:22):

Thanks a lot @Cyril Cohen. I'll try to digest all this to make my setting work again.

view this post on Zulip Notification Bot (Jun 07 2023 at 15:08):

Pierre Jouvelot has marked this topic as unresolved.

view this post on Zulip Pierre Jouvelot (Jun 07 2023 at 15:11):

Cyril Cohen said:

Pierre Jouvelot said:

Ali Caglayan said:

yeah that dune error is because make cannot find the dune exec. You need to do what Cyril says and activate dune in the derivation so that nix makes it available for make.

Indeed. All worked fine after a nix-env -i dune. Thanks a lot Ali Caglayan Cyril Cohen Pierre Roux Théo Zimmermann

It's a bit dangerous to mix pure and impure derivations... if it works for you right now I guess it's ok, but it may break unexpectedly in the future and it will definitely not work if you release your development.

Thanks @Cyril Cohen for the heads-up. It's fair to say I'm a bit overwhelmed by the complexity of the installation and update process, but this is working for now, and, with computers, I'm inclined to just not move when things work ;)

view this post on Zulip Ali Caglayan (Jun 07 2023 at 15:24):

Unfortunately the learning curve for Nix is a bit steep, but it flattens out soon :)

view this post on Zulip Pierre Roux (Jun 07 2023 at 15:34):

Pierre Jouvelot said:

this is working for now, and, with computers, I'm inclined to just not move when things work ;)

IIUC, the point of Cyril is that it is working because you locally made nix-env -i dune but should you (or someone else) take your code on another machine, things won't work out of the box (one will have to redo the nix-env command there witout any way to discover that). Writing all those dependencies in the .nix direcory (either in an overlay in .nix/coq-overlays or in a bundle in .nix/config.nix) would fix that.

view this post on Zulip Pierre Jouvelot (Jun 07 2023 at 18:43):

Pierre Roux said:

Pierre Jouvelot said:

this is working for now, and, with computers, I'm inclined to just not move when things work ;)

IIUC, the point of Cyril is that it is working because you locally made nix-env -i dune but should you (or someone else) take your code on another machine, things won't work out of the box (one will have to redo the nix-env command there witout any way to discover that). Writing all those dependencies in the .nix direcory (either in an overlay in .nix/coq-overlays or in a bundle in .nix/config.nix) would fix that.

Yes, I'll try to learn more about how to add the dune dependence in a bundle (it was there before I tried to do all these upgrades that, in one way or another, polluted my settings), since the first person to not discover that is probably going to be me in a couple of weeks :) Thanks @Pierre Roux


Last updated: May 19 2024 at 16:02 UTC