blob: ef3a85954e61e353fae42c200c93728b5312b0bc (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
{ stdenv, lib, coq, itauto }:
let excluded =
lib.optionals (lib.versions.isEq "8.16" itauto.version) [ "arith.v" "refl_bool.v" ]
; in
stdenv.mkDerivation {
pname = "coq${coq.coq-version}-itauto-test";
inherit (itauto) src version;
nativeCheckInputs = [ coq itauto ];
dontConfigure = true;
dontBuild = true;
doCheck = true;
checkPhase = ''
cd test-suite
for m in *.v
do
echo -n ${lib.concatStringsSep " " excluded} | grep --silent $m && continue
echo $m && coqc $m
done
'';
installPhase = "touch $out";
}
|