Idris2: Refactor default.nix
We take the idris2 projects version of the derivation. Originally, Idris2 did not maintain their own nix derivation, so we created our own. Now they maintain their own derivation, so we should try to keep ours as close to theirs. This change comes with the following differences: * support files are in its own output, instead of packaged with idris2 - This makes it necessary to provide --package for contrib and network !!! This is a breaking change !!! * IDIRS2_PREFIX is set to ~/.idris2 instead of pointing to nix-store - This makes --install work as expected for the user * Properly set IDRIS2_PACKAGE_PATH * non-linux platform uses chez-racket instead of chez
This commit is contained in:
parent
d36d401087
commit
205b0f2c5e
|
@ -252,6 +252,15 @@
|
||||||
set <literal>autoSubUidGidRange = true</literal>.
|
set <literal>autoSubUidGidRange = true</literal>.
|
||||||
</para>
|
</para>
|
||||||
</listitem>
|
</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>
|
<listitem>
|
||||||
<para>
|
<para>
|
||||||
<literal>services.thelounge.private</literal> was removed in
|
<literal>services.thelounge.private</literal> was removed in
|
||||||
|
|
|
@ -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`.
|
- 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.
|
- `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}
|
## Other Notable Changes {#sec-release-22.05-notable-changes}
|
||||||
|
|
|
@ -1,18 +1,27 @@
|
||||||
{ lib
|
# Almost 1:1 copy of idris2's nix/platform.nix. Some work done in their flake.nix
|
||||||
, stdenv
|
# we do here instead.
|
||||||
|
{ stdenv
|
||||||
|
, lib
|
||||||
|
, chez
|
||||||
|
, chez-racket
|
||||||
|
, clang
|
||||||
|
, gmp
|
||||||
, fetchFromGitHub
|
, fetchFromGitHub
|
||||||
, makeWrapper
|
, makeWrapper
|
||||||
, clang
|
, gambit
|
||||||
, chez
|
, nodejs
|
||||||
, gmp
|
|
||||||
, zsh
|
, zsh
|
||||||
, callPackage
|
, callPackage
|
||||||
}:
|
}:
|
||||||
|
|
||||||
# NOTICE: An `idris2WithPackages` is available at: https://github.com/claymager/idris2-pkgs
|
# 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
|
# Uses scheme to bootstrap the build of idris2
|
||||||
stdenv.mkDerivation rec {
|
in stdenv.mkDerivation rec {
|
||||||
pname = "idris2";
|
pname = "idris2";
|
||||||
version = "0.5.1";
|
version = "0.5.1";
|
||||||
|
|
||||||
|
@ -23,14 +32,10 @@ stdenv.mkDerivation rec {
|
||||||
sha256 = "sha256-6CTn8o5geWSesXO7vTrrV/2EOQ3f+nPQ2M5cem13ZSY=";
|
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;
|
strictDeps = true;
|
||||||
nativeBuildInputs = [ makeWrapper clang chez ]
|
nativeBuildInputs = [ makeWrapper clang platformChez ]
|
||||||
++ lib.optional stdenv.isDarwin [ zsh ];
|
++ lib.optional stdenv.isDarwin [ zsh ];
|
||||||
buildInputs = [ gmp ];
|
buildInputs = [ platformChez gmp ];
|
||||||
|
|
||||||
prePatch = ''
|
prePatch = ''
|
||||||
patchShebangs --build tests
|
patchShebangs --build tests
|
||||||
|
@ -43,44 +48,40 @@ stdenv.mkDerivation rec {
|
||||||
buildFlags = [ "bootstrap" "SCHEME=scheme" ];
|
buildFlags = [ "bootstrap" "SCHEME=scheme" ];
|
||||||
|
|
||||||
checkTarget = "test";
|
checkTarget = "test";
|
||||||
|
checkInputs = [ gambit nodejs ]; # racket ];
|
||||||
|
checkFlags = [ "INTERACTIVE=" ];
|
||||||
|
|
||||||
# TODO: Move this into its own derivation, such that this can be changed
|
# TODO: Move this into its own derivation, such that this can be changed
|
||||||
# without having to recompile idris2 every time.
|
# without having to recompile idris2 every time.
|
||||||
postInstall = let
|
postInstall = let
|
||||||
includedLibs = [ "base" "contrib" "network" "prelude" ];
|
|
||||||
name = "${pname}-${version}";
|
name = "${pname}-${version}";
|
||||||
packagePaths =
|
globalLibraries = [
|
||||||
builtins.map (l: "$out/${name}/${l}-${version}") includedLibs;
|
"\\$HOME/.nix-profile/lib/${name}"
|
||||||
additionalIdris2Paths = builtins.concatStringsSep ":" packagePaths;
|
"/run/current-system/sw/lib/${name}"
|
||||||
|
"$out/${name}"
|
||||||
|
];
|
||||||
|
globalLibrariesPath = builtins.concatStringsSep ":" globalLibraries;
|
||||||
in ''
|
in ''
|
||||||
# Remove existing idris2 wrapper that sets incorrect LD_LIBRARY_PATH
|
# Remove existing idris2 wrapper that sets incorrect LD_LIBRARY_PATH
|
||||||
rm $out/bin/idris2
|
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
|
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/*
|
rm $out/bin/idris2_app/*
|
||||||
rmdir $out/bin/idris2_app
|
rmdir $out/bin/idris2_app
|
||||||
|
|
||||||
# idris2 needs to find scheme at runtime to compile
|
# idris2 needs to find scheme at runtime to compile
|
||||||
# idris2 installs packages with --install into the path given by PREFIX.
|
# idris2 installs packages with --install into the path given by
|
||||||
# Since PREFIX is in nix-store, it is immutable so --install does not work.
|
# IDRIS2_PREFIX. We set that to a default of ~/.idris2, to mirror the
|
||||||
# If the user redefines PREFIX to be able to install packages, idris2 will
|
# behaviour of the standard Makefile install.
|
||||||
# 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.
|
|
||||||
# TODO: Make support libraries their own derivation such that
|
# TODO: Make support libraries their own derivation such that
|
||||||
# overriding LD_LIBRARY_PATH is unnecessary
|
# overriding LD_LIBRARY_PATH is unnecessary
|
||||||
# TODO: Maybe set IDRIS2_PREFIX to the users home directory
|
|
||||||
wrapProgram "$out/bin/idris2" \
|
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_LIBS ':' "$out/${name}/lib" \
|
||||||
--suffix IDRIS2_DATA ':' "$out/${name}/support" \
|
--suffix IDRIS2_DATA ':' "$out/${name}/support" \
|
||||||
--suffix IDRIS2_PATH ':' "${additionalIdris2Paths}" \
|
--suffix IDRIS2_PACKAGE_PATH ':' "${globalLibrariesPath}" \
|
||||||
--suffix ${if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH"} ':' "$out/${name}/lib"
|
--suffix DYLD_LIBRARY_PATH ':' "$out/${name}/lib" \
|
||||||
|
--suffix LD_LIBRARY_PATH ':' "$out/${name}/lib"
|
||||||
'';
|
'';
|
||||||
|
|
||||||
# Run package tests
|
# Run package tests
|
||||||
|
|
|
@ -50,6 +50,7 @@ in {
|
||||||
# Data.Vect.Sort is available via --package contrib
|
# Data.Vect.Sort is available via --package contrib
|
||||||
use-contrib = testCompileAndRun {
|
use-contrib = testCompileAndRun {
|
||||||
testName = "use-contrib";
|
testName = "use-contrib";
|
||||||
|
packages = [ "contrib" ];
|
||||||
code = ''
|
code = ''
|
||||||
module Main
|
module Main
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue