tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 hydra-battles,
6 pocklington,
7 version ? null,
8}:
9
10mkCoqDerivation {
11 pname = "goedel";
12 owner = "coq-community";
13
14 releaseRev = (v: "v${v}");
15
16 release."8.12.0".sha256 = "sha256-4lAwWFHGUzPcfHI9u5b+N+7mQ0sLJ8bH8beqQubfFEQ=";
17 release."8.13.0".sha256 = "0sqqkmj6wsk4xmhrnqkhcsbsrqjzn2gnk67nqzgrmjpw5danz8y5";
18
19 inherit version;
20 defaultVersion =
21 with lib.versions;
22 lib.switch coq.coq-version [
23 {
24 case = range "8.11" "8.16";
25 out = "8.13.0";
26 }
27 ] null;
28
29 propagatedBuildInputs = [
30 hydra-battles
31 pocklington
32 ];
33
34 meta = with lib; {
35 description = "Gödel-Rosser 1st incompleteness theorem in Coq";
36 maintainers = with maintainers; [ siraben ];
37 license = licenses.mit;
38 platforms = platforms.unix;
39 };
40}