idris2Packages: QoL improvements, test coverage, nixfmt (#341387)

pkgs/development/compilers/idris2/build-idris.nix

@@ -1,4 +1,8 @@
-{ stdenv, lib, idris2, makeWrapper
+{
+  stdenv,
+  lib,
+  idris2,
+  makeBinaryWrapper,
 }:
 # Usage: let
 #          pkg = idris2Packages.buildIdris {
@@ -11,49 +15,57 @@
 #          bin = pkg.executable;
 #        }
 #
-{ src
-, ipkgName
-, version ? "unversioned"
-, idrisLibraries # Other libraries built with buildIdris
-, ... }@attrs:
+{
+  src,
+  ipkgName,
+  version ? "unversioned",
+  idrisLibraries, # Other libraries built with buildIdris
+  ...
+}@attrs:
 
 let
   # loop over idrisLibraries and normalize them by turning any that are
   # direct outputs of the buildIdris function into the `.library {}`
   # property.
-  idrisLibraryLibs = map (idrisLib:
-    if lib.isDerivation idrisLib
-    then idrisLib
-    else if builtins.isFunction idrisLib
-    then idrisLib {}
-    else if (builtins.isAttrs idrisLib && idrisLib ? "library")
-    then idrisLib.library {}
-    else throw "Found an Idris2 library dependency that was not the result of the buildIdris function"
+  idrisLibraryLibs = map (
+    idrisLib:
+    if lib.isDerivation idrisLib then
+      idrisLib
+    else if builtins.isFunction idrisLib then
+      idrisLib { }
+    else if (builtins.isAttrs idrisLib && idrisLib ? "library") then
+      idrisLib.library { }
+    else
+      throw "Found an Idris2 library dependency that was not the result of the buildIdris function"
   ) idrisLibraries;
 
-  propagate = libs: lib.unique (lib.concatMap (nextLib: [nextLib] ++ nextLib.propagatedIdrisLibraries) libs);
+  propagate =
+    libs: lib.unique (lib.concatMap (nextLib: [ nextLib ] ++ nextLib.propagatedIdrisLibraries) libs);
   ipkgFileName = ipkgName + ".ipkg";
   idrName = "idris2-${idris2.version}";
   libSuffix = "lib/${idrName}";
   propagatedIdrisLibraries = propagate idrisLibraryLibs;
-  libDirs =
-    (lib.makeSearchPath libSuffix propagatedIdrisLibraries) +
-    ":${idris2}/${idrName}";
+  libDirs = (lib.makeSearchPath libSuffix propagatedIdrisLibraries) + ":${idris2}/${idrName}";
   supportDir = "${idris2}/${idrName}/lib";
   drvAttrs = builtins.removeAttrs attrs [
     "ipkgName"
     "idrisLibraries"
   ];
 
-  derivation = stdenv.mkDerivation (finalAttrs:
-    drvAttrs // {
+  derivation = stdenv.mkDerivation (
+    finalAttrs:
+    drvAttrs
+    // {
       pname = ipkgName;
       inherit version;
       src = src;
-      nativeBuildInputs = [ idris2 makeWrapper ] ++ attrs.nativeBuildInputs or [];
-      buildInputs = propagatedIdrisLibraries ++ attrs.buildInputs or [];
+      nativeBuildInputs = [
+        idris2
+        makeBinaryWrapper
+      ] ++ attrs.nativeBuildInputs or [ ];
+      buildInputs = propagatedIdrisLibraries ++ attrs.buildInputs or [ ];
 
-      IDRIS2_PACKAGE_PATH = libDirs;
+      env.IDRIS2_PACKAGE_PATH = libDirs;
 
       buildPhase = ''
         runHook preBuild
@@ -63,15 +75,16 @@ let
 
       passthru = {
         inherit propagatedIdrisLibraries;
-      };
+      } // (attrs.passthru or { });
 
       shellHook = ''
-        export IDRIS2_PACKAGE_PATH="${finalAttrs.IDRIS2_PACKAGE_PATH}"
+        export IDRIS2_PACKAGE_PATH="${finalAttrs.env.IDRIS2_PACKAGE_PATH}"
       '';
     }
   );
 
-in {
+in
+{
   executable = derivation.overrideAttrs {
     installPhase = ''
       runHook preInstall
@@ -97,9 +110,14 @@ in {
     '';
   };
 
-  library = { withSource ? false }:
-    let installCmd = if withSource then "--install-with-src" else "--install";
-    in derivation.overrideAttrs {
+  library =
+    {
+      withSource ? false,
+    }:
+    let
+      installCmd = if withSource then "--install-with-src" else "--install";
+    in
+    derivation.overrideAttrs {
       installPhase = ''
         runHook preInstall
         mkdir -p $out/${libSuffix}

pkgs/development/compilers/idris2/default.nix

@@ -1,21 +1,8 @@
-{ callPackage
-, idris2Packages
-}:
-
-let
-in {
+{ callPackage }:
+{
   idris2 = callPackage ./idris2.nix { };
+  idris2Api = callPackage ./idris2-api.nix { };
   idris2Lsp = callPackage ./idris2-lsp.nix { };
 
   buildIdris = callPackage ./build-idris.nix { };
-
-  idris2Api = (idris2Packages.buildIdris {
-    inherit (idris2Packages.idris2) src version;
-    ipkgName = "idris2api";
-    idrisLibraries = [ ];
-    preBuild = ''
-      export IDRIS2_PREFIX=$out/lib
-      make src/IdrisPaths.idr
-    '';
-  }).library;
 }

pkgs/development/compilers/idris2/idris2-api.nix

@@ -0,0 +1,22 @@
+{ lib, idris2Packages }:
+let
+  inherit (idris2Packages) idris2 buildIdris;
+  apiPkg = buildIdris {
+    inherit (idris2) src version;
+    ipkgName = "idris2api";
+    idrisLibraries = [ ];
+    preBuild = ''
+      export IDRIS2_PREFIX=$out/lib
+      make src/IdrisPaths.idr
+    '';
+
+    meta = {
+      description = "Idris2 Compiler API Library";
+      homepage = "https://github.com/idris-lang/Idris2";
+      license = lib.licenses.bsd3;
+      maintainers = with lib.maintainers; [ mattpolzin ];
+      inherit (idris2.meta) platforms;
+    };
+  };
+in
+apiPkg.library { }

pkgs/development/compilers/idris2/idris2-lsp.nix

@@ -1,14 +1,21 @@
-{ lib, fetchFromGitHub, idris2Packages, makeWrapper }:
+{
+  lib,
+  fetchFromGitHub,
+  idris2Packages,
+  makeWrapper,
+}:
 
 let
-  globalLibraries = let
-    idrName = "idris2-${idris2Packages.idris2.version}";
-    libSuffix = "lib/${idrName}";
-  in [
-    "\\$HOME/.nix-profile/lib/${idrName}"
-    "/run/current-system/sw/lib/${idrName}"
-    "${idris2Packages.idris2}/${idrName}"
-  ];
+  globalLibraries =
+    let
+      idrName = "idris2-${idris2Packages.idris2.version}";
+      libSuffix = "lib/${idrName}";
+    in
+    [
+      "\\$HOME/.nix-profile/lib/${idrName}"
+      "/run/current-system/sw/lib/${idrName}"
+      "${idris2Packages.idris2}/${idrName}"
+    ];
   globalLibrariesPath = builtins.concatStringsSep ":" globalLibraries;
 
   inherit (idris2Packages) idris2Api;
@@ -16,10 +23,10 @@ let
     ipkgName = "lsp-lib";
     version = "2024-01-21";
     src = fetchFromGitHub {
-     owner = "idris-community";
-     repo = "LSP-lib";
-     rev = "03851daae0c0274a02d94663d8f53143a94640da";
-     hash = "sha256-ICW9oOOP70hXneJFYInuPY68SZTDw10dSxSPTW4WwWM=";
+      owner = "idris-community";
+      repo = "LSP-lib";
+      rev = "03851daae0c0274a02d94663d8f53143a94640da";
+      hash = "sha256-ICW9oOOP70hXneJFYInuPY68SZTDw10dSxSPTW4WwWM=";
     };
     idrisLibraries = [ ];
   };
@@ -28,12 +35,15 @@ let
     ipkgName = "idris2-lsp";
     version = "2024-01-21";
     src = fetchFromGitHub {
-       owner = "idris-community";
-       repo = "idris2-lsp";
-       rev = "a77ef2d563418925aa274fa29f06880dde43f4ec";
-       hash = "sha256-zjfVfkpiQS9AdmTfq0hYRSelJq5Caa9VGTuFLtSvl5o=";
+      owner = "idris-community";
+      repo = "idris2-lsp";
+      rev = "a77ef2d563418925aa274fa29f06880dde43f4ec";
+      hash = "sha256-zjfVfkpiQS9AdmTfq0hYRSelJq5Caa9VGTuFLtSvl5o=";
     };
-    idrisLibraries = [idris2Api lspLib];
+    idrisLibraries = [
+      idris2Api
+      lspLib
+    ];
 
     nativeBuildInputs = [ makeWrapper ];
     postInstall = ''
@@ -49,4 +59,5 @@ let
       maintainers = with maintainers; [ mattpolzin ];
     };
   };
-in lspPkg.executable
+in
+lspPkg.executable

pkgs/development/compilers/idris2/idris2.nix

@@ -1,29 +1,30 @@
 # Almost 1:1 copy of idris2's nix/package.nix. Some work done in their flake.nix
 # we do here instead.
-{ stdenv
-, lib
-, chez
-, chez-racket
-, clang
-, gmp
-, fetchFromGitHub
-, makeWrapper
-, gambit
-, nodejs
-, zsh
-, callPackage
+{
+  stdenv,
+  lib,
+  chez,
+  chez-racket,
+  clang,
+  gmp,
+  fetchFromGitHub,
+  makeWrapper,
+  gambit,
+  nodejs,
+  zsh,
+  callPackage,
 }:
 
 # NOTICE: An `idris2WithPackages` is available at: https://github.com/claymager/idris2-pkgs
 
 let
   platformChez =
-    if (stdenv.system == "x86_64-linux") || (lib.versionAtLeast chez.version "10.0.0")
-      then
-        chez
-      else
-        chez-racket;
-in stdenv.mkDerivation rec {
+    if (stdenv.system == "x86_64-linux") || (lib.versionAtLeast chez.version "10.0.0") then
+      chez
+    else
+      chez-racket;
+in
+stdenv.mkDerivation rec {
   pname = "idris2";
   version = "0.7.0";
 
@@ -35,56 +36,69 @@ in stdenv.mkDerivation rec {
   };
 
   strictDeps = true;
-  nativeBuildInputs = [ makeWrapper clang platformChez ]
-    ++ lib.optionals stdenv.isDarwin [ zsh ];
-  buildInputs = [ platformChez gmp ];
+  nativeBuildInputs = [
+    makeWrapper
+    clang
+    platformChez
+  ] ++ lib.optionals stdenv.isDarwin [ zsh ];
+  buildInputs = [
+    platformChez
+    gmp
+  ];
 
   prePatch = ''
     patchShebangs --build tests
   '';
 
-  makeFlags = [ "PREFIX=$(out)" ]
-    ++ lib.optional stdenv.isDarwin "OS=";
+  makeFlags = [ "PREFIX=$(out)" ] ++ lib.optional stdenv.isDarwin "OS=";
 
   # The name of the main executable of pkgs.chez is `scheme`
-  buildFlags = [ "bootstrap" "SCHEME=scheme" ];
+  buildFlags = [
+    "bootstrap"
+    "SCHEME=scheme"
+  ];
 
   checkTarget = "test";
-  nativeCheckInputs = [ gambit nodejs ]; # racket ];
+  nativeCheckInputs = [
+    gambit
+    nodejs
+  ]; # racket ];
   checkFlags = [ "INTERACTIVE=" ];
 
   # TODO: Move this into its own derivation, such that this can be changed
   #       without having to recompile idris2 every time.
-  postInstall = let
-    name = "${pname}-${version}";
-    globalLibraries = [
-      "\\$HOME/.nix-profile/lib/${name}"
-      "/run/current-system/sw/lib/${name}"
-      "$out/${name}"
-    ];
-    globalLibrariesPath = builtins.concatStringsSep ":" globalLibraries;
-  in ''
-    # Remove existing idris2 wrapper that sets incorrect LD_LIBRARY_PATH
-    rm $out/bin/idris2
-    # The only thing we need from idris2_app is the actual binary
-    mv $out/bin/idris2_app/idris2.so $out/bin/idris2
-    rm $out/bin/idris2_app/*
-    rmdir $out/bin/idris2_app
-    # idris2 needs to find scheme at runtime to compile
-    # idris2 installs packages with --install into the path given by
-    #   IDRIS2_PREFIX. We set that to a default of ~/.idris2, to mirror the
-    #   behaviour of the standard Makefile install.
-    # TODO: Make support libraries their own derivation such that
-    #       overriding LD_LIBRARY_PATH is unnecessary
-    wrapProgram "$out/bin/idris2" \
-      --set-default CHEZ "${platformChez}/bin/scheme" \
-      --run 'export IDRIS2_PREFIX=''${IDRIS2_PREFIX-"$HOME/.idris2"}' \
-      --suffix IDRIS2_LIBS ':' "$out/${name}/lib" \
-      --suffix IDRIS2_DATA ':' "$out/${name}/support" \
-      --suffix IDRIS2_PACKAGE_PATH ':' "${globalLibrariesPath}" \
-      --suffix DYLD_LIBRARY_PATH ':' "$out/${name}/lib" \
-      --suffix LD_LIBRARY_PATH ':' "$out/${name}/lib"
-  '';
+  postInstall =
+    let
+      name = "${pname}-${version}";
+      globalLibraries = [
+        "\\$HOME/.nix-profile/lib/${name}"
+        "/run/current-system/sw/lib/${name}"
+        "$out/${name}"
+      ];
+      globalLibrariesPath = builtins.concatStringsSep ":" globalLibraries;
+    in
+    ''
+      # Remove existing idris2 wrapper that sets incorrect LD_LIBRARY_PATH
+      rm $out/bin/idris2
+      # The only thing we need from idris2_app is the actual binary
+      mv $out/bin/idris2_app/idris2.so $out/bin/idris2
+      rm $out/bin/idris2_app/*
+      rmdir $out/bin/idris2_app
+      # idris2 needs to find scheme at runtime to compile
+      # idris2 installs packages with --install into the path given by
+      #   IDRIS2_PREFIX. We set that to a default of ~/.idris2, to mirror the
+      #   behaviour of the standard Makefile install.
+      # TODO: Make support libraries their own derivation such that
+      #       overriding LD_LIBRARY_PATH is unnecessary
+      wrapProgram "$out/bin/idris2" \
+        --set-default CHEZ "${platformChez}/bin/scheme" \
+        --run 'export IDRIS2_PREFIX=''${IDRIS2_PREFIX-"$HOME/.idris2"}' \
+        --suffix IDRIS2_LIBS ':' "$out/${name}/lib" \
+        --suffix IDRIS2_DATA ':' "$out/${name}/support" \
+        --suffix IDRIS2_PACKAGE_PATH ':' "${globalLibrariesPath}" \
+        --suffix DYLD_LIBRARY_PATH ':' "$out/${name}/lib" \
+        --suffix LD_LIBRARY_PATH ':' "$out/${name}/lib"
+    '';
 
   # Run package tests
   passthru.tests = callPackage ./tests.nix { inherit pname; };
@@ -94,7 +108,11 @@ in stdenv.mkDerivation rec {
     mainProgram = "idris2";
     homepage = "https://github.com/idris-lang/Idris2";
     license = lib.licenses.bsd3;
-    maintainers = with lib.maintainers; [ fabianhjr wchresta mattpolzin ];
+    maintainers = with lib.maintainers; [
+      fabianhjr
+      wchresta
+      mattpolzin
+    ];
     inherit (chez.meta) platforms;
   };
 }

pkgs/development/compilers/idris2/tests.nix

@@ -1,19 +1,36 @@
-{ stdenv, lib, pname, idris2, zsh }:
+{
+  stdenv,
+  runCommand,
+  lib,
+  pname,
+  idris2,
+  idris2Packages,
+  zsh,
+  tree,
+}:
 
 let
-  testCompileAndRun = {testName, code, want, packages ? []}: let
+  testCompileAndRun =
+    {
+      testName,
+      code,
+      want,
+      packages ? [ ],
+    }:
+    let
       packageString = builtins.concatStringsSep " " (map (p: "--package " + p) packages);
-    in stdenv.mkDerivation {
-      name = "${pname}-${testName}";
-      meta.timeout = 60;
+    in
+    runCommand "${pname}-${testName}"
+      {
+        meta.timeout = 60;
 
-      # with idris2 compiled binaries assume zsh is available on darwin, but that
-      # is not the case with pure nix environments. Thus, we need to include zsh
-      # 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 = ''
+        # with idris2 compiled binaries assume zsh is available on darwin, but that
+        # is not the case with pure nix environments. Thus, we need to include zsh
+        # 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 ];
+      }
+      ''
         set -eo pipefail
 
         cat > packageTest.idr <<HERE
@@ -33,10 +50,43 @@ let
 
         touch $out
       '';
-    };
-in {
+
+  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
@@ -48,7 +98,7 @@ in {
   };
 
   # Data.Vect.Sort is available via --package contrib
-  use-contrib = testCompileAndRun {
+  useContrib = testCompileAndRun {
     testName = "use-contrib";
     packages = [ "contrib" ];
     code = ''
@@ -65,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'';
+  };
 }