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

Conversation

Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Nov 5, 2018 •
edited

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.

@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

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 Zimmi48 force-pushed the give-default-version-of-ssreflect branch from 9d1fc00 to 7cc369c Compare November 5, 2018 17:11
@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

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 Mic92 left review comments

Assignees
No one assigned
Labels
10.rebuild-darwin: 0 10.rebuild-linux: 0
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

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