Pierre Jouvelot (Jun 06 2023 at 14:54): 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$
Is your nixpkgs too old to have 8.17?
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"
Ali Caglayan (Jun 06 2023 at 15:07):That link definitely isn't correct. Weird that there is no validation on your params tho.
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?
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.
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
Pierre Jouvelot (Jun 06 2023 at 15:08):Pierre Roux said:
I guess
mathcomp = "2.0"should bemathcomp = "2.0.0"and maybecoq = "8.17"should becoq = "8.17.0"
Unfortunately, I still get a similar message.... with ".0" added :smile:
Ali Caglayan (Jun 06 2023 at 15:09):Maybe @Théo Zimmermann can understand what needs to be done.
Ali Caglayan (Jun 06 2023 at 15:10):I don't know tbh since I am not too familiar with how the toolbox works
Ali Caglayan (Jun 06 2023 at 15:10):I'm guessing your default.nix is the one generated by the toolbox?
Pierre Roux (Jun 06 2023 at 15:11):Indeed, the correct link is "V8.17.0" (found there: https://github.com/coq/coq/releases)
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.
Pierre Roux (Jun 06 2023 at 15:19):Could you provide your default.nix file so that we could reproduce?
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)
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
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.nixfile ( here is the one from mathcomp for instance: https://github.com/math-comp/math-comp/blob/master/.nix/config.nix ) and then justnix-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)
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))
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.
Pierre Jouvelot (Jun 06 2023 at 15:58):Is there a recommended way to do that?
Pierre Roux (Jun 06 2023 at 16:04):Just edit the .nix/coq-nix-toolbox.nix file.
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?
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.
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?
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.
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
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?
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.
Cyril Cohen (Jun 07 2023 at 09:40):Hi, I skimmed quickly through this conv:
nix-channel's job to update but updateNixToolBox instead (or updateNixpkgs variants to overload the version of nixpkgs at use)8.17 indead of 8.17.0 and 2.0 instead of 2.0.0 for known revision should still work even though not recommended (there is a tentative of finding the latest release associated to it :sweat_smile: )nix-shell command, but the addition of a dedicated bundle in config.nix.dune in your derivation. 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.
Notification Bot (Jun 07 2023 at 15:08):Pierre Jouvelot has marked this topic as unresolved.
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 ZimmermannIt'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 ;)
Ali Caglayan (Jun 07 2023 at 15:24):Unfortunately the learning curve for Nix is a bit steep, but it flattens out soon :)
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.
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 dunebut should you (or someone else) take your code on another machine, things won't work out of the box (one will have to redo thenix-envcommand there witout any way to discover that). Writing all those dependencies in the.nixdirecory (either in an overlay in.nix/coq-overlaysor 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: Oct 08 2024 at 14:01 UTC