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.
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.
I don’t know. This seems to be a change between the β and the release.
There was a problem hiding this comment.
Could that change in Coq be related: coq/coq#12604?
There was a problem hiding this comment.
Yes, this is certainly it. And the timeline matches perfectly.
There was a problem hiding this comment.
Thanks. I’ve also fixed bignums.
There was a problem hiding this comment.
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.
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.
Thanks, I think this is a good summary and a good solution.
Will Coq get rid of
numin 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
equationspackage for compatibility with Coq 8.12.0Things done
sandboxinnix.confon non-NixOS linux)nix-shell -p nixpkgs-review --run "nixpkgs-review wip"./result/bin/)nix path-info -Sbefore and after)