Merge pull request #154052 from wchresta/idris2-use-project-derivation

Idris2: Refactor default.nix

nixos/doc/manual/from_md/release-notes/rl-2205.section.xml

@@ -252,6 +252,15 @@
           set <literal>autoSubUidGidRange = true</literal>.
         </para>
       </listitem>
+      <listitem>
+        <para>
+          <literal>idris2</literal> now requires
+          <literal>--package</literal> when using packages
+          <literal>contrib</literal> and <literal>network</literal>,
+          while previously these idris2 packages were automatically
+          loaded.
+        </para>
+      </listitem>
       <listitem>
         <para>
           <literal>services.thelounge.private</literal> was removed in

nixos/doc/manual/release-notes/rl-2205.section.md

@@ -83,6 +83,8 @@ In addition to numerous new and upgraded packages, this release has the followin
 
 - Normal users (with `isNormalUser = true`) which have non-empty `subUidRanges` or `subGidRanges` set no longer have additional implicit ranges allocated. To enable automatic allocation back set `autoSubUidGidRange = true`.
 
+- `idris2` now requires `--package` when using packages `contrib` and `network`, while previously these idris2 packages were automatically loaded.
+
 - `services.thelounge.private` was removed in favor of `services.thelounge.public`, to follow with upstream changes.
 
 ## Other Notable Changes {#sec-release-22.05-notable-changes}

pkgs/development/compilers/idris2/default.nix

@@ -1,18 +1,27 @@
-{ lib
-, stdenv
+# Almost 1:1 copy of idris2's nix/platform.nix. Some work done in their flake.nix
+# we do here instead.
+{ stdenv
+, lib
+, chez
+, chez-racket
+, clang
+, gmp
 , fetchFromGitHub
 , makeWrapper
-, clang
-, chez
-, gmp
+, gambit
+, nodejs
 , zsh
 , callPackage
 }:
 
 # NOTICE: An `idris2WithPackages` is available at: https://github.com/claymager/idris2-pkgs
 
+let
+  # Taken from Idris2/idris2/flake.nix. Check if the idris2 project does it this
+  # way, still, every now and then.
+  platformChez = if stdenv.system == "x86_64-linux" then chez else chez-racket;
 # Uses scheme to bootstrap the build of idris2
-stdenv.mkDerivation rec {
+in stdenv.mkDerivation rec {
   pname = "idris2";
   version = "0.5.1";
 
@@ -23,14 +32,10 @@ stdenv.mkDerivation rec {
     sha256 = "sha256-6CTn8o5geWSesXO7vTrrV/2EOQ3f+nPQ2M5cem13ZSY=";
   };
 
-  # We do not add any propagatedNativeBuildInputs because we do not want the
-  # executables idris2 produces to depend on the nix-store. As such, it is left
-  # to the user to guarantee chez (or any other codgen dependency) is available
-  # in the path during compilation of programs with idris2.
   strictDeps = true;
-  nativeBuildInputs = [ makeWrapper clang chez ]
+  nativeBuildInputs = [ makeWrapper clang platformChez ]
     ++ lib.optional stdenv.isDarwin [ zsh ];
-  buildInputs = [ gmp ];
+  buildInputs = [ platformChez gmp ];
 
   prePatch = ''
     patchShebangs --build tests
@@ -43,44 +48,40 @@ stdenv.mkDerivation rec {
   buildFlags = [ "bootstrap" "SCHEME=scheme" ];
 
   checkTarget = "test";
+  checkInputs = [ 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
-    includedLibs = [ "base" "contrib" "network" "prelude" ];
     name = "${pname}-${version}";
-    packagePaths =
-      builtins.map (l: "$out/${name}/${l}-${version}") includedLibs;
-    additionalIdris2Paths = builtins.concatStringsSep ":" packagePaths;
+    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
-    # Move actual idris2 binary
+    # The only thing we need from idris2_app is the actual binary
     mv $out/bin/idris2_app/idris2.so $out/bin/idris2
-
-    # After moving the binary, there is nothing left in idris2_app that isn't
-    # either contained in lib/ or is useless to us.
     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 PREFIX.
-    # Since PREFIX is in nix-store, it is immutable so --install does not work.
-    # If the user redefines PREFIX to be able to install packages, idris2 will
-    # not find the libraries and packages since all paths are relative to
-    # PREFIX by default.
-    # We explicitly make all paths to point to nix-store, such that they are
-    # independent of what IDRIS2_PREFIX is. This allows the user to redefine
-    # IDRIS2_PREFIX and use --install as expected.
+    # 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
-    # TODO: Maybe set IDRIS2_PREFIX to the users home directory
     wrapProgram "$out/bin/idris2" \
-      --set-default CHEZ "${chez}/bin/scheme" \
+      --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_PATH ':' "${additionalIdris2Paths}" \
-      --suffix ${if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH"} ':' "$out/${name}/lib"
+      --suffix IDRIS2_PACKAGE_PATH ':' "${globalLibrariesPath}" \
+      --suffix DYLD_LIBRARY_PATH ':' "$out/${name}/lib" \
+      --suffix LD_LIBRARY_PATH ':' "$out/${name}/lib"
   '';
 
   # Run package tests

pkgs/development/compilers/idris2/tests.nix

@@ -50,6 +50,7 @@ in {
   # Data.Vect.Sort is available via --package contrib
   use-contrib = testCompileAndRun {
     testName = "use-contrib";
+    packages = [ "contrib" ];
     code = ''
       module Main