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.

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

coqPackages coqPackages_8_10 coqPackages_8_11 #86088

Merged
merged 3 commits into from May 9, 2020
Merged

Conversation

@CohenCyril
Copy link
Contributor

CohenCyril commented Apr 27, 2020

Motivation for this change

The way Coq mathcomp core and extra packages were generated did not allow enough freedom to both limit the number of exposed derivation and dynamically patch one. Now it does and it is highly configurable.

Also:

  • fixed bignum version
  • fixed coq-bits version
  • fixed coqprime version
Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
  • 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 nixpkgs-review --run "nixpkgs-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)
  • Ensured that relevant documentation is up to date
  • Fits CONTRIBUTING.md.
@CohenCyril
Copy link
Contributor Author

CohenCyril commented Apr 27, 2020

@GrahamcOfBorg build coqPackages coqPackages_8_10 coqPackages_8_11

@CohenCyril CohenCyril mentioned this pull request Apr 27, 2020
3 of 10 tasks complete
@CohenCyril CohenCyril changed the title Updating coqPackages coqPackages_8_10 coqPackages_8_11 coqPackages coqPackages_8_10 coqPackages_8_11 Apr 27, 2020
@vbgl vbgl added the 6.topic: coq label Apr 27, 2020
@CohenCyril
Copy link
Contributor Author

CohenCyril commented Apr 27, 2020

@vbgl my build was not triggered, but I intend to simplify my PR a little bit again so wait for my signal.

- fixed bignum version
- fixed coq-bits version
- fixed coqprime version
- fixed mathcomp and mathcomp extra packages
  (reworked building scheme and removed unused ssreflect directory)
- giving the user access to function filterCoqPackages, because overrideScope' does not re-apply it.
@CohenCyril CohenCyril force-pushed the CohenCyril:mathcomp-1.11 branch from 593d2d8 to 597fa61 Apr 27, 2020
@CohenCyril
Copy link
Contributor Author

CohenCyril commented Apr 27, 2020

@GrahamcOfBorg build coqPackages coqPackages_8_10 coqPackages_8_11

@CohenCyril
Copy link
Contributor Author

CohenCyril commented Apr 27, 2020

@vbgl can you trigger the builds? Thanks 😸

@vbgl
Copy link
Contributor

vbgl commented Apr 27, 2020

No, sorry. The bot seems lazy today. Might be enjoying the beautiful weather outside…

CohenCyril added 2 commits Apr 27, 2020
@CohenCyril
Copy link
Contributor Author

CohenCyril commented Apr 30, 2020

@GrahamcOfBorg build coqPackages coqPackages_8_10 coqPackages_8_11

@vbgl
Copy link
Contributor

vbgl commented May 6, 2020

@GrahamcOfBorg build coqPackages.mathcomp coqPackages_8_10.mathcomp coqPackages_8_11.mathcomp

@CohenCyril
Copy link
Contributor Author

CohenCyril commented May 8, 2020

@vbgl do you understand why the compilation on darwin is still running???

@vbgl vbgl merged commit 8d05e53 into NixOS:master May 9, 2020
19 checks passed
19 checks passed
(unknown attributes) on x86_64-darwin No attempt
Details
coqPackages, coqPackages_8_10, coqPackages_8_11 on aarch64-linux Failure
Details
coqPackages, coqPackages_8_10, coqPackages_8_11 on x86_64-linux Failure
Details
Evaluation Performance Report Evaluator Performance Report
Details
coqPackages.mathcomp, coqPackages_8_10.mathcomp, coqPackages_8_11.mathcomp on aarch64-linux Success
Details
coqPackages.mathcomp, coqPackages_8_10.mathcomp, coqPackages_8_11.mathcomp on x86_64-darwin Success
Details
coqPackages.mathcomp, coqPackages_8_10.mathcomp, coqPackages_8_11.mathcomp on x86_64-linux Success
Details
grahamcofborg-eval ^.^!
Details
grahamcofborg-eval-check-meta config.nix: checkMeta = true
Details
grahamcofborg-eval-darwin nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="6a22f47"; rev="6a22f478dc3a51664b6df829e6b82beb3502846b"; } ./pkgs/t
Details
grahamcofborg-eval-lib-tests nix-build --arg pkgs import ./. {} ./lib/tests/release.nix
Details
grahamcofborg-eval-nixos nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="6a22f47"; rev="6a22f478dc3a51664b6df829e6b82beb3502846b"; } ./nixos/
Details
grahamcofborg-eval-nixos-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="6a22f47"; rev="6a22f478dc3a51664b6df829e6b82beb3502846b"; } ./nixos/
Details
grahamcofborg-eval-nixos-options nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="6a22f47"; rev="6a22f478dc3a51664b6df829e6b82beb3502846b"; } ./nixos/
Details
grahamcofborg-eval-nixpkgs-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="6a22f47"; rev="6a22f478dc3a51664b6df829e6b82beb3502846b"; } ./pkgs/t
Details
grahamcofborg-eval-nixpkgs-tarball nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="6a22f47"; rev="6a22f478dc3a51664b6df829e6b82beb3502846b"; } ./pkgs/t
Details
grahamcofborg-eval-nixpkgs-unstable-jobset nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="6a22f47"; rev="6a22f478dc3a51664b6df829e6b82beb3502846b"; } ./pkgs/t
Details
grahamcofborg-eval-package-list nix-env -qa --json --file .
Details
grahamcofborg-eval-package-list-no-aliases nix-env -qa --json --file . --arg config { allowAliases = false; }
Details
@vbgl
Copy link
Contributor

vbgl commented May 9, 2020

Thank you Cyril for taking care of the mathcomp package set!

@CohenCyril
Copy link
Contributor Author

CohenCyril commented May 9, 2020

@vbgl thanks for merging!

maralorn added a commit to maralorn/nixpkgs that referenced this pull request May 10, 2020
- fixed bignum version
- fixed coq-bits version
- fixed coqprime version
- fixed mathcomp and mathcomp extra packages
  (reworked building scheme and removed unused ssreflect directory)
- giving the user access to function filterCoqPackages, because overrideScope' does not re-apply it.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

2 participants
You can’t perform that action at this time.