num is a dependency for Nix CI about aac-tactics HOT 16 CLOSED

The mystery thickens: I just tested on the v8.12 branch, and it turns out num is not a necessary Nix dependency there.

from aac-tactics.

@Zimmi48 so the change was introduced between 8.12+beta1 and 8.12.0? Then it makes sense that I couldn't trigger it with Nix here, since apparently, 8.12 for Nix was then equal to 8.12+beta1, see this Travis job.

from aac-tactics.

Ah OK, since you said v8.12 I thought you meant the v8.12 branch.

This was my mistake, since I didn't keep track of whether the Nix CI had 8.12 or https://github.com/coq/coq-on-cachix/tarball/v8.12.

from aac-tactics.

I thought the fix would be as simple as adding num in default.nix to read:

buildInputs = with coq.ocamlPackages; [ ocaml findlib num ]

... but this results in every Nix CI run building Coq and everything else from scratch, which takes 20+ minutes.

from aac-tactics.

Your fix is probably unrelated to the rebuilding of Coq. Looking at a failed log, I can see "warning: ignoring untrusted substituter" at the top. This is an independent issue that is likely to show up in other projects as well...

from aac-tactics.

@Zimmi48 so for precision, I did the right thing with num? And we should have this also in our default.nix.mustache template?

from aac-tactics.

Yes, but I'm wondering why the need for num appeared only recently. It could indeed make sense to add it to the template if other plugins are likely to have the same issue.

Regarding the binary cache issue, looking at the build history, this is likely related to the fact that the version of Nix is not pinned in .travis.yml (contrary to the template): therefore, the Nix build started failing a month ago, then fixed itself when the default version was bumped in Travis recently, but this also triggered this issue and the 30-minute (instead of 3-minute) builds.

from aac-tactics.

Hum no, actually, here is another build failing to use the binary cache despite the pinned Nix version: https://travis-ci.com/github/coq-community/HighSchoolGeometry/jobs/358107996

from aac-tactics.

@palmskog We need to copy these three lines for the Cachix substitution to work again:

https://github.com/nix-community/nur-packages-template/blob/a16929a6f9e2134b2488c82a4abaa4b5b37dba95/.travis.yml#L32-L34

Would you mind testing this in your branch before we apply it to the templates?

from aac-tactics.

Works fine for me after adding the three lines, see https://travis-ci.com/github/coq-community/aac-tactics/jobs/360377680

from aac-tactics.

I'm still puzzled by the sudden need for num though. From what I can see in the dune file contained in the src directory, num shouldn't even be a direct dependency. Furthermore, we reuse the ocamlPackages from Coq and nothing changed in the master branch regarding this between June 27th and June 30th, when this started to fail because with this error. It may be something that was changed in nixpkgs but I'm not sure exactly what (and the commit log is hard to browse). Maybe @vbgl would know more.

from aac-tactics.

The mystery thickens: I just tested on the v8.12 branch, and it turns out num is not a necessary Nix dependency there.

Was your v8.12 branch up-to-date? When updating the Coq version from 8.12+beta1 to 8.12.0 in nixpkgs, the addition of the num dependency to several plugins was required. @vbgl traced back the change to coq/coq#12604.

from aac-tactics.

Ah OK, since you said v8.12 I thought you meant the v8.12 branch.

from aac-tactics.

An explicit dependency on num is no longer needed. I've removed it from the default.nix in the master branch.

from aac-tactics.

@Zimmi48 but it will still be needed for 8.12, right?

from aac-tactics.

No, this fix was also applied in NixOS/nixpkgs#94230 which bumped the nixpkgs version from 8.12+beta1 to 8.12.0, and it will be backported to v8.12 so that people testing on https://github.com/coq/coq-on-cachix/tarball/v8.12 instead of "8.12" from nixpkgs can benefit from it as well.

from aac-tactics.