Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

coqPackages.ssreflect: refactor choice of source version #49780

Merged
merged 3 commits into from
Nov 6, 2018
Merged

coqPackages.ssreflect: refactor choice of source version #49780

merged 3 commits into from
Nov 6, 2018
+32 −66

Conversation

Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Nov 5, 2018 •
edited
Loading

Motivation for this change

Define a default version for SSReflect package.

Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS)
  • Built on platform(s)
    • NixOS
    • macOS
    • other Linux distributions
  • Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Determined the impact on package closure size (by running nix path-info -S before and after)
  • Fits CONTRIBUTING.md.

Sorry, something went wrong.

@Zimmi48 Zimmi48 mentioned this pull request Nov 5, 2018
Merged
@Zimmi48
Copy link
Member Author

Zimmi48 commented Nov 5, 2018

Thanks @Mic92, I wrote this too fast.

Mic92
Mic92 reviewed Nov 5, 2018
View reviewed changes
pkgs/development/coq-modules/mathcomp/default.nix

};
param = params."${coq.coq-version}";
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

param is still beeing used in line 22.

Copy link
Member

@Mic92 Mic92 Nov 5, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Although it should use fetchFromGitHub instead of fetchurl since the archive's checksum can change if github decides to regenerate the archive.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for noticing! Fixed (there is no params anymore). As for the fetchurl / fetchFromGitHub thing, I did not get the difference but in any case this is orthogonal to the current PR and can be changed independently.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added it because otherwise I would forget about that.

@Zimmi48
coqPackages.ssreflect: refactor choice of source version

Verified

This commit was signed with the committer’s verified signature.
Mic92 Jörg Thalheim
GPG key ID: CA4106B8D7CC79FA
Verified
Learn about vigilant mode
7cc369c
@Zimmi48 Zimmi48 force-pushed the give-default-version-of-ssreflect branch from 9d1fc00 to 7cc369c Compare November 5, 2018 17:11
@GrahamcOfBorg GrahamcOfBorg added 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux labels Nov 5, 2018
@globin
Copy link
Member

globin commented Nov 6, 2018

@GrahamcOfBorg build coqPackages.ssreflect coqPackages_8_5.ssreflect

Mic92
Mic92 reviewed Nov 6, 2018
View reviewed changes
pkgs/development/coq-modules/ssreflect/default.nix Outdated
"8.9" = param_1_7;

};
param = params."${coq.coq-version}";
in

stdenv.mkDerivation {
Copy link
Member

@Mic92 Mic92 Nov 6, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would be

inherit (mathcomp) src;

not a better choice here? Then we only need to keep one of the two modules up-to-date.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I thought about doing this indeed. I don't know why it wasn't the case from the beginning.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Feel free to go ahead and push another commit changing this.

@Mic92 Mic92 merged commit 846b2fa into NixOS:master Nov 6, 2018
@Zimmi48 Zimmi48 deleted the give-default-version-of-ssreflect branch November 6, 2018 16:13
@GrahamcOfBorg
Copy link

Success on x86_64-linux (full log)

Attempted: coqPackages.ssreflect, coqPackages_8_5.ssreflect

Partial log (click to expand)

make[1]: Entering directory '/build/source/mathcomp/ssreflect'
make[1]: Leaving directory '/build/source/mathcomp/ssreflect'
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/1zg4rdaxlxng4d6dd4pdyxw11w6jf8cx-coq8.8-ssreflect-1.7.0
strip is /nix/store/vcc4svb8gy29g4pam2zja6llkbcwsyiq-binutils-2.30/bin/strip
stripping (with command strip and flags -S) in /nix/store/1zg4rdaxlxng4d6dd4pdyxw11w6jf8cx-coq8.8-ssreflect-1.7.0/lib
patching script interpreter paths in /nix/store/1zg4rdaxlxng4d6dd4pdyxw11w6jf8cx-coq8.8-ssreflect-1.7.0
checking for references to /build in /nix/store/1zg4rdaxlxng4d6dd4pdyxw11w6jf8cx-coq8.8-ssreflect-1.7.0...
/nix/store/1zg4rdaxlxng4d6dd4pdyxw11w6jf8cx-coq8.8-ssreflect-1.7.0
/nix/store/hxa3n9s7p6zpkdk26mi816klybxddszz-coq8.5-ssreflect-1.6.1

@GrahamcOfBorg
Copy link

Success on x86_64-darwin (full log)

Attempted: coqPackages.ssreflect, coqPackages_8_5.ssreflect

Partial log (click to expand)

INSTALL ssrnotations.glob /nix/store/p8zp6w6hpv23rnbcv9kpxqgv5rwln67i-coq8.8-ssreflect-1.7.0/lib/coq/8.8/user-contrib/mathcomp/ssreflect/
INSTALL ssrmatching.glob /nix/store/p8zp6w6hpv23rnbcv9kpxqgv5rwln67i-coq8.8-ssreflect-1.7.0/lib/coq/8.8/user-contrib/mathcomp/ssreflect/
make[1]: Entering directory '/private/tmp/nix-build-coq8.8-ssreflect-1.7.0.drv-0/source/mathcomp/ssreflect'
make[1]: Leaving directory '/private/tmp/nix-build-coq8.8-ssreflect-1.7.0.drv-0/source/mathcomp/ssreflect'
post-installation fixup
strip is /nix/store/g5r4apl0za012ffs6ladinwa5w0m1l3k-cctools-binutils-darwin/bin/strip
stripping (with command strip and flags -S) in /nix/store/p8zp6w6hpv23rnbcv9kpxqgv5rwln67i-coq8.8-ssreflect-1.7.0/lib
patching script interpreter paths in /nix/store/p8zp6w6hpv23rnbcv9kpxqgv5rwln67i-coq8.8-ssreflect-1.7.0
/nix/store/p8zp6w6hpv23rnbcv9kpxqgv5rwln67i-coq8.8-ssreflect-1.7.0
/nix/store/p7rmhj02zqfz1jrjgs8msvcy5yhqyic9-coq8.5-ssreflect-1.6.1

@GrahamcOfBorg
Copy link

Success on aarch64-linux (full log)

Attempted: coqPackages.ssreflect

The following builds were skipped because they don't evaluate on aarch64-linux: coqPackages_8_5.ssreflect

Partial log (click to expand)

INSTALL ssrmatching.glob /nix/store/aq4napq6ykqv23028922wx16j9889liz-coq8.8-ssreflect-1.7.0/lib/coq/8.8/user-contrib/mathcomp/ssreflect/
make[1]: Entering directory '/build/source/mathcomp/ssreflect'
make[1]: Leaving directory '/build/source/mathcomp/ssreflect'
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/aq4napq6ykqv23028922wx16j9889liz-coq8.8-ssreflect-1.7.0
strip is /nix/store/p9akxn2sfy4wkhqdqa3li97pc6jaz3r1-binutils-2.30/bin/strip
stripping (with command strip and flags -S) in /nix/store/aq4napq6ykqv23028922wx16j9889liz-coq8.8-ssreflect-1.7.0/lib
patching script interpreter paths in /nix/store/aq4napq6ykqv23028922wx16j9889liz-coq8.8-ssreflect-1.7.0
checking for references to /build in /nix/store/aq4napq6ykqv23028922wx16j9889liz-coq8.8-ssreflect-1.7.0...
/nix/store/aq4napq6ykqv23028922wx16j9889liz-coq8.8-ssreflect-1.7.0

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Mic92 Mic92

Assignees
No one assigned
Labels
10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@Zimmi48 @globin @GrahamcOfBorg @Mic92