Commit 43f5fc8e authored by Mathew Polzin's avatar Mathew Polzin
Browse files

idris2: add buildIdris tests

parent b09ba65a
Loading
Loading
Loading
Loading
+116 −13
Original line number Diff line number Diff line
{
  stdenv,
  runCommand,
  lib,
  pname,
  idris2,
  idris2Packages,
  zsh,
  tree,
}:

let
@@ -17,8 +20,8 @@ let
    let
      packageString = builtins.concatStringsSep " " (map (p: "--package " + p) packages);
    in
    stdenv.mkDerivation {
      name = "${pname}-${testName}";
    runCommand "${pname}-${testName}"
      {
        meta.timeout = 60;

        # with idris2 compiled binaries assume zsh is available on darwin, but that
@@ -26,8 +29,8 @@ let
        # when we build for darwin in tests. While this is impure, this is also what
        # we find in real darwin hosts.
        nativeBuildInputs = lib.optionals stdenv.isDarwin [ zsh ];

      buildCommand = ''
      }
      ''
        set -eo pipefail

        cat > packageTest.idr <<HERE
@@ -47,11 +50,43 @@ let

        touch $out
      '';
    };

  testBuildIdris =
    {
      testName,
      buildIdrisArgs,
      makeExecutable,
      expectedTree,
    }:
    let
      final = pkg: if makeExecutable then pkg.executable else pkg.library { };
      idrisPkg = final (idris2Packages.buildIdris buildIdrisArgs);
    in
    runCommand "${pname}-${testName}"
      {
        meta.timeout = 60;

        nativeBuildInputs = [ tree ];
      }
      ''
        GOT="$(tree ${idrisPkg} | tail -n +2)"

        if [ "$GOT" = '${expectedTree}' ]; then
          echo "${testName} SUCCESS"
        else
          >&2 echo "Got:
          $GOT"
          >&2 echo 'want:
          ${expectedTree}'
          exit 1
        fi

        touch $out
      '';
in
{
  # Simple hello world compiles, runs and outputs as expected
  hello-world = testCompileAndRun {
  helloWorld = testCompileAndRun {
    testName = "hello-world";
    code = ''
      module Main
@@ -63,7 +98,7 @@ in
  };

  # Data.Vect.Sort is available via --package contrib
  use-contrib = testCompileAndRun {
  useContrib = testCompileAndRun {
    testName = "use-contrib";
    packages = [ "contrib" ];
    code = ''
@@ -80,4 +115,72 @@ in
    '';
    want = "[1, 3, 5]";
  };

  buildLibrary = testBuildIdris {
    testName = "library-package";
    buildIdrisArgs = {
      ipkgName = "pkg";
      idrisLibraries = [ idris2Packages.idris2Api ];
      src = runCommand "library-package-src" { } ''
        mkdir $out

        cat > $out/Main.idr <<EOF
        module Main

        import Compiler.ANF -- from Idris2Api

        hello : String
        hello = "world"
        EOF

        cat > $out/pkg.ipkg <<EOF
        package pkg
        modules = Main
        depends = idris2
        EOF
      '';
    };
    makeExecutable = false;
    expectedTree = ''
      `-- lib
          `-- idris2-0.7.0
              `-- pkg-0
                  |-- 2023090800
                  |   |-- Main.ttc
                  |   `-- Main.ttm
                  `-- pkg.ipkg

      5 directories, 3 files'';
  };

  buildExecutable = testBuildIdris {
    testName = "executable-package";
    buildIdrisArgs = {
      ipkgName = "pkg";
      idrisLibraries = [ ];
      src = runCommand "executable-package-src" { } ''
        mkdir $out

        cat > $out/Main.idr <<EOF
        module Main

        main : IO ()
        main = putStrLn "hi"
        EOF

        cat > $out/pkg.ipkg <<EOF
        package pkg
        modules = Main
        main = Main
        executable = mypkg
        EOF
      '';
    };
    makeExecutable = true;
    expectedTree = ''
      `-- bin
          `-- mypkg

      2 directories, 1 file'';
  };
}