Added new nix functionalities (#1154)

.github/workflows/ci-nix.yml

@@ -20,4 +20,4 @@ jobs:
         install_url: https://github.com/numtide/nix-flakes-installer/releases/download/nix-2.4pre20210126_f15f0b8/install
         extra_nix_config: |
           experimental-features = nix-command flakes
-    - run: nix build
+    - run: nix flake check

.gitignore

@@ -1,4 +1,5 @@
 idris2docs_venv
+result
 *~
 *.ibc
 *.ttc

INSTALL.md

@@ -16,7 +16,7 @@ The requirements are:
   with `pkg_add coreutils gmake` command.
 
 On Windows, it has been reported that installing via `MSYS2` works
-(https://www.msys2.org/). On Windows older than Windows 8, you may need to
+[MSYS2](https://www.msys2.org/). On Windows older than Windows 8, you may need to
 set an environment variable `OLD_WIN=1` or modify it in `config.mk`.
 
 On Raspberry Pi, you can bootstrap via Racket.
@@ -126,3 +126,11 @@ by running the following command:
 If you are a [nix flakes](https://nixos.wiki/wiki/Flakes) user you can install Idris 2 together with all the requirements by running the following command:
 
     nix profile install github:idris-lang/Idris2
+
+## Running in text editor
+
+### Run on emacs using nix flakes
+
+If you are a [nix flakes](https://nixos.wiki/wiki/Flakes) user you can run Idris 2 in emacs by running the following command:
+
+    nix run idris-lang/Idris2#emacs-with-idris idrisCode.idr

default.nix

@@ -1,3 +1,3 @@
-{ nixpkgs ? import <nixos> {} }: with nixpkgs;
-
-callPackage ./package.nix {}
+(import (fetchTarball https://github.com/edolstra/flake-compat/archive/master.tar.gz) {
+  src = builtins.fetchGit ./.;
+}).defaultNix

flake.lock

@@ -1,12 +1,43 @@
 {
   "nodes": {
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1614513358,
+        "narHash": "sha256-LakhOx3S1dRjnh0b5Dg3mbZyH0ToC9I8Y2wKSkBaTzU=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "5466c5bbece17adaab2d82fae80b46e807611bf3",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "idris-emacs-src": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1613351183,
+        "narHash": "sha256-ngg48SzrR2LCtjle3WR3BOK86USRB0ZXmgXWu9EzQbo=",
+        "owner": "redfish64",
+        "repo": "idris2-mode",
+        "rev": "77390611a934f13e03a45e9f8a4e476dd17a9c5b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "redfish64",
+        "repo": "idris2-mode",
+        "type": "github"
+      }
+    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1608233493,
-        "narHash": "sha256-erk1llMWMpSoUrnjHUY99FSP1mexMwjdPS7xaSQT0kk=",
+        "lastModified": 1614810944,
+        "narHash": "sha256-mDpk7kP5nRRMhXZDjGQUIoq+3mUgixPXt93md0fI46E=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "2fe2d0aeea8e7a14f4ef843755e2cb9e12d9085a",
+        "rev": "d485a4db259470c19872ef6bf13ef4a0c5b2bb3c",
         "type": "github"
       },
       "original": {
@@ -16,6 +47,8 @@
     },
     "root": {
       "inputs": {
+        "flake-utils": "flake-utils",
+        "idris-emacs-src": "idris-emacs-src",
         "nixpkgs": "nixpkgs"
       }
     }

flake.nix

@@ -1,11 +1,43 @@
 {
   description = "Idris2 flake";
 
-  outputs = { self, nixpkgs }: {
-
-    packages.x86_64-linux.idris2 = import ./default.nix { nixpkgs = nixpkgs.legacyPackages.x86_64-linux; };
-
-    defaultPackage.x86_64-linux = self.packages.x86_64-linux.idris2;
-
+  inputs.flake-utils.url = github:numtide/flake-utils;
+  inputs.idris-emacs-src = {
+    url = github:redfish64/idris2-mode;
+    flake = false;
   };
+
+  outputs = { self, nixpkgs, flake-utils, idris-emacs-src }:
+    let idris2-version = "0.3.0";
+    in flake-utils.lib.eachDefaultSystem (system:
+      let pkgs = import nixpkgs { inherit system; };
+          idris2Pkg = pkgs.callPackage ./nix/package.nix { inherit idris2-version; };
+          text-editor = import ./nix/text-editor.nix { inherit pkgs idris-emacs-src idris2Pkg; };
+          buildIdrisPkg = { projectName, src, idrisLibraries }:
+            pkgs.callPackage ./nix/buildIdris.nix
+              { inherit src projectName idrisLibraries idris2-version; idris2 = idris2Pkg; };
+      in if system != "aarch64-linux" then rec {
+        checks = with pkgs; import ./nix/test.nix
+          { inherit nixpkgs flake-utils system stdenv runCommand lib; idris = self; };
+        packages = rec {
+          idris2 = idris2Pkg;
+        } // text-editor;
+        apps = rec {
+          type = "app";
+          emacs-dev = text-editor.emacs-dev;
+        };
+        buildIdris = buildIdrisPkg;
+        defaultPackage = packages.idris2;
+      } else {}) // rec {
+        templates.pkg = {
+          path = ./nix/templates/pkg;
+          description = "A custom Idris 2 package";
+        };
+        templates.pkgWithDeps = {
+          path = ./nix/templates/pkgWithDeps;
+          description = "A custom Idris 2 package with dependencies";
+        };
+        defaultTemplate = templates.pkg;
+        version = idris2-version;
+      };
 }

nix/buildIdris.nix

@@ -0,0 +1,42 @@
+{ stdenv
+, lib
+, projectName
+, src
+, idris2
+, idris2-version
+, idrisLibraries
+}:
+with lib.strings;
+let
+  ipkgName = projectName + ".ipkg";
+  libSuffix = "lib/${idrName}";
+  idrName = "idris2-${idris2-version}";
+  lib-dirs = concatMapStringsSep ":" (p: "${p}/${libSuffix}") idrisLibraries;
+in
+rec {
+  build = stdenv.mkDerivation {
+    name = projectName;
+    src = src;
+    buildInputs = [ idris2 ];
+    configurePhase = ''
+      export IDRIS2_PACKAGE_PATH=${lib-dirs}
+    '';
+    buildPhase = ''
+      idris2 --build ${ipkgName}
+    '';
+    installPhase = ''
+      mkdir -p $out/bin
+      mv build/exec/* $out/bin
+    '';
+  };
+  installLibrary = build.overrideAttrs (oldAttrs: {
+    buildPhase = "";
+    installPhase = let
+      ipkgName = projectName + ".ipkg";
+    in ''
+      mkdir -p $out/${libSuffix}
+      export IDRIS2_PREFIX=$out/lib
+      idris2 --install ${ipkgName}
+    '';
+  });
+}

nix/init.el

@@ -0,0 +1 @@
+(require 'idris2-mode)

nix/package.nix

@@ -1,16 +1,18 @@
 { stdenv
+, lib
 , chez
 , clang
 , fetchFromGitHub
 , makeWrapper
+, idris2-version
 }:
 
 # Uses scheme to bootstrap the build of idris2
 stdenv.mkDerivation rec {
   pname = "idris2";
-  version = "0.3.0";
+  version = idris2-version;
 
-  src = ./.;
+  src = ../.;
 
   strictDeps = true;
   nativeBuildInputs = [ makeWrapper clang chez ];
@@ -21,7 +23,7 @@ stdenv.mkDerivation rec {
   '';
 
   makeFlags = [ "PREFIX=$(out)" ]
-    ++ stdenv.lib.optional stdenv.isDarwin "OS=";
+    ++ lib.optional stdenv.isDarwin "OS=";
 
   # The name of the main executable of pkgs.chez is `scheme`
   buildFlags = [ "bootstrap" "SCHEME=scheme" ];
@@ -35,6 +37,8 @@ stdenv.mkDerivation rec {
     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}" ];
+    globalLibrariesPath = builtins.concatStringsSep ":" globalLibraries;
   in ''
     # Remove existing idris2 wrapper that sets incorrect LD_LIBRARY_PATH
     rm $out/bin/idris2
@@ -61,6 +65,7 @@ stdenv.mkDerivation rec {
       --suffix IDRIS2_LIBS ':' "$out/${name}/lib" \
       --suffix IDRIS2_DATA ':' "$out/${name}/support" \
       --suffix IDRIS2_PATH ':' "${additionalIdris2Paths}" \
+      --run "export IDRIS2_PACKAGE_PATH=\$IDRIS2_PACKAGE_PATH:${globalLibrariesPath}" \
       --suffix LD_LIBRARY_PATH ':' "$out/${name}/lib"
   '';
 }

nix/templates/pkg/Foo.idr

@@ -0,0 +1,4 @@
+module Foo
+
+main : IO ()
+main = printLn "Foo"

nix/templates/pkg/default.nix

@@ -0,0 +1,3 @@
+(import (fetchTarball https://github.com/edolstra/flake-compat/archive/master.tar.gz) {
+  src = builtins.fetchGit ./.;
+}).defaultNix

nix/templates/pkg/flake.nix

@@ -0,0 +1,32 @@
+{
+  description = "My Idris 2 package";
+
+  inputs.flake-utils.url = github:numtide/flake-utils;
+  inputs.idris = {
+    url = github:idris-lang/Idris2;
+    inputs.nixpkgs.follows = "nixpkgs";
+    inputs.flake-utils.follows = "flake-utils";
+  };
+
+  outputs = { self, nixpkgs, idris, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
+    let
+      npkgs = import nixpkgs { inherit system; };
+      idrisPkgs = idris.packages.${system};
+      buildIdris = idris.buildIdris.${system};
+      pkgs = buildIdris {
+        projectName = "mypkg";
+        src = ./.;
+        idrisLibraries = [];
+      };
+    in rec {
+      packages = pkgs // idrisPkgs;
+      defaultPackage = pkgs.build;
+      devShell = npkgs.mkShell {
+        buildInputs = [ idrisPkgs.idris2 npkgs.rlwrap ];
+        shellHook = ''
+          alias idris2="rlwrap -s 1000 idris2 --no-banner"
+        '';
+      };
+    }
+  );
+}

nix/templates/pkg/mypkg.ipkg

@@ -0,0 +1,5 @@
+package mypkg
+
+modules = Foo
+main = Foo
+executable = runMyPkg

nix/templates/pkgWithDeps/Bar.idr

@@ -0,0 +1,6 @@
+module Bar
+
+import Foo
+
+main : IO ()
+main = printLn "Bar"

nix/templates/pkgWithDeps/default.nix

@@ -0,0 +1,3 @@
+(import (fetchTarball https://github.com/edolstra/flake-compat/archive/master.tar.gz) {
+  src = builtins.fetchGit ./.;
+}).defaultNix

nix/templates/pkgWithDeps/flake.nix

@@ -0,0 +1,38 @@
+{
+  description = "My Idris 2 package";
+
+  inputs.flake-utils.url = github:numtide/flake-utils;
+  inputs.idris = {
+    url = github:idris-lang/Idris2;
+    inputs.nixpkgs.follows = "nixpkgs";
+    inputs.flake-utils.follows = "flake-utils";
+  };
+  inputs.pkg = {
+    url = github:idris-lang/pkg;
+    inputs.flake-utils.follows = "flake-utils";
+    inputs.idris.follows = "idris";
+  };
+
+  outputs = { self, nixpkgs, idris, flake-utils, pkg }: flake-utils.lib.eachDefaultSystem (system:
+    let
+      npkgs = import nixpkgs { inherit system; };
+      my-pkg = pkg.packages.${system}.installLibrary;
+      idrisPkgs = idris.packages.${system};
+      buildIdris = idris.buildIdris.${system};
+      pkgs = buildIdris {
+        projectName = "pkgWithDeps";
+        src = ./.;
+        idrisLibraries = [ pkg ];
+      };
+    in rec {
+      packages = pkgs // idrisPkgs;
+      defaultPackage = pkgs.build;
+      devShell = npkgs.mkShell {
+        buildInputs = [ idrisPkgs.idris2 npkgs.rlwrap ];
+        shellHook = ''
+          alias idris2="rlwrap -s 1000 idris2 --no-banner"
+        '';
+      };
+    }
+  );
+}

nix/templates/pkgWithDeps/pkgWithDeps.ipkg

@@ -0,0 +1,7 @@
+package mypkg2
+
+depends = mypkg
+
+modules = Bar
+main = Bar
+executable = runMyPkg2

nix/test.nix

@@ -0,0 +1,44 @@
+{ nixpkgs
+, idris
+, flake-utils
+, system
+, stdenv
+, runCommand
+, lib
+}:
+let
+  withTests = tests: drv:
+    let testDrvs = lib.mapAttrs
+      (name: testScript:
+        runCommand "${drv.name}-test-${name}"
+          {} ''
+            ${testScript}
+            touch "$out"
+          '') tests;
+     in testDrvs;
+  createTemplate = flake: inputs: type: let
+    self = import flake;
+    template = self.outputs ({ inherit self nixpkgs idris flake-utils; } // inputs);
+    templateBuild = template.packages.${system}.${type};
+    in templateBuild;
+
+  templateBuildDefault = createTemplate ./templates/pkg/flake.nix {} "build";
+  templateBuildDefaultLibrary = createTemplate ./templates/pkg/flake.nix {} "installLibrary";
+  templateBuildWithDeps = createTemplate ./templates/pkgWithDeps/flake.nix
+    { pkg = templateBuildDefaultLibrary; } "build";
+
+  testsTemplate = {
+    checkFoo = ''
+      ${templateBuildDefault}/bin/runMyPkg \
+        | grep "Foo"
+    '';
+  };
+  testsTemplateWithDeps = {
+    checkBar = ''
+      ${templateBuildWithDeps}/bin/runMyPkg2 \
+        | grep "Bar"
+    '';
+  };
+in
+withTests testsTemplate templateBuildDefault
+// withTests testsTemplateWithDeps templateBuildWithDeps

nix/text-editor.nix

@@ -0,0 +1,28 @@
+{ pkgs
+, idris-emacs-src
+, idris2Pkg
+}: with pkgs;
+let
+  init-file = ./init.el;
+  makeEmacsWrapper = name: my-emacs: init: writeShellScriptBin name ''
+    ${my-emacs}/bin/emacs -q -l ${init-file} $@
+  '';
+in rec {
+  idris2-mode = emacsPackages.melpaBuild {
+    pname = "idris2-mode";
+    src = idris-emacs-src;
+    packageRequires = with pkgs.emacsPackages.melpaPackages; [
+      prop-menu
+    ];
+    version = "1";
+    recipe = pkgs.writeText "recipe" ''
+      (idris2-mode :repo "redfish64/idris2-mode" :fetcher github)
+    '';
+  };
+  idris-emacs = emacsWithPackages [ idris2-mode ];
+  emacs-dev = makeEmacsWrapper "emacs-dev" idris-emacs init-file;
+  emacs-with-idris = writeShellScriptBin "emacs-with-idris" ''
+    export PATH=${idris2Pkg}/bin:$PATH
+    ${emacs-dev}/bin/emacs-dev $@
+  '';
+}