blob: 75ad9aec33a7a1d72559ee0b63e70fdfa7cb04e1 (
plain)
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
{
lib,
mkCoqDerivation,
coq,
stdlib,
unicoq,
version ? null,
}:
mkCoqDerivation {
pname = "Mtac2";
owner = "Mtac2";
inherit version;
defaultVersion =
with lib.versions;
lib.switch coq.version [
{
case = isEq "9.1";
out = "1.4-rocq${coq.coq-version}";
}
{
case = range "8.19" "9.0";
out = "1.4-coq${coq.coq-version}";
}
] null;
release."1.4-rocq9.1".hash = "sha256-A+ac84ZfDMW2NhS/NrGIfdairXmzXxZIYGNmJIz0ReM=";
release."1.4-coq9.0".sha256 = "sha256-pAPBRCW7M46UZPJ+v/0xAT8mpQURN8czMmlrfYz/MVU=";
release."1.4-coq8.20".sha256 = "sha256-3nu/8zDvdnl6WzGtw46mVcdqgkRgc6Xy8/I+lUOrSIY=";
release."1.4-coq8.19".sha256 = "sha256-G9eK0eLyECdT20/yf8yyz7M8Xq2WnHHaHpxVGP0yTtU=";
releaseRev = v: "v${v}";
mlPlugin = true;
propagatedBuildInputs = [
stdlib
unicoq
];
meta = {
description = "Typed tactic language for Coq";
license = lib.licenses.mit;
};
preBuild = ''
coq_makefile -f _CoqProject -o Makefile
patchShebangs tests/sf-5/configure.sh
'';
}
|
