gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

rocqPackages.micromega-plugin: init at 1.0.0 (#516906)

Browse Source
This commit is contained in:
Vincent Laporte
2026-05-06 13:43:08 +00:00
committed by GitHub
parent adc31dc975 d0f59b5219
commit fa04c27722
10 changed files with 97 additions and 19 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/development/coq-modules/compcert/default.nix
+2 -3
View File
@@ -4,7 +4,6 @@
coq,
flocq,
MenhirLib,
ocamlPackages,
fetchpatch,
makeWrapper,
coq2html,
@@ -71,7 +70,7 @@ let
strictDeps = true;
nativeBuildInputs = with ocamlPackages; [
nativeBuildInputs = with coq.ocamlPackages; [
makeWrapper
ocaml
findlib
@@ -79,7 +78,7 @@ let
coq
coq2html
];
buildInputs = with ocamlPackages; [ menhirLib ];
buildInputs = with coq.ocamlPackages; [ menhirLib ];
propagatedBuildInputs = [
flocq
MenhirLib
pkgs/development/coq-modules/graph-theory/default.nix
+4 -2
View File
@@ -52,10 +52,12 @@ mkCoqDerivation {
mathcomp.algebra
mathcomp-finmap
mathcomp.fingroup
mathcomp-algebra-tactics
fourcolor
stdlib
];
]
++ lib.optional (
mathcomp.version != "dev" && lib.versions.isLe "2.5" mathcomp.version
) mathcomp-algebra-tactics;
meta = {
description = "Library of formalized graph theory results in Coq";
pkgs/development/coq-modules/jasmin/default.nix
+4 -2
View File
@@ -38,9 +38,11 @@
release."2024.07.2".sha256 = "sha256-aF8SYY5jRxQ6iEr7t6mRN3BEmIDhJ53PGhuZiJGB+i8=";
propagatedBuildInputs = [
mathcomp-algebra-tactics
mathcomp-word
];
]
++ lib.optional (
mathcomp.version != "dev" && lib.versions.isLe "2.5" mathcomp.version
) mathcomp-algebra-tactics;
makeFlags = [
"-C"
pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
+7 -7
View File
@@ -32,13 +32,13 @@ mkCoqDerivation {
lib.switch
[ coq.coq-version mathcomp-algebra.version ]
[
(case (range "8.20" "9.1") (isGe "2.4") "1.2.7")
(case (range "8.20" "9.1") (isGe "2.4") "1.2.6")
(case (range "8.20" "9.1") (isGe "2.4") "1.2.5")
(case (range "8.16" "9.0") (isGe "2.0") "1.2.4")
(case (range "8.16" "8.18") (isGe "2.0") "1.2.2")
(case (range "8.16" "8.19") (isGe "1.15") "1.1.1")
(case (range "8.13" "8.16") (isGe "1.12") "1.0.0")
(case (range "8.20" "9.1") (range "2.4" "2.5") "1.2.7")
(case (range "8.20" "9.1") (range "2.4" "2.4") "1.2.6")
(case (range "8.20" "9.1") (range "2.4" "2.4") "1.2.5")
(case (range "8.16" "9.0") (range "2.0" "2.3") "1.2.4")
(case (range "8.16" "8.18") (range "2.0" "2.2") "1.2.2")
(case (range "8.16" "8.19") (range "1.15" "1.19") "1.1.1")
(case (range "8.13" "8.16") (range "1.12" "1.17") "1.0.0")
]
null;
pkgs/development/coq-modules/mathcomp-infotheo/default.nix
+6 -1
View File
@@ -1,6 +1,7 @@
{
coq,
mkCoqDerivation,
mathcomp,
mathcomp-analysis,
mathcomp-analysis-stdlib,
mathcomp-algebra-tactics,
@@ -71,6 +72,10 @@
(o: {
propagatedBuildInputs =
o.propagatedBuildInputs
++ lib.optional (lib.versions.isGe "0.6.1" o.version || o.version == "dev") mathcomp-algebra-tactics
++ lib.optional (
mathcomp.version != "dev"
&& lib.versions.isLe "2.5" mathcomp.version
&& (lib.versions.isGe "0.6.1" o.version || o.version == "dev")
) mathcomp-algebra-tactics
++ lib.optional (lib.versions.isGe "0.7.2" o.version || o.version == "dev") interval;
})
pkgs/development/coq-modules/mathcomp/default.nix
+1 -1
View File
@@ -256,7 +256,7 @@ if coq.rocqPackages ? mathcomp && version != "2.3.0" && version != "2.4.0" then
fetchzip
hierarchy-builder
;
inherit (coq.rocqPackages) rocq-core;
inherit (coq.rocqPackages) rocq-core micromega-plugin;
};
in
mc
pkgs/development/rocq-modules/mathcomp/default.nix
+17 -2
View File
@@ -21,6 +21,7 @@
single ? false,
rocq-core,
hierarchy-builder,
micromega-plugin,
version ? null,
}@args:
@@ -139,8 +140,22 @@ let
extraInstallFlags = [ "-f Makefile.coq" ];
}
);
# patched-derivation1 = derivation.overrideAttrs ...
patched-derivation1 = derivation.overrideAttrs (
o:
lib.optionalAttrs
(
lib.elem package [
"algebra"
"single"
]
&& o.version != null
&& (o.version == "dev" || lib.versions.isGe "2.6.0" o.version)
)
{
propagatedBuildInputs = o.propagatedBuildInputs ++ [ micromega-plugin ];
}
);
in
derivation;
patched-derivation1;
in
mathcomp_ (if single then "single" else "all")
pkgs/development/rocq-modules/micromega-plugin/default.nix
+55
View File
@@ -0,0 +1,55 @@
{
lib,
mkRocqDerivation,
rocq-core,
version ? null,
}:
mkRocqDerivation {
pname = "micromega-plugin";
owner = "rocq-community";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch rocq-core.rocq-version [
(case (range "9.0" "9.2") "1.0.0")
] null;
release = {
"1.0.0".sha256 = "sha256-srDOrGC4h21O9MIHfmOMJ0BKQhamaWyzQT72TwgfDYc=";
};
releaseRev = v: "v${v}";
mlPlugin = true;
useDune = true;
nativeBuildInputs = [
rocq-core.ocamlPackages.ppx_optcomp
];
propagatedBuildInputs = [
rocq-core.ocamlPackages.findlib
];
configurePhase = ''
patchShebangs etc/with-rocq-wrap.sh
'';
buildPhase = ''
etc/with-rocq-wrap.sh dune build -p micromega-plugin @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
'';
installPhase = ''
etc/with-rocq-wrap.sh dune install --root . micromega-plugin --prefix=$out --libdir $OCAMLFIND_DESTDIR
mkdir $out/lib/coq/
mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${rocq-core.rocq-version}
'';
meta = {
description = "Plugin for (semi)decision procedures for arithmetic.";
license = lib.licenses.lgpl21;
};
}
pkgs/top-level/coq-packages.nix
-1
View File
@@ -88,7 +88,6 @@ let
lib
stdenv
;
ocamlPackages = ocamlPackages_4_14;
};
ConCert = callPackage ../development/coq-modules/ConCert { };
coq-bits = callPackage ../development/coq-modules/coq-bits { };
pkgs/top-level/rocq-packages.nix
+1
View File
@@ -57,6 +57,7 @@ let
mathcomp-finmap = callPackage ../development/rocq-modules/mathcomp-finmap { };
mathcomp-reals = self.mathcomp-analysis.reals;
mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib;
micromega-plugin = callPackage ../development/rocq-modules/micromega-plugin { };
parseque = callPackage ../development/rocq-modules/parseque { };
relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };
rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };