tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp-boot,
6 stdlib,
7 version ? null,
8}:
9
10mkCoqDerivation {
11 pname = "autosubst";
12
13 releaseRev = v: "v${v}";
14
15 release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI=";
16 release."1.8".sha256 = "sha256-n0lD8D+tjqkDDjFiE4CggxczOPS5TkEnxpB3zEwWZ2I=";
17 release."1.9".sha256 = "sha256-XiLZjMc+1iwRGOstfLm/WQRF6FTdX6oJr5urn3wmLlA=";
18
19 inherit version;
20 defaultVersion =
21 let
22 case = case: out: { inherit case out; };
23 in
24 with lib.versions;
25 lib.switch coq.coq-version [
26 (case (range "8.14" "9.1") "1.9")
27 (case (range "8.14" "8.18") "1.8")
28 (case (range "8.10" "8.13") "1.7")
29 ] null;
30
31 propagatedBuildInputs = [
32 mathcomp-boot
33 stdlib
34 ];
35
36 meta = with lib; {
37 homepage = "https://www.ps.uni-saarland.de/autosubst/";
38 description = "Automation for de Bruijn syntax and substitution in Coq";
39 maintainers = with maintainers; [
40 siraben
41 jwiegley
42 ];
43 license = licenses.mit;
44 };
45}