From d7a058e6f74f03b72d3c85df8ffcf1edf2aab3e7 Mon Sep 17 00:00:00 2001 From: Mathew Polzin Date: Tue, 2 Jan 2024 10:38:06 -0600 Subject: [PATCH 1/3] idris2: add api package and buildIdris helper --- .../compilers/idris2/build-idris.nix | 73 ++++++++++++ pkgs/development/compilers/idris2/default.nix | 105 +++--------------- pkgs/development/compilers/idris2/idris2.nix | 97 ++++++++++++++++ pkgs/top-level/all-packages.nix | 4 +- 4 files changed, 187 insertions(+), 92 deletions(-) create mode 100644 pkgs/development/compilers/idris2/build-idris.nix create mode 100644 pkgs/development/compilers/idris2/idris2.nix diff --git a/pkgs/development/compilers/idris2/build-idris.nix b/pkgs/development/compilers/idris2/build-idris.nix new file mode 100644 index 000000000000..c299128aa526 --- /dev/null +++ b/pkgs/development/compilers/idris2/build-idris.nix @@ -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 + ]); +} diff --git a/pkgs/development/compilers/idris2/default.nix b/pkgs/development/compilers/idris2/default.nix index 4bac5d33b1eb..8a2d28eb1ce0 100644 --- a/pkgs/development/compilers/idris2/default.nix +++ b/pkgs/development/compilers/idris2/default.nix @@ -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"; +in { + idris2 = callPackage ./idris2.nix { }; - src = fetchFromGitHub { - owner = "idris-lang"; - repo = "Idris2"; - rev = "v${version}"; - sha256 = "sha256-VwveX3fZfrxEsytpbOc5Tm6rySpLFhTt5132J6rmrmM="; - }; + buildIdris = callPackage ./build-idris.nix { }; - 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; - }; + idris2Api = (idris2Packages.buildIdris { + inherit (idris2Packages.idris2) src; + projectName = "idris2api"; + idrisLibraries = [ ]; + preBuild = '' + export IDRIS2_PREFIX=$out/lib + make src/IdrisPaths.idr + ''; + }).library; } diff --git a/pkgs/development/compilers/idris2/idris2.nix b/pkgs/development/compilers/idris2/idris2.nix new file mode 100644 index 000000000000..fc72bffb3847 --- /dev/null +++ b/pkgs/development/compilers/idris2/idris2.nix @@ -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; + }; +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index eae59a992506..788af0b82343 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -16379,7 +16379,9 @@ with pkgs; idris = idrisPackages.with-packages [ idrisPackages.base ] ; - idris2 = callPackage ../development/compilers/idris2 { }; + idris2Packages = recurseIntoAttrs (callPackage ../development/compilers/idris2 { }); + + inherit (idris2Packages) idris2; inherit (callPackage ../development/tools/database/indradb { }) indradb-server From ce58e0643bd5939a51f2de13b8987f6b1be4898a Mon Sep 17 00:00:00 2001 From: Mathew Polzin Date: Tue, 2 Jan 2024 19:04:10 -0600 Subject: [PATCH 2/3] doc: idris2 section --- doc/languages-frameworks/idris2.section.md | 47 ++++++++++++++++++++++ doc/languages-frameworks/index.md | 1 + 2 files changed, 48 insertions(+) create mode 100644 doc/languages-frameworks/idris2.section.md diff --git a/doc/languages-frameworks/idris2.section.md b/doc/languages-frameworks/idris2.section.md new file mode 100644 index 000000000000..47bcbf46aee9 --- /dev/null +++ b/doc/languages-frameworks/idris2.section.md @@ -0,0 +1,47 @@ +# Idris2 {#sec-idris2} + +In addition to exposing the Idris2 compiler itself, Nixpkgs exposes an `idris2Packages.buildIdris` helper to make it a bit more ergonomic to build Idris2 executables or libraries. + +The `buildIdris` function takes a package set that defines at a minimum the `src` and `projectName` of the package to be built and any `idrisLibraries` required to build it. The `src` is the same source you're familiar with but the `projectName` must be the name of the `ipkg` file for the project (omitting the `.ipkg` extension). The `idrisLibraries` is a list of other library derivations created with `buildIdris`. You can optionally specify other derivation properties as needed but sensible defaults for `configurePhase`, `buildPhase`, and `installPhase` are provided. + +Importantly, `buildIdris` does not create a single derivation but rather an attribute set with two properties: `executable` and `library`. The `executable` property is a derivation and the `library` property is a function that will return a derivation for the library with or without source code included. Source code need not be included unless you are aiming to use IDE or LSP features that are able to jump to definitions within an editor. + +A simple example of a fully packaged library would be the [`LSP-lib`](https://github.com/idris-community/LSP-lib) found in the `idris-community` GitHub organization. +```nix +{ fetchFromGitHub, idris2Packages }: +let lspLibPkg = idris2Packages.buildIdris { + projectName = "lsp-lib"; + src = fetchFromGitHub { + owner = "idris-community"; + repo = "LSP-lib"; + rev = "main"; + hash = "sha256-EvSyMCVyiy9jDZMkXQmtwwMoLaem1GsKVFqSGNNHHmY="; + }; + idrisLibraries = [ ]; +}; +in lspLibPkg.library +``` + +The above results in a derivation with the installed library results (with sourcecode). + +A slightly more involved example of a fully packaged executable would be the [`idris2-lsp`](https://github.com/idris-community/idris2-lsp) which is an Idris2 language server that uses the `LSP-lib` found above. +```nix +{ callPackage, fetchFromGitHub, idris2Packages }: + +# Assuming the previous example lives in `lsp-lib.nix`: +let lspLib = callPackage ./lsp-lib.nix { }; + lspPkg = idris2Packages.buildIdris { + projectName = "idris2-lsp"; + src = fetchFromGitHub { + owner = "idris-community"; + repo = "idris2-lsp"; + rev = "main"; + hash = "sha256-vQTzEltkx7uelDtXOHc6QRWZ4cSlhhm5ziOqWA+aujk="; + }; + idrisLibraries = [(idris2Packages.idris2Api { }) (lspLib { })]; + }; +in lspPkg.executable +``` + +The above uses the default value of `withSource = false` for both of the two required Idris libraries that the `idris2-lsp` executable depends on. `idris2Api` in the above derivation comes built in with `idris2Packages`. This library exposes many of the otherwise internal APIs of the Idris2 compiler. + diff --git a/doc/languages-frameworks/index.md b/doc/languages-frameworks/index.md index f177de507841..67107fb5b687 100644 --- a/doc/languages-frameworks/index.md +++ b/doc/languages-frameworks/index.md @@ -21,6 +21,7 @@ go.section.md haskell.section.md hy.section.md idris.section.md +idris2.section.md ios.section.md java.section.md javascript.section.md From f3c916f9090dc461c59f807ddcd756ca43a166cd Mon Sep 17 00:00:00 2001 From: Mathew Polzin Date: Mon, 15 Jan 2024 18:20:58 -0600 Subject: [PATCH 3/3] idris2: add mattpolzin as a maintainer --- pkgs/development/compilers/idris2/idris2.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/development/compilers/idris2/idris2.nix b/pkgs/development/compilers/idris2/idris2.nix index fc72bffb3847..88c4d05703cf 100644 --- a/pkgs/development/compilers/idris2/idris2.nix +++ b/pkgs/development/compilers/idris2/idris2.nix @@ -91,7 +91,7 @@ in stdenv.mkDerivation rec { 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 ]; + maintainers = with lib.maintainers; [ fabianhjr wchresta mattpolzin ]; inherit (chez.meta) platforms; }; }