coqPackages_8_20.coq-elpi: fix build

coqPackages_8_20.stalmarck-tactic: fix build
This commit is contained in:
Vincent Laporte 2026-06-04 14:32:05 +02:00
commit 1d5b338a70
No known key found for this signature in database
5 changed files with 20 additions and 2 deletions

View file

@ -105,11 +105,25 @@ let
substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
'';
dune =
if lib.versions.isEq coq-version "8.20" then
args.dune.override { version = "3.21.1"; }
else
args.dune;
ocamlPackages =
if customOCamlPackages != null then
customOCamlPackages
else
lib.switch coq-version [
{
case = lib.versions.isEq "8.20";
out = ocamlPackages_4_14.overrideScope (
self: super: {
inherit dune;
dune_3 = dune;
}
);
}
{
case = lib.versions.range "8.16" "9.1";
out = ocamlPackages_4_14;

View file

@ -22,6 +22,7 @@ stdenv.mkDerivation {
hash =
{
"3.22.2" = "sha256-wsz4vGsXr6R8RQKXNXSWMDqnyGgOMpt52Yxo41AToRg=";
"3.21.1" = "sha256-hPeoLG2ApxJPOEfppInoDPvq+3vtNXOsAShu9W/QjZQ=";
"2.9.3" = "sha256:1ml8bxym8sdfz25bx947al7cvsi2zg5lcv7x9w6xb01cmdryqr9y";
}
."${version}";

View file

@ -2,6 +2,7 @@
lib,
mkCoqDerivation,
which,
dune,
coq,
stdlib,
version ? null,
@ -33,7 +34,7 @@ let
propagatedBuildInputs_wo_elpi = [
coq.ocamlPackages.findlib
];
derivation = mkCoqDerivation {
derivation = mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
pname = "elpi";
repo = "coq-elpi";
owner = "LPCIC";

View file

@ -1,6 +1,7 @@
{
lib,
mkCoqDerivation,
dune,
coq,
stdlib,
version ? null,
@ -38,7 +39,7 @@ let
else
"A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.";
in
mkCoqDerivation {
mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
inherit
version
pname

View file

@ -17,6 +17,7 @@
fetchpatch,
makeWrapper,
coq2html,
dune,
}@args:
let
lib = import ../build-support/coq/extra-lib.nix { inherit (args) lib; };