-
-
Notifications
You must be signed in to change notification settings - Fork 13.1k
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
coq_8_12: 8.12+β1 → 8.12.0; coqPackages.equations: 1.2.2 → 1.2.3 #94230
Conversation
@GrahamcOfBorg build coqPackages_8_12.bignums coqPackages_8_12.equations |
@@ -59,7 +59,9 @@ stdenv.mkDerivation rec { | |||
sha256 = param.sha256; | |||
}; | |||
|
|||
buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; | |||
buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ] | |||
++ stdenv.lib.optional (stdenv.lib.versionAtLeast coq.coq-version "8.12") num |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you explain what changed that necessitates this starting with 8.12? I've also observed this failure in aac-tactics (cf. coq-community/aac-tactics#61) but it left me puzzled regarding its origin. Note that this fix is not sufficient, you need the same for Bignums (cf. the failing checks).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don’t know. This seems to be a change between the β and the release.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could that change in Coq be related: coq/coq#12604?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, this is certainly it. And the timeline matches perfectly.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks. I’ve also fixed bignums.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Have you seen the discussion about this issue in coq/coq#12604? Do you think we should propagate the dependency on num
and be done with it? Do you understand why this PR had this effect? Enrico was puzzled by it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
IIUC, if ocamlfind
is told not to link a specific library, it tries to resolve it and fails if the library is not there. Therefore, Coq plug-ins that do not use num
must depend on them so that ocamlfind
can find out what is the library that should not be linked.
Let’s hide this funny issue under the carpet and have Coq-8.12 propagate num
. Will Coq get rid of num
in 8.13?
Thanks Théo for leading this discussion.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, I think this is a good summary and a good solution.
Will Coq get rid of
num
in 8.13?
I really can't tell.
coqPackages.equations: 1.2.2 → 1.2.3
Since this PR, ocamlfind looks for num when building plugins. To avoid requiring all plugins to add a new, irrelevant, dependency, we propagate it. This solution imitates what was decided for nixpkgs in NixOS/nixpkgs#94230. Fix coq-community/aac-tactics#61.
Since this PR, ocamlfind looks for num when building plugins. To avoid requiring all plugins to add a new, irrelevant, dependency, we propagate it. This solution imitates what was decided for nixpkgs in NixOS/nixpkgs#94230. Fix coq-community/aac-tactics#61. (cherry picked from commit a2da872)
Since this PR, ocamlfind looks for num when building plugins. To avoid requiring all plugins to add a new, irrelevant, dependency, we propagate it. This solution imitates what was decided for nixpkgs in NixOS/nixpkgs#94230. Fix coq-community/aac-tactics#61.
Since this PR, ocamlfind looks for num when building plugins. To avoid requiring all plugins to add a new, irrelevant, dependency, we propagate it. This solution imitates what was decided for nixpkgs in NixOS/nixpkgs#94230. Fix coq-community/aac-tactics#61.
Motivation for this change
New release: https://github.com/coq/coq/releases/tag/V8.12.0
Also update the
equations
package for compatibility with Coq 8.12.0Things done
sandbox
innix.conf
on non-NixOS linux)nix-shell -p nixpkgs-review --run "nixpkgs-review wip"
./result/bin/
)nix path-info -S
before and after)