coqPackages.simple-io: fix & add tests

pkgs/development/coq-modules/simple-io/default.nix

@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, coq, coq-ext-lib, version ? null }:
+{ lib, callPackage, mkCoqDerivation, coq, coq-ext-lib, version ? null }:
 
 with lib; mkCoqDerivation {
   pname = "simple-io";
@@ -13,11 +13,14 @@ with lib; mkCoqDerivation {
   release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
   mlPlugin = true;
   nativeBuildInputs = [ coq.ocamlPackages.cppo ];
-  propagatedBuildInputs = [ coq-ext-lib coq.ocamlPackages.ocamlbuild ];
+  propagatedBuildInputs = [ coq-ext-lib ]
+  ++ (with coq.ocamlPackages; [ ocaml findlib ocamlbuild ]);
 
   doCheck = true;
   checkTarget = "test";
 
+  passthru.tests.HelloWorld = callPackage ./test.nix {};
+
   meta = {
     description = "Purely functional IO for Coq";
     license = licenses.mit;

pkgs/development/coq-modules/simple-io/test.nix

@@ -0,0 +1,21 @@
+{ stdenv, coq, simple-io }:
+
+stdenv.mkDerivation {
+  pname = "coq-simple-io-test";
+  inherit (simple-io) src version;
+  checkInputs = [ coq simple-io ];
+  dontConfigure = true;
+  dontBuild = true;
+  doCheck = true;
+
+  checkPhase = ''
+    cd test
+    for p in Argv.v Example.v HelloWorld.v TestExtraction.v TestPervasives.v
+    do
+      [ -f $p ] && echo $p && coqc $p
+    done
+  '';
+
+  installPhase = "touch $out";
+
+}