-
-
Notifications
You must be signed in to change notification settings - Fork 13.7k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
idris2: add api package and buildIdris helper
- Loading branch information
1 parent
fad7e7e
commit d7a058e
Showing
4 changed files
with
189 additions
and
94 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,73 @@ | ||
{ stdenv, lib, idris2 | ||
}: | ||
# Usage: let | ||
# pkg = idris2Packages.buildIdris { | ||
# src = ...; | ||
# projectName = "my-pkg"; | ||
# idrisLibraries = [ ]; | ||
# }; | ||
# in { | ||
# lib = pkg.library { withSource = true; }; | ||
# bin = pkg.executable; | ||
# } | ||
# | ||
{ src | ||
, projectName | ||
, idrisLibraries # Other libraries built with buildIdris | ||
, ... }@attrs: | ||
|
||
let | ||
ipkgName = projectName + ".ipkg"; | ||
idrName = "idris2-${idris2.version}"; | ||
libSuffix = "lib/${idrName}"; | ||
libDirs = | ||
lib.makeSearchPath libSuffix idrisLibraries; | ||
drvAttrs = builtins.removeAttrs attrs [ "idrisLibraries" ]; | ||
|
||
sharedAttrs = { | ||
name = projectName; | ||
src = src; | ||
nativeBuildInputs = [ idris2 ]; | ||
|
||
IDRIS2_PACKAGE_PATH = libDirs; | ||
|
||
configurePhase = '' | ||
runHook preConfigure | ||
runHook postConfigure | ||
''; | ||
|
||
buildPhase = '' | ||
runHook preBuild | ||
idris2 --build ${ipkgName} | ||
runHook postBuild | ||
''; | ||
}; | ||
|
||
in { | ||
executable = stdenv.mkDerivation (lib.attrsets.mergeAttrsList [ | ||
sharedAttrs | ||
{ installPhase = '' | ||
runHook preInstall | ||
mkdir -p $out/bin | ||
mv build/exec/* $out/bin | ||
runHook postInstall | ||
''; | ||
} | ||
drvAttrs | ||
]); | ||
library = { withSource ? false }: | ||
let installCmd = if withSource then "--install-with-src" else "--install"; | ||
in stdenv.mkDerivation (lib.attrsets.mergeAttrsList [ | ||
sharedAttrs | ||
{ | ||
installPhase = '' | ||
runHook preInstall | ||
mkdir -p $out/${libSuffix} | ||
export IDRIS2_PREFIX=$out/lib | ||
idris2 ${installCmd} ${ipkgName} | ||
runHook postInstall | ||
''; | ||
} | ||
drvAttrs | ||
]); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,97 +1,20 @@ | ||
# 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 | ||
, gambit | ||
, nodejs | ||
, zsh | ||
, callPackage | ||
{ callPackage | ||
, idris2Packages | ||
}: | ||
|
||
# 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 | ||
in stdenv.mkDerivation rec { | ||
pname = "idris2"; | ||
version = "0.7.0"; | ||
|
||
src = fetchFromGitHub { | ||
owner = "idris-lang"; | ||
repo = "Idris2"; | ||
rev = "v${version}"; | ||
sha256 = "sha256-VwveX3fZfrxEsytpbOc5Tm6rySpLFhTt5132J6rmrmM="; | ||
}; | ||
|
||
strictDeps = true; | ||
nativeBuildInputs = [ makeWrapper clang platformChez ] | ||
++ lib.optionals stdenv.isDarwin [ zsh ]; | ||
buildInputs = [ platformChez gmp ]; | ||
|
||
prePatch = '' | ||
patchShebangs --build tests | ||
''; | ||
|
||
makeFlags = [ "PREFIX=$(out)" ] | ||
++ lib.optional stdenv.isDarwin "OS="; | ||
|
||
# The name of the main executable of pkgs.chez is `scheme` | ||
buildFlags = [ "bootstrap" "SCHEME=scheme" ]; | ||
|
||
checkTarget = "test"; | ||
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" | ||
''; | ||
|
||
# Run package tests | ||
passthru.tests = callPackage ./tests.nix { inherit pname; }; | ||
|
||
meta = { | ||
description = "A purely functional programming language with first class types"; | ||
homepage = "https://github.com/idris-lang/Idris2"; | ||
license = lib.licenses.bsd3; | ||
maintainers = with lib.maintainers; [ fabianhjr wchresta ]; | ||
inherit (chez.meta) platforms; | ||
}; | ||
in { | ||
idris2 = callPackage ./idris2.nix { }; | ||
|
||
buildIdris = callPackage ./build-idris.nix { }; | ||
|
||
idris2Api = (idris2Packages.buildIdris { | ||
inherit (idris2Packages.idris2) src; | ||
projectName = "idris2api"; | ||
idrisLibraries = [ ]; | ||
preBuild = '' | ||
export IDRIS2_PREFIX=$out/lib | ||
make src/IdrisPaths.idr | ||
''; | ||
}).library; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,97 @@ | ||
# 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 | ||
}: | ||
|
||
# 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 | ||
in stdenv.mkDerivation rec { | ||
pname = "idris2"; | ||
version = "0.7.0"; | ||
|
||
src = fetchFromGitHub { | ||
owner = "idris-lang"; | ||
repo = "Idris2"; | ||
rev = "v${version}"; | ||
sha256 = "sha256-VwveX3fZfrxEsytpbOc5Tm6rySpLFhTt5132J6rmrmM="; | ||
}; | ||
|
||
strictDeps = true; | ||
nativeBuildInputs = [ makeWrapper clang platformChez ] | ||
++ lib.optionals stdenv.isDarwin [ zsh ]; | ||
buildInputs = [ platformChez gmp ]; | ||
|
||
prePatch = '' | ||
patchShebangs --build tests | ||
''; | ||
|
||
makeFlags = [ "PREFIX=$(out)" ] | ||
++ lib.optional stdenv.isDarwin "OS="; | ||
|
||
# The name of the main executable of pkgs.chez is `scheme` | ||
buildFlags = [ "bootstrap" "SCHEME=scheme" ]; | ||
|
||
checkTarget = "test"; | ||
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" | ||
''; | ||
|
||
# Run package tests | ||
passthru.tests = callPackage ./tests.nix { inherit pname; }; | ||
|
||
meta = { | ||
description = "A purely functional programming language with first class types"; | ||
homepage = "https://github.com/idris-lang/Idris2"; | ||
license = lib.licenses.bsd3; | ||
maintainers = with lib.maintainers; [ fabianhjr wchresta ]; | ||
inherit (chez.meta) platforms; | ||
}; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters