coqPackages.ElmExtraction: init at 0.1.0 (#326305)

maintainers/maintainer-list.nix

@@ -243,6 +243,12 @@
     github = "48cf";
     githubId = 32851089;
   };
+  _4ever2 = {
+    email = "eske@cs.au.dk";
+    github = "4ever2";
+    githubId = 3417013;
+    name = "Eske Nielsen";
+  };
   _6543 = {
     email = "6543@obermui.de";
     github = "6543";

pkgs/development/coq-modules/ElmExtraction/default.nix

@@ -0,0 +1,52 @@
+{
+  lib,
+  mkCoqDerivation,
+  which,
+  coq,
+  metacoq,
+  version ? null,
+}:
+
+with lib;
+mkCoqDerivation {
+  pname = "ElmExtraction";
+  repo = "coq-elm-extraction";
+  owner = "AU-COBRA";
+  domain = "github.com";
+
+  inherit version;
+  defaultVersion =
+    with versions;
+    switch
+      [
+        coq.coq-version
+        metacoq.version
+      ]
+      [
+        {
+          cases = [
+            (range "8.17" "8.20")
+            (range "1.3.1" "1.3.2")
+          ];
+          out = "0.1.0";
+        }
+      ]
+      null;
+
+  release."0.1.0".sha256 = "EWjubBHsxAl2HuRAfJI3B9qzP2mj89eh0CUc8y7/7Ds=";
+
+  releaseRev = v: "v${v}";
+
+  propagatedBuildInputs = [
+    coq.ocamlPackages.findlib
+    metacoq
+  ];
+
+  postPatch = ''patchShebangs ./tests/process-extraction-examples.sh'';
+
+  meta = {
+    description = "A framework for extracting Coq programs to Elm";
+    maintainers = with maintainers; [ _4ever2 ];
+    license = licenses.mit;
+  };
+}

pkgs/top-level/coq-packages.nix

@@ -60,6 +60,7 @@ let
       corn = callPackage ../development/coq-modules/corn {};
       deriving = callPackage ../development/coq-modules/deriving {};
       dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
+      ElmExtraction = callPackage ../development/coq-modules/ElmExtraction {};
       equations = callPackage ../development/coq-modules/equations { };
       extructures = callPackage ../development/coq-modules/extructures { };
       fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};