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

Jump to bottom

coqPackages: fix + add multinomials 1.3 + coqeal 1.0.0 #62718

Merged
merged 1 commit into from Jul 2, 2019
Merged

coqPackages: fix + add multinomials 1.3 + coqeal 1.0.0 #62718

merged 1 commit into from Jul 2, 2019

Conversation

CohenCyril
Copy link
Contributor

Motivation for this change

Fixing my buggy implementation of generation of additional packages for mathcomp and added multinomials release 1.3 and coqeal release 1.0.0

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 nix-review --run "nix-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)
  • Assured whether relevant documentation is up to date
  • Fits CONTRIBUTING.md.

@CohenCyril
Copy link
Contributor Author

CohenCyril commented Jun 5, 2019 •
edited

@vbgl can you build the appropriate packages (coqPackages_8_8.coqeal, coqPackages_8_9.coqeal, coqPackages_8_9.multinomials)

@vbgl
Copy link
Contributor

vbgl commented Jun 5, 2019

Evaluation fails:

error: while querying the derivation named 'coq8.8-mathcomp-1.7.0-analysis-0.1.0':
undefined variable 'mathcomp' at …/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix:138:13

Also (unrelated to this PR, I guess, but worth mentioning), the naming is wrong: this mathcomp-analysis package is named “coq8.8-mathcomp” and has version “1.7.0-analysis-0.1.0”.

@CohenCyril CohenCyril force-pushed the coqPackages_fix branch 2 times, most recently from d73e9cb to f3a8f41 Compare June 5, 2019 09:15
@CohenCyril
Copy link
Contributor Author

Also (unrelated to this PR, I guess, but worth mentioning), the naming is wrong: this mathcomp-analysis package is named “coq8.8-mathcomp” and has version “1.7.0-analysis-0.1.0”.

I could not reproduce this,

nix-repl> with import ./. {}; coqPackages.mathcomp-analysis.name

and all the variants I could think of give the right versions.

@CohenCyril
Copy link
Contributor Author

Evaluation fails:

error: while querying the derivation named 'coq8.8-mathcomp-1.7.0-analysis-0.1.0':
undefined variable 'mathcomp' at …/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix:138:13

This should be fixed now

@vbgl
Copy link
Contributor

vbgl commented Jun 5, 2019

nix-repl> lib.getVersion coqPackages.mathcomp-analysis.name
"1.9.0-analysis-0.2.2"

@CohenCyril
Copy link
Contributor Author

@vbgl what would be the recommended name instead of coq8.8-mathcomp-1.7.0-analysis-0.1.0 ?

@CohenCyril
Copy link
Contributor Author

@vbgl, would it be analysis-0.1.0+coq-8.8.1+mathcomp-1.7.0 ?

@vbgl
Copy link
Contributor

vbgl commented Jun 6, 2019

CoqEAL does not build with Coq 8.7 or 8.9, e.g.:

builder for '/nix/store/n57zd4031f9y3xkjfcxz122m938hhaha-coq8.8-mathcomp-1.9.0-coqeal-1.0.0.drv' failed with exit code 2; last 10 log lines:
COQC refinements/refinements.v
COQC refinements/pos.v
COQC refinements/binnat.v
File "./refinements/binnat.v", line 379, characters 0-4:
Error: Attempt to save an incomplete proof (in proof Rnat_ltE)
make[2]: *** [Makefile.coq:657: refinements/binnat.vo] Error 1
make[1]: *** [Makefile.coq:318: all] Error 2
make[1]: Leaving directory '/build/source'
make: *** [Makefile.common:67: this-build] Error 2

About naming, something looks wrong: it is OK to have different versions of a library for different versions of Coq. But for a given version of Coq, one version of the library should be enough. Otherwise you are bound to have to deal with an exponential mess.

@CohenCyril
Copy link
Contributor Author

CohenCyril commented Jun 6, 2019 •
edited

About naming, something looks wrong: it is OK to have different versions of a library for different versions of Coq. But for a given version of Coq, one version of the library should be enough. Otherwise you are bound to have to deal with an exponential mess.

It's not enough, some libraries are compatible only with a restricted set of versions of the others...

@CohenCyril CohenCyril mentioned this pull request Jun 13, 2019
Closed
10 tasks
@CohenCyril
Copy link
Contributor Author

CoqEAL does not build with Coq 8.7 or 8.9, e.g.:

This should be fixed now...

@CohenCyril
Copy link
Contributor Author

@vbgl is it okay to merge now?

@vbgl
Copy link
Contributor

vbgl commented Jun 15, 2019

mathcomp-analysis does not build with Coq 8.7.

@CohenCyril
Copy link
Contributor Author

@vbgl should be fixed now

vbgl
vbgl reviewed Jun 27, 2019
View reviewed changes
pkgs/top-level/coq-packages.nix Outdated

mathcomp_1_7-finmap mathcomp_1_7-bigenough mathcomp_1_7-analysis
mathcomp_1_7-multinomials mathcomp_1_7-real-closed
mathcomp_1_7-finmap_1_0
mathcomp_1_7-finmap_1_0 mathcomp_1_7-coqeal
Copy link
Contributor

Choose a reason for hiding this comment

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

This guy does not exist (mathcomp_1_7-coqeal)

pkgs/top-level/coq-packages.nix Outdated

mathcomp_1_9-finmap mathcomp_1_9-bigenough mathcomp_1_9-analysis
mathcomp_1_9-multinomials mathcomp_1_9-real-closed;
mathcomp_1_9-multinomials mathcomp_1_9-real-closed mathcomp_1_9-coqeal;
Copy link
Contributor

Choose a reason for hiding this comment

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

This one neither (mathcomp_1_9-coqeal).

vbgl
vbgl reviewed Jun 27, 2019
View reviewed changes
pkgs/top-level/coq-packages.nix Outdated

mathcomp_1_9-finmap mathcomp_1_9-bigenough mathcomp_1_9-analysis
mathcomp_1_9-multinomials mathcomp_1_9-real-closed;
mathcomp_1_9-multinomials mathcomp_1_9-real-closed
Copy link
Contributor

Choose a reason for hiding this comment

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

missing semicolon?

@vbgl
Copy link
Contributor

vbgl commented Jul 2, 2019

@GrahamcOfBorg build coqPackages_8_9.coqeal

@vbgl vbgl merged commit d801489 into NixOS:master Jul 2, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vbgl vbgl vbgl 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
2 participants
@CohenCyril @vbgl