pyrox.dev
coqPackages.itauto: init at 8.17.0 for Coq 8.17
Propagate `findlib` when needed
Add tests
authored by Vincent Laporte and committed by Vincent Laporte cc2fb2c1 d0c43ed4
+10
-3
pkgs/development/coq-modules/itauto/default.nix
+10
-3
pkgs/development/coq-modules/itauto/default.nix
···
1
-
{ lib, mkCoqDerivation, coq, version ? null }:
1
+
{ lib, callPackage, mkCoqDerivation, coq, version ? null }:
2
2
3
-
mkCoqDerivation rec {
3
+
(mkCoqDerivation rec {
4
4
pname = "itauto";
5
5
owner = "fbesson";
6
6
domain = "gitlab.inria.fr";
7
7
8
+
release."8.17.0".sha256 = "sha256-fgdnKchNT1Hyrq14gU8KWYnlSfg3qlsSw5A4+RoA26w=";
8
9
release."8.16.0".sha256 = "sha256-4zAUYGlw/pBcLPv2GroIduIlvbfi1+Vy+TdY8KLCqO4=";
9
10
release."8.15.0".sha256 = "sha256:10qpv4nx1p0wm9sas47yzsg9z22dhvizszfa21yff08a8fr0igya";
10
11
release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9";
11
12
release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
12
13
inherit version;
13
14
defaultVersion = with lib.versions; lib.switch coq.coq-version [
15
+
{ case = isEq "8.17"; out = "8.17.0"; }
14
16
{ case = isEq "8.16"; out = "8.16.0"; }
15
17
{ case = isEq "8.15"; out = "8.15.0"; }
16
18
{ case = isEq "8.14"; out = "8.14.0"; }
···
21
23
nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
22
24
enableParallelBuilding = false;
23
25
26
+
passthru.tests.suite = callPackage ./test.nix {};
27
+
24
28
meta = with lib; {
25
29
description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
26
30
maintainers = with maintainers; [ siraben ];
27
31
license = licenses.gpl3Plus;
28
32
};
29
-
}
33
+
}).overrideAttrs (o: lib.optionalAttrs
34
+
(o.version == "dev" || lib.versionAtLeast o.version "8.16") {
35
+
propagatedBuildInputs = [ coq.ocamlPackages.findlib ];
36
+
})
+27
pkgs/development/coq-modules/itauto/test.nix
+27
pkgs/development/coq-modules/itauto/test.nix
···
1
+
{ stdenv, lib, coq, itauto }:
2
+
3
+
let excluded =
4
+
lib.optionals (lib.versions.isEq "8.16" itauto.version) [ "arith.v" "refl_bool.v" ]
5
+
; in
6
+
7
+
stdenv.mkDerivation {
8
+
pname = "coq${coq.coq-version}-itauto-test";
9
+
inherit (itauto) src version;
10
+
11
+
nativeCheckInputs = [ coq itauto ];
12
+
13
+
dontConfigure = true;
14
+
dontBuild = true;
15
+
doCheck = true;
16
+
17
+
checkPhase = ''
18
+
cd test-suite
19
+
for m in *.v
20
+
do
21
+
echo -n ${lib.concatStringsSep " " excluded} | grep --silent $m && continue
22
+
echo $m && coqc $m
23
+
done
24
+
'';
25
+
26
+
installPhase = "touch $out";
27
+
}