pkgs/development/compilers/idris2/tests.nix

   1 {
   2   stdenv,
   3   runCommand,
   4   lib,
   5   pname,
   6   idris2,
   7   idris2Packages,
   8   zsh,
   9   tree,
  10 }:
  11
  12 let
  13   testCompileAndRun =
  14     {
  15       testName,
  16       code,
  17       want,
  18       packages ? [ ],
  19     }:
  20     let
  21       packageString = builtins.concatStringsSep " " (map (p: "--package " + p) packages);
  22     in
  23     runCommand "${pname}-${testName}"
  24       {
  25         meta.timeout = 60;
  26
  27         # with idris2 compiled binaries assume zsh is available on darwin, but that
  28         # is not the case with pure nix environments. Thus, we need to include zsh
  29         # when we build for darwin in tests. While this is impure, this is also what
  30         # we find in real darwin hosts.
  31         nativeBuildInputs = lib.optionals stdenv.hostPlatform.isDarwin [ zsh ];
  32       }
  33       ''
  34         set -eo pipefail
  35
  36         cat > packageTest.idr <<HERE
  37         ${code}
  38         HERE
  39
  40         ${idris2}/bin/idris2 ${packageString} -o packageTest packageTest.idr
  41
  42         GOT=$(./build/exec/packageTest)
  43
  44         if [ "$GOT" = "${want}" ]; then
  45           echo "${testName} SUCCESS: '$GOT' = '${want}'"
  46         else
  47           >&2 echo "Got '$GOT', want: '${want}'"
  48           exit 1
  49         fi
  50
  51         touch $out
  52       '';
  53
  54   testBuildIdris =
  55     {
  56       testName,
  57       buildIdrisArgs,
  58       # function that takes result of `buildIdris` and transforms it (commonly
  59       # by calling `.executable` or `.library {}` upon it):
  60       transformBuildIdrisOutput,
  61       expectedTree,
  62     }:
  63     let
  64       idrisPkg = transformBuildIdrisOutput (idris2Packages.buildIdris buildIdrisArgs);
  65     in
  66     runCommand "${pname}-${testName}"
  67       {
  68         meta.timeout = 60;
  69
  70         nativeBuildInputs = [ tree ];
  71       }
  72       ''
  73         GOT="$(tree ${idrisPkg} | tail -n +2)"
  74
  75         if [ "$GOT" = '${expectedTree}' ]; then
  76           echo "${testName} SUCCESS"
  77         else
  78           >&2 echo "Got:
  79           $GOT"
  80           >&2 echo 'want:
  81           ${expectedTree}'
  82           exit 1
  83         fi
  84
  85         touch $out
  86       '';
  87 in
  88 {
  89   # Simple hello world compiles, runs and outputs as expected
  90   helloWorld = testCompileAndRun {
  91     testName = "hello-world";
  92     code = ''
  93       module Main
  94
  95       main : IO ()
  96       main = putStrLn "Hello World!"
  97     '';
  98     want = "Hello World!";
  99   };
 100
 101   # Data.Vect.Sort is available via --package contrib
 102   useContrib = testCompileAndRun {
 103     testName = "use-contrib";
 104     packages = [ "contrib" ];
 105     code = ''
 106       module Main
 107
 108       import Data.Vect
 109       import Data.Vect.Sort  -- from contrib
 110
 111       vect : Vect 3 Int
 112       vect = 3 :: 1 :: 5 :: Nil
 113
 114       main : IO ()
 115       main = putStrLn $ show (sort vect)
 116     '';
 117     want = "[1, 3, 5]";
 118   };
 119
 120   buildLibrary = testBuildIdris {
 121     testName = "library-package";
 122     buildIdrisArgs = {
 123       ipkgName = "pkg";
 124       idrisLibraries = [ idris2Packages.idris2Api ];
 125       src = runCommand "library-package-src" { } ''
 126         mkdir $out
 127
 128         cat > $out/Main.idr <<EOF
 129         module Main
 130
 131         import Compiler.ANF -- from Idris2Api
 132
 133         hello : String
 134         hello = "world"
 135         EOF
 136
 137         cat > $out/pkg.ipkg <<EOF
 138         package pkg
 139         modules = Main
 140         depends = idris2
 141         EOF
 142       '';
 143     };
 144     transformBuildIdrisOutput = pkg: pkg.library { withSource = false; };
 145     expectedTree = ''
 146       `-- lib
 147           `-- idris2-0.7.0
 148               `-- pkg-0
 149                   |-- 2023090800
 150                   |   |-- Main.ttc
 151                   |   `-- Main.ttm
 152                   `-- pkg.ipkg
 153
 154       5 directories, 3 files'';
 155   };
 156
 157   buildLibraryWithSource = testBuildIdris {
 158     testName = "library-with-source-package";
 159     buildIdrisArgs = {
 160       ipkgName = "pkg";
 161       idrisLibraries = [ idris2Packages.idris2Api ];
 162       src = runCommand "library-package-src" { } ''
 163         mkdir $out
 164
 165         cat > $out/Main.idr <<EOF
 166         module Main
 167
 168         import Compiler.ANF -- from Idris2Api
 169
 170         hello : String
 171         hello = "world"
 172         EOF
 173
 174         cat > $out/pkg.ipkg <<EOF
 175         package pkg
 176         modules = Main
 177         depends = idris2
 178         EOF
 179       '';
 180     };
 181     transformBuildIdrisOutput = pkg: pkg.library { withSource = true; };
 182     expectedTree = ''
 183       `-- lib
 184           `-- idris2-0.7.0
 185               `-- pkg-0
 186                   |-- 2023090800
 187                   |   |-- Main.ttc
 188                   |   `-- Main.ttm
 189                   |-- Main.idr
 190                   `-- pkg.ipkg
 191
 192       5 directories, 4 files'';
 193   };
 194
 195   buildLibraryWithSourceRetroactively = testBuildIdris {
 196     testName = "library-with-source-retro-package";
 197     buildIdrisArgs = {
 198       ipkgName = "pkg";
 199       idrisLibraries = [ idris2Packages.idris2Api ];
 200       src = runCommand "library-package-src" { } ''
 201         mkdir $out
 202
 203         cat > $out/Main.idr <<EOF
 204         module Main
 205
 206         import Compiler.ANF -- from Idris2Api
 207
 208         hello : String
 209         hello = "world"
 210         EOF
 211
 212         cat > $out/pkg.ipkg <<EOF
 213         package pkg
 214         modules = Main
 215         depends = idris2
 216         EOF
 217       '';
 218     };
 219     transformBuildIdrisOutput = pkg: pkg.library'.withSource;
 220     expectedTree = ''
 221       `-- lib
 222           `-- idris2-0.7.0
 223               `-- pkg-0
 224                   |-- 2023090800
 225                   |   |-- Main.ttc
 226                   |   `-- Main.ttm
 227                   |-- Main.idr
 228                   `-- pkg.ipkg
 229
 230       5 directories, 4 files'';
 231   };
 232
 233   buildExecutable = testBuildIdris {
 234     testName = "executable-package";
 235     buildIdrisArgs = {
 236       ipkgName = "pkg";
 237       idrisLibraries = [ ];
 238       src = runCommand "executable-package-src" { } ''
 239         mkdir $out
 240
 241         cat > $out/Main.idr <<EOF
 242         module Main
 243
 244         main : IO ()
 245         main = putStrLn "hi"
 246         EOF
 247
 248         cat > $out/pkg.ipkg <<EOF
 249         package pkg
 250         modules = Main
 251         main = Main
 252         executable = mypkg
 253         EOF
 254       '';
 255     };
 256     transformBuildIdrisOutput = pkg: pkg.executable;
 257     expectedTree = ''
 258       `-- bin
 259           `-- mypkg
 260
 261       2 directories, 1 file'';
 262   };
 263 }