coq: 8.13+beta1 -> 8.13.0 #109479

jarlg · 2021-01-15T21:20:57Z

Motivation for this change

Things done

You can check correctness of the sha with:
nix-prefetch-url --unpack https://github.com/coq/coq/archive/V8.13.0.tar.gz

SuperSandro2000 · 2021-01-15T22:46:17Z

This is a semi-automatic executed nixpkgs-review which does not build all packages (e.g. lumo, tensorflow or pytorch)
If you find some bugs or got suggestions for further things to search or run please reach out to SuperSandro2000 on IRC.

Result of nixpkgs-review pr 109479 run on x86_64-darwin 1

1 package failed to build and are new build failure:

coq_8_13: log was empty

We should probably mark this as broken:

  checkdir error:  cannot create coq-8.13.0/test-suite/misc/deps/+?+?
                   Illegal byte sequence
                   unable to process coq-8.13.0/test-suite/misc/deps/+?+?/.
  checkdir error:  cannot create coq-8.13.0/test-suite/misc/deps/+?+?
                   Illegal byte sequence
                   unable to process coq-8.13.0/test-suite/misc/deps/+?+?/+?+?.v.
  checkdir error:  cannot create coq-8.13.0/test-suite/misc/deps/+?+?
                   Illegal byte sequence
                   unable to process coq-8.13.0/test-suite/misc/deps/+?+?/+?+?.v.
  do not know how to unpack source archive /private/tmp/nix-build-source.drv-0/V8.13.0.zip

SuperSandro2000 · 2021-01-16T10:56:03Z

hash mismatch in fixed-output derivation '/nix/store/qshi58p6j3xy776bzgihms5ngjkmlh2d-source':
  wanted: sha256:1l2c63vskp8kiyxiyi5rpgbmnv67ysn3y4lybd6nj0li5llibifi
  got:    sha256:0sjbqmz6qcvnz0hv87xha80qbhvmmyd675wyc5z4rgr34j2l1ymd
cannot build derivation '/nix/store/a3g6yvxg7fvyyi810jm4ldyzs7qg972b-coq-8.13.0.drv': 1 dependencies couldn't be built
cannot build derivation '/nix/store/9q6pnhkpp7zyyrf4rn49maczxcqapbk3-env.drv': 1 dependencies couldn't be built

vbgl · 2021-01-19T08:01:03Z

Cyril: how to guess the correct hash? IIUC, by reading the code, the src attribute is fetchzip with https://github.com/coq/coq/archive/V8.13.0.zip as url argument. (BTW, the name argument of default-fetcher is never used.) But the hashes returned by nix-prefetch-url and by nix build differ.

Also, what’s wrong with the Greek letters in the file paths?

ping @CohenCyril

SuperSandro2000 · 2021-01-19T11:31:33Z

Also, what’s wrong with the Greek letters in the file paths?

The darwin file system has probably a problem with it. You can skip the tests or mark the package broken on darwin.

You probably need to pass --unpack to nix-prefetch-url

 ➜ nix-prefetch-url https://github.com/coq/coq/archive/V8.13.0.zip
[8.5 MiB DL]
path is '/nix/store/zz3jqwj5kp0samxv3yb48vvg9v3id7w2-V8.13.0.zip'
0v7aw4iq592khdx54jb0jx78fnab45m1lj1rpjj160ycywmlmg9g


 ➜ nix-prefetch-url https://github.com/coq/coq/archive/V8.13.0.zip --unpack
unpacking...
[8.5 MiB DL]
path is '/nix/store/a7h7ym385f3kw62csx2rmy8zghbgmp4b-V8.13.0.zip'
1l2c63vskp8kiyxiyi5rpgbmnv67ysn3y4lybd6nj0li5llibifi

CohenCyril · 2021-01-19T12:30:41Z

Cyril: how to guess the correct hash? IIUC, by reading the code, the src attribute is fetchzip with https://github.com/coq/coq/archive/V8.13.0.zip as url argument. (BTW, the name argument of default-fetcher is never used.) But the hashes returned by nix-prefetch-url and by nix build differ.

I don't understand what is happening, I have the same problem. The weird thing is that I did not have to change any of the previous Coq sha256... (e.g. Coq 8.12.0 sha256 from nix-build and nix-pretech-url are the same) So what's different now?

Also, what’s wrong with the Greek letters in the file paths?

I don't know, I cannot manage to get nix-prefetch-url work for Coq zip's either... I get warning: Pathname cannot be converted from UTF-8 to current locale. Although in principle it should be the same sha as for the tarball...

CohenCyril · 2021-01-19T12:38:58Z

Maybe we are having the same problems as in #107768?

CohenCyril · 2021-01-19T12:46:22Z

I'm totally confused, I downloaded both the zip and the tar.gz, extracted both diff does not show a single difference...

vbgl · 2021-01-31T08:55:09Z

Jarl, can you please fix the hash?

jarlg · 2021-01-31T18:29:34Z

@vbgl Which hash do you want me to change to? The one in the PR is the one nix-prefetch-url --unpack returns. Isn't that as it should be?

My understanding of the comments above is that there's an issue on darwin, which I can't test or do anything about.

CohenCyril · 2021-01-31T18:35:43Z

@GrahamcOfBorg build coq_8_13

CohenCyril · 2021-01-31T18:36:54Z

@vbgl Which hash do you want me to change to? The one in the PR is the one nix-prefetch-url --unpack returns. Isn't that as it should be?

This is the correct hash:

$ nix-prefetch-url --unpack https://github.com/coq/coq/archive/V8.13.0.zip
unpacking...
[8.5 MiB DL]
path is '/nix/store/a7h7ym385f3kw62csx2rmy8zghbgmp4b-V8.13.0.zip'
1l2c63vskp8kiyxiyi5rpgbmnv67ysn3y4lybd6nj0li5llibifi

My understanding of the comments above is that there's an issue on darwin, which I can't test or do anything about.

The issue on darwin is that nix-preferch-url does not work for some zip files... but here the hash is wrong anyway (and I launched GrahamcOfBorg to witness it here.)

jarlg · 2021-01-31T18:54:25Z

@vbgl Which hash do you want me to change to? The one in the PR is the one nix-prefetch-url --unpack returns. Isn't that as it should be?

This is the correct hash:
$ nix-prefetch-url --unpack https://github.com/coq/coq/archive/V8.13.0.zip
unpacking...
[8.5 MiB DL]
path is '/nix/store/a7h7ym385f3kw62csx2rmy8zghbgmp4b-V8.13.0.zip'
1l2c63vskp8kiyxiyi5rpgbmnv67ysn3y4lybd6nj0li5llibifi

Yeah, that's the one used in this PR as well.

My understanding of the comments above is that there's an issue on darwin, which I can't test or do anything about.

The issue on darwin is that nix-preferch-url does not work for some zip files... but here the hash is wrong anyway (and I launched GrahamcOfBorg to witness it here.)

Great! Unfortunately not something I can help with. I'm guessing that when the issues on darwin have been resolved, this PR can simply be merged.

CohenCyril · 2021-01-31T19:29:09Z

@vbgl Which hash do you want me to change to? The one in the PR is the one nix-prefetch-url --unpack returns. Isn't that as it should be?

This is the correct hash:
$ nix-prefetch-url --unpack https://github.com/coq/coq/archive/V8.13.0.zip
unpacking...
[8.5 MiB DL]
path is '/nix/store/a7h7ym385f3kw62csx2rmy8zghbgmp4b-V8.13.0.zip'
1l2c63vskp8kiyxiyi5rpgbmnv67ysn3y4lybd6nj0li5llibifi
Yeah, that's the one used in this PR as well.

My understanding of the comments above is that there's an issue on darwin, which I can't test or do anything about.

The issue on darwin is that nix-preferch-url does not work for some zip files... but here the hash is wrong anyway (and I launched GrahamcOfBorg to witness it here.)

Great! Unfortunately not something I can help with. I'm guessing that when the issues on darwin have been resolved, this PR can simply be merged.

No we cannot merge have a look at this please: the CI fails on this PR.
Sorry I got confused (again!) I cannot wrap my head around this problem...
The correct hash seems to be 0sjbqmz6qcvnz0hv87xha80qbhvmmyd675wyc5z4rgr34j2l1ymd...

There is a discrepancy between the output of nix-prefetch-url and the behaviour of fetchzip:

$ nix-build -E '(import <nixpkgs> {}).fetchzip {url = "https://github.com/coq/coq/archive/V8.13.0.zip"; sha256="1l2c63vskp8kiyxiyi5rpgbmnv67ysn3y4lybd6nj0li5llibifi"; }'

EDIT: Now I narrowed it down, I will submit an issue...

jarlg · 2021-01-31T20:36:40Z

Thanks for the clarification, @CohenCyril! I tried the corrected hash and everything seems to work fine on my side. Hopefully the CI agrees. (Now I'm wondering, why did my previous hash work?)

vbgl · 2021-01-31T20:41:47Z

Now I'm wondering, why did my previous hash work?

When there is already a path in the store with the expected hash, nix is lazy and won’t try to build it again.

SuperSandro2000 · 2021-01-31T23:51:47Z

@ofborg eval

CohenCyril · 2021-02-01T00:03:13Z

@GrahamcOfBorg build coqPackages_8_13

SuperSandro2000 · 2021-02-01T07:37:49Z

This is a semi-automatic executed nixpkgs-review with nixpkgs-review-checks extension. It is checked by a human on a best effort basis and does not build all packages (e.g. lumo, tensorflow or pytorch).
If you have any questions or problems please reach out to SuperSandro2000 on IRC.

Result of nixpkgs-review pr 109479 run on x86_64-linux 1

1 package built:

coq_8_13

The following issues got detected with the above build packages.
Please fix at least the ones listed with your changed packages:

coq_8_13:

Please consider this feature to be alpha.

A substituteInPlace with an unmatched pattern got detected:

substituteStream(): WARNING: pattern '/bin/uname' doesn't match anything in file 'configure'
substituteStream(): WARNING: pattern '"md5 -q"' doesn't match anything in file 'configure.ml'

Please check the offending substituteInPlace for typos or changes in source.
When evaluating attribute ‘coq_8_13’:
warning: unclear-gpl
lgpl21 is a deprecated license, check if project uses lgpl21Plus or lgpl21Only and change meta.license accordingly.

Near pkgs/applications/science/logic/coq/default.nix:179:5:

    |
179 |     license = licenses.lgpl21;
    |     ^

See: https://github.com/jtojnar/nixpkgs-hammering/blob/master/explanations/unclear-gpl.md

SuperSandro2000 · 2021-02-01T07:42:15Z

This is a semi-automatic executed nixpkgs-review with nixpkgs-review-checks extension. It is checked by a human on a best effort basis and does not build all packages (e.g. lumo, tensorflow or pytorch).
If you have any questions or problems please reach out to SuperSandro2000 on IRC.

Result of nixpkgs-review pr 109479 run on x86_64-darwin 1

1 package failed to build and are new build failure:

coq_8_13: log was empty

coq: 8.13+beta1 -> 8.13.0

42233da

ofborg bot requested review from thoughtpolice, roconnor, vbgl and Zimmi48 January 15, 2021 21:34

ofborg bot added 10.rebuild-darwin: 1-10 10.rebuild-darwin: 1 10.rebuild-linux: 1-10 10.rebuild-linux: 1 labels Jan 15, 2021

thoughtpolice approved these changes Jan 16, 2021

View reviewed changes

coq: 8.13+beta1 -> 8.13.0 (corrected hash)

9e1b82b

CohenCyril mentioned this pull request Jan 31, 2021

The nix-prefetch-url --unpack command and fetchzip derivation do not agree on the sha256 #111508

Open

ofborg bot requested a review from thoughtpolice February 1, 2021 00:01

CohenCyril mentioned this pull request Feb 1, 2021

The nix-prefetch-url --unpack command and fetchzip derivation do not agree on the sha256 NixOS/nix#4499

Open

vbgl merged commit 813d14b into NixOS:master Feb 3, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

coq: 8.13+beta1 -> 8.13.0 #109479

coq: 8.13+beta1 -> 8.13.0 #109479

jarlg commented Jan 15, 2021

SuperSandro2000 commented Jan 15, 2021

SuperSandro2000 commented Jan 16, 2021

vbgl commented Jan 19, 2021

SuperSandro2000 commented Jan 19, 2021 •

edited

CohenCyril commented Jan 19, 2021 •

edited

CohenCyril commented Jan 19, 2021

CohenCyril commented Jan 19, 2021

vbgl commented Jan 31, 2021

jarlg commented Jan 31, 2021

CohenCyril commented Jan 31, 2021

CohenCyril commented Jan 31, 2021 •

edited

jarlg commented Jan 31, 2021

CohenCyril commented Jan 31, 2021 •

edited

jarlg commented Jan 31, 2021

vbgl commented Jan 31, 2021

SuperSandro2000 commented Jan 31, 2021

CohenCyril commented Feb 1, 2021

SuperSandro2000 commented Feb 1, 2021

SuperSandro2000 commented Feb 1, 2021

coq: 8.13+beta1 -> 8.13.0 #109479

coq: 8.13+beta1 -> 8.13.0 #109479

Conversation

jarlg commented Jan 15, 2021

Motivation for this change

Things done

SuperSandro2000 commented Jan 15, 2021

SuperSandro2000 commented Jan 16, 2021

vbgl commented Jan 19, 2021

SuperSandro2000 commented Jan 19, 2021 • edited

CohenCyril commented Jan 19, 2021 • edited

CohenCyril commented Jan 19, 2021

CohenCyril commented Jan 19, 2021

vbgl commented Jan 31, 2021

jarlg commented Jan 31, 2021

CohenCyril commented Jan 31, 2021

CohenCyril commented Jan 31, 2021 • edited

jarlg commented Jan 31, 2021

CohenCyril commented Jan 31, 2021 • edited

jarlg commented Jan 31, 2021

vbgl commented Jan 31, 2021

SuperSandro2000 commented Jan 31, 2021

CohenCyril commented Feb 1, 2021

SuperSandro2000 commented Feb 1, 2021

SuperSandro2000 commented Feb 1, 2021

SuperSandro2000 commented Jan 19, 2021 •

edited

CohenCyril commented Jan 19, 2021 •

edited

CohenCyril commented Jan 31, 2021 •

edited

CohenCyril commented Jan 31, 2021 •

edited