coq_8_14: init at 8.14+rc1 #138274

Zimmi48 · 2021-09-17T13:01:39Z

Motivation for this change

Coq 8.14+rc1 was just tagged.

Things done

Currently testing this, but I expect this will work given that the Coq derivation has been 8.14-ready for a while now.

Zimmi48 · 2021-09-17T13:15:57Z

coq_8_14 does build fine on my machine. I'm currently testing at https://github.com/coq-community/coq-nix-toolbox/actions/runs/1245604615 if there are packages in the already quite large coqPackages_8_14 set that are not actually buildable.

vbgl · 2021-09-17T13:33:36Z

Build failure (is which missing from the nativeBuildInputs?):

dev/tools/make_git_revision.sh: line 3: which: command not found

Also coqPackages_8_14.addition-chains fails to evaluate; suggested patch:

--- a/pkgs/development/coq-modules/addition-chains/default.nix
+++ b/pkgs/development/coq-modules/addition-chains/default.nix
@@ -11,7 +11,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.11"; out = "0.4"; }
+    { case = range "8.11" "8.13"; out = "0.4"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-algebra paramcoq ];

pkgs/development/coq-modules/bignums/default.nix

Zimmi48 · 2021-09-17T13:55:14Z

Is the problem really that which is missing (I think this is just a warning) or this line: Error: no rule to make target bin/votour (or missing .PHONY)? How come it didn't fail when I built it on my side?

vbgl · 2021-09-17T14:22:24Z

Indeed, the bin/votour missing target seems to be the actual error. How does it only happen on CI?

BTW, Cheerios, Verdi, CoqEAL still fail to evaluate.

Zimmi48 · 2021-09-17T14:29:30Z

dev/tools/make_git_revision.sh: line 3: which: command not found can indeed also been seen in the log of the successful build at: https://github.com/coq-community/coq-nix-toolbox/pull/65/checks?check_run_id=3632607063. For some reason, in this case this is a different derivation that is built. However, on my system, I have checked that the derivation that I've built is the same as the one that has failed in CI here. So, that's strange indeed.

Zimmi48 · 2021-09-17T14:30:11Z

I also got this line in the log linked above: make[1]: 'bin/votour' is up to date.

Zimmi48 · 2021-09-17T14:50:30Z

It's a bit annoying to have to manually tweak the defaultVersion computation of packages just because they have dependencies that are marked as broken (even if they might actually work fine with Coq 8.14 if we update the dependency). Would it be possible to automatically mark as broken the reverse dependencies of a broken package?

vbgl · 2021-09-17T14:55:10Z

You may leave out the evaluation failures for now and just be sure that they get fixed before 8.14.0 gets in nixpkgs.

Zimmi48 · 2021-09-17T15:21:47Z

Yes, but I also want CI on the coq-nix-toolbox repo to pass fully, so I'll fix all the evaluation failures.

Zimmi48 · 2021-09-19T14:03:46Z

IIUC the only blocking thing to merge this PR would be to understand the CI failure, but despite the failure being reproducible on ofborg runs, it is truly incomprehensible since it never occurred while building locally or on the coq-nix-toolbox CI (and I have checked that the derivations being built are the same). Are there some known outside parameters that can influence how a derivation is built? I believe that my initial build was sandboxed as it ran on my NixOS machine.

SkySkimmer · 2021-09-22T19:26:18Z

https://github.com/NixOS/nixpkgs/blob/2131f28314d353e326eea14dd8523a4befb34316/pkgs/applications/science/logic/coq/default.nix#L165 bin/votour is not a target since the switch to dune

Zimmi48 · 2021-09-22T19:34:50Z

Thanks for your suggestion. I will make it conditional. But I still fail to understand why the same version was building fine elsewhere.

Zimmi48 · 2021-09-22T19:38:32Z

Rebuilding coq_8_14 after this change did not trigger a new build on my machine, which seems to indicate that the derivation which was build was already ignoring this target (or the buildFlags entirely).

Nah, that was my conditional which was backwards.

vbgl · 2021-09-28T06:11:35Z

Oh, nice. I did not notice that you had fixed it.

Zimmi48 · 2021-09-28T07:51:28Z

That's new from yesterday 😉

FTR, here is the current structure of result:

bin/
lib/coq/theories
lib/coq/user-contribs
lib/coq-core/META (and OCaml libs)
lib/coqide/META
lib/coqide-server/META (and OCaml libs)
lib/ocaml/4.10.2/site-lib/coq-core (symbolic link to lib/coq-core)
lib/stublibs
nix-support
share/applications
share/coq
share/doc (with just LICENSE and README files under coq-core, etc.)
share/man/man1
share/pixmaps
share/texmf/tex/latex/misc

Do you see anything to fix? From my side, all I noticed is that there should probably also be a symlink from lib/ocaml/4.10.2/site-lib/coqide-server to lib/coqide-server.

Zimmi48 · 2021-09-28T08:15:20Z

From my side, all I noticed is that there should probably also be a symlink from lib/ocaml/4.10.2/site-lib/coqide-server to lib/coqide-server.

Now fixed.

Zimmi48 · 2021-09-28T12:40:20Z

Something has been broken with the darwin build for a while, although previously in a different way.
eg https://github.com/NixOS/nixpkgs/runs/1959980556 (coq_8_13: 8.13.0 → 8.13.1) has no log just "This check concluded as stale."

It seems that this happens because ofborg will sometimes never run these Darwin tests. And this seems to be happening again now.

Zimmi48 · 2021-09-28T12:44:41Z

FTR I did some tests on macOS via the Coq Nix Toolbox CI, and there doesn't seem to be any issue building Coq. Could there be again some discrepancy between how CI behaves when run by ofborg or in the GitHub Actions from the Coq Nix Toolbox? Hard to tell if the CI here doesn't complete.

Zimmi48 · 2021-09-30T18:33:09Z

The ofborg CI tests on darwin have finally run, and they have completed with a failure. Meanwhile, the same tests ran in the GitHub Actions CI of the Coq Nix Toolbox and have completed successfully.

Once again, building the same derivation was attempted in both cases:

/nix/store/sq9wmdfqyppqbhzfrhqv1sc7i03a8f1q-coq-8.14+rc1.drv

The failure in ofborg tests is deterministic, it is always:

trying https://github.com/coq/coq/archive/V8.14+rc1.zip
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100   117  100   117    0     0    609      0 --:--:-- --:--:-- --:--:--   609
100 8749k    0 8749k    0     0  5208k      0 --:--:--  0:00:01 --:--:-- 9053k
unpacking source archive /private/tmp/nix-build-source.drv-0/V8.14+rc1.zip
checkdir error:  cannot create coq-8.14-rc1/test-suite/misc/deps/+?+?
                 Illegal byte sequence
                 unable to process coq-8.14-rc1/test-suite/misc/deps/+?+?/.
checkdir error:  cannot create coq-8.14-rc1/test-suite/misc/deps/+?+?
                 Illegal byte sequence
                 unable to process coq-8.14-rc1/test-suite/misc/deps/+?+?/+?+?.v.
checkdir error:  cannot create coq-8.14-rc1/test-suite/misc/deps/+?+?
                 Illegal byte sequence
                 unable to process coq-8.14-rc1/test-suite/misc/deps/+?+?/+?+?.v.
do not know how to unpack source archive /private/tmp/nix-build-source.drv-0/V8.14+rc1.zip
builder for '/nix/store/p66rcxr6g0q9sn57spbgmn4qq7vsn95d-source.drv' failed with exit code 1

Similarly, the failure we were getting on Linux before fixing the build targets was also deterministic (and was not observed in the GitHub Actions CI of the Coq Nix Toolbox, despite the two buildings the same derivation).

I'm quite annoyed by this discrepancy, which is not supposed to happen with Nix. Could the explanation be that the two use a different version of Nix? The Coq Nix Toolbox CI uses Nix 2.3.15, but I don't know how to tell which version the ofborg CI uses.

Zimmi48 · 2021-09-30T18:38:36Z

cc @grahamc in case you are able to help with this (see comment just above)

Zimmi48 · 2021-10-01T19:17:11Z

So, it's actually not a Nix version problem. I have been able to reproduce the problem observed here in the GitHub Actions CI with Nix 2.3.15. See https://github.com/Zimmi48/coq-nix-toolbox/runs/3771003867?check_suite_focus=true (not explicitly pinned) and https://github.com/Zimmi48/coq-nix-toolbox/runs/3770951230?check_suite_focus=true (explicitly pinned).
Now, what I don't understand is what is the difference that made /nix/store/sq9wmdfqyppqbhzfrhqv1sc7i03a8f1q-coq-8.14+rc1.drv build successfully in https://github.com/coq-community/coq-nix-toolbox/runs/3730072982?check_suite_focus=true but consistently fail in other runs (like the two linked above).

Zimmi48 · 2021-10-04T09:49:37Z

Now, what I don't understand is what is the difference that made /nix/store/sq9wmdfqyppqbhzfrhqv1sc7i03a8f1q-coq-8.14+rc1.drv build successfully in https://github.com/coq-community/coq-nix-toolbox/runs/3730072982?check_suite_focus=true but consistently fail in other runs (like the two linked above).

I'm thinking the explanation might simply be that the archive to download is the same on Linux and Darwin. So it suffices that the archive has already been downloaded on Linux and cached in NixOS official cache (or some Cachix) to make it available to derivations building Coq on Darwin. If that's the case, then it alleviates the problem for users (and explains that it wasn't noticed when running CI with the coq-community Cachix, which already contained the derivation output on Linux).

Does that make sense?

In any case, this issue does not seem to be a regression from 8.14 but rather a problem that was introduced with the switch from fetchTarball to fetchzip in #105877. We should discuss how to resolve it independently of this PR which has been delayed for too long already.

@vbgl Do you agree?

vbgl

The multinomials library at version 1.5.4 is compatible with Coq 8.14.

pkgs/development/coq-modules/coqeal/default.nix

vbgl · 2021-10-12T06:18:51Z

pkgs/development/coq-modules/interval/default.nix

-    { case = range "8.8" "8.12"; out = "4.0.0"; }
-    { case = range "8.7" "8.11"; out = "3.4.2"; }
+    { case = range "8.8" "8.13"; out = "4.3.0"; }
+    { case = isEq  "8.7";        out = "3.4.2"; }
    { case = range "8.5" "8.6";  out = "3.3.0"; }
  ] null;


Please drop this change from this PR (unrelated and arguably wrong).

The entire change to this file or the second line? If that's the second line, then I can certainly revert that but my point for doing this kind of change was that defaultVersion is not about providing "correct" version constraints but about having a way to decide which version to use based on the version of Coq and having overlapping ranges is not helpful in this respect (it rather makes the code less clear). (Similarly for the removed case that was just never reached.)

I meant the entire set of changes made to this file.

As your reply suggests, it is worth discussion and unrelated to Coq 8.14.

Indeed, interval builds fine with Coq 8.14. I dropped the changes to this file.

Zimmi48 · 2021-10-13T07:09:23Z

@vbgl anything else?

Zimmi48 · 2021-10-14T12:12:36Z

With Cyril, we've discussed that we should report the issues with non-reproducibility of derivation building that we've encountered while preparing this PR (the bin/votour issue and the macOS-specific failure to download the source tarball) but I don't know when I'll find sufficient time to sit down and write a proper report for this. Probably not for a while.

ofborg bot added the 8.has: package (new) This PR adds a new package label Sep 17, 2021

ofborg bot requested review from roconnor, vbgl and thoughtpolice September 17, 2021 13:14

ofborg bot added 11.by: package-maintainer This PR was created by the maintainer of the package it changes 10.rebuild-darwin: 1-10 10.rebuild-darwin: 1 10.rebuild-linux: 1-10 10.rebuild-linux: 1 labels Sep 17, 2021

Zimmi48 force-pushed the coq-8-14 branch from 1e39a6d to 2f46049 Compare September 17, 2021 13:52

vbgl reviewed Sep 17, 2021

View reviewed changes

pkgs/development/coq-modules/bignums/default.nix Outdated Show resolved Hide resolved

Zimmi48 force-pushed the coq-8-14 branch from 2f46049 to 159ea6f Compare September 17, 2021 13:58

ofborg bot requested a review from vbgl September 17, 2021 14:11

Zimmi48 force-pushed the coq-8-14 branch 2 times, most recently from 4753333 to dbce3f9 Compare September 17, 2021 14:48

Zimmi48 force-pushed the coq-8-14 branch from dbce3f9 to 2131f28 Compare September 17, 2021 15:34

ofborg bot requested a review from jwiegley September 22, 2021 19:50

Zimmi48 force-pushed the coq-8-14 branch from e7decda to a948544 Compare September 28, 2021 07:43

Zimmi48 force-pushed the coq-8-14 branch from a948544 to c2b1fdb Compare September 28, 2021 08:15

Zimmi48 mentioned this pull request Oct 1, 2021

Testing with Nix 2.2. cachix/install-nix-action#99

Closed

Zimmi48 force-pushed the coq-8-14 branch from c2b1fdb to 624f1e3 Compare October 4, 2021 09:43

Zimmi48 force-pushed the coq-8-14 branch from 624f1e3 to ee3dfe0 Compare October 11, 2021 13:42

Zimmi48 mentioned this pull request Oct 11, 2021

coqPackages: filter packages depending on filtered packages #141260

Closed

12 tasks

Zimmi48 force-pushed the coq-8-14 branch from ee3dfe0 to 9bf8298 Compare October 11, 2021 15:07

vbgl reviewed Oct 11, 2021

View reviewed changes

pkgs/development/coq-modules/coqeal/default.nix Outdated Show resolved Hide resolved

Zimmi48 force-pushed the coq-8-14 branch from 9bf8298 to d9df775 Compare October 11, 2021 17:05

ofborg bot requested a review from vbgl October 11, 2021 17:18

vbgl reviewed Oct 12, 2021

View reviewed changes

Zimmi48 added 2 commits October 12, 2021 11:30

coq_8_14: init at 8.14+rc1

baa7d5b

coqPackages_8_14.serapi: init at 8.14+rc1+0.14.0

95bab0c

Zimmi48 force-pushed the coq-8-14 branch from d9df775 to 95bab0c Compare October 12, 2021 09:30

ofborg bot requested a review from vbgl October 12, 2021 09:44

vbgl merged commit e7735f2 into NixOS:master Oct 13, 2021

Zimmi48 deleted the coq-8-14 branch October 13, 2021 18:44

Zimmi48 mentioned this pull request Mar 2, 2022

fetchzip does not work correctly with unicode file names #118612

Closed

Zimmi48 mentioned this pull request Jun 4, 2022

coq.src can't be built on darwin (UTF-8 file names?) #176225

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

coq_8_14: init at 8.14+rc1 #138274

coq_8_14: init at 8.14+rc1 #138274

Zimmi48 commented Sep 17, 2021 •

edited

Loading

Zimmi48 commented Sep 17, 2021

vbgl commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

vbgl commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

vbgl commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

Zimmi48 commented Sep 19, 2021

SkySkimmer commented Sep 22, 2021

Zimmi48 commented Sep 22, 2021

Zimmi48 commented Sep 22, 2021 •

edited

Loading

vbgl commented Sep 28, 2021

Zimmi48 commented Sep 28, 2021

Zimmi48 commented Sep 28, 2021

Zimmi48 commented Sep 28, 2021

Zimmi48 commented Sep 28, 2021

Zimmi48 commented Sep 30, 2021 •

edited

Loading

Zimmi48 commented Sep 30, 2021

Zimmi48 commented Oct 1, 2021

Zimmi48 commented Oct 4, 2021

vbgl left a comment

vbgl Oct 12, 2021

Zimmi48 Oct 12, 2021 •

edited

Loading

vbgl Oct 12, 2021 •

edited

Loading

Zimmi48 Oct 12, 2021

Zimmi48 commented Oct 13, 2021

Zimmi48 commented Oct 14, 2021

coq_8_14: init at 8.14+rc1 #138274

coq_8_14: init at 8.14+rc1 #138274

Conversation

Zimmi48 commented Sep 17, 2021 • edited Loading

Motivation for this change

Things done

Zimmi48 commented Sep 17, 2021

vbgl commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

vbgl commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

vbgl commented Sep 17, 2021

Zimmi48 commented Sep 17, 2021

Zimmi48 commented Sep 19, 2021

SkySkimmer commented Sep 22, 2021

Zimmi48 commented Sep 22, 2021

Zimmi48 commented Sep 22, 2021 • edited Loading

vbgl commented Sep 28, 2021

Zimmi48 commented Sep 28, 2021

Zimmi48 commented Sep 28, 2021

Zimmi48 commented Sep 28, 2021

Zimmi48 commented Sep 28, 2021

Zimmi48 commented Sep 30, 2021 • edited Loading

Zimmi48 commented Sep 30, 2021

Zimmi48 commented Oct 1, 2021

Zimmi48 commented Oct 4, 2021

vbgl left a comment

Choose a reason for hiding this comment

vbgl Oct 12, 2021

Choose a reason for hiding this comment

Zimmi48 Oct 12, 2021 • edited Loading

Choose a reason for hiding this comment

vbgl Oct 12, 2021 • edited Loading

Choose a reason for hiding this comment

Zimmi48 Oct 12, 2021

Choose a reason for hiding this comment

Zimmi48 commented Oct 13, 2021

Zimmi48 commented Oct 14, 2021

Zimmi48 commented Sep 17, 2021 •

edited

Loading

Zimmi48 commented Sep 22, 2021 •

edited

Loading

Zimmi48 commented Sep 30, 2021 •

edited

Loading

Zimmi48 Oct 12, 2021 •

edited

Loading

vbgl Oct 12, 2021 •

edited

Loading