summaryrefslogtreecommitdiff
path: root/pkgs/development/coq-modules/goedel/default.nix
diff options
context:
space:
mode:
Diffstat (limited to 'pkgs/development/coq-modules/goedel/default.nix')
-rw-r--r--pkgs/development/coq-modules/goedel/default.nix24
1 files changed, 24 insertions, 0 deletions
diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/coq-modules/goedel/default.nix
new file mode 100644
index 000000000000..f6ed9491e98c
--- /dev/null
+++ b/pkgs/development/coq-modules/goedel/default.nix
@@ -0,0 +1,24 @@
+{ lib, mkCoqDerivation, coq, hydra-battles, pocklington, version ? null }:
+with lib;
+
+mkCoqDerivation {
+ pname = "goedel";
+ owner = "coq-community";
+
+ release."8.12.0".rev = "v8.12.0";
+ release."8.12.0".sha256 = "sha256-4lAwWFHGUzPcfHI9u5b+N+7mQ0sLJ8bH8beqQubfFEQ=";
+
+ inherit version;
+ defaultVersion = with versions; switch coq.coq-version [
+ { case = isGe "8.11"; out = "8.12.0"; }
+ ] null;
+
+ propagatedBuildInputs = [ hydra-battles pocklington ];
+
+ meta = {
+ description = "The Gödel-Rosser 1st incompleteness theorem in Coq";
+ maintainers = with maintainers; [ siraben ];
+ license = licenses.mit;
+ platforms = platforms.unix;
+ };
+}