diff --git a/.github/workflows/ci-nix.yml b/.github/workflows/ci-nix.yml index e81143863..75153b70d 100644 --- a/.github/workflows/ci-nix.yml +++ b/.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 diff --git a/.gitignore b/.gitignore index b8f0e4c99..b1f356050 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ idris2docs_venv +result *~ *.ibc *.ttc diff --git a/INSTALL.md b/INSTALL.md index 233529a80..9ef49bf13 100644 --- a/INSTALL.md +++ b/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 diff --git a/default.nix b/default.nix index 40d105cf6..b22e926ea 100644 --- a/default.nix +++ b/default.nix @@ -1,3 +1,3 @@ -{ nixpkgs ? import {} }: with nixpkgs; - -callPackage ./package.nix {} +(import (fetchTarball https://github.com/edolstra/flake-compat/archive/master.tar.gz) { + src = builtins.fetchGit ./.; +}).defaultNix diff --git a/flake.lock b/flake.lock index c7678cc6e..84f4e4e6e 100644 --- a/flake.lock +++ b/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" } } diff --git a/flake.nix b/flake.nix index d37043a8e..e8181e04f 100644 --- a/flake.nix +++ b/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; + }; } diff --git a/nix/buildIdris.nix b/nix/buildIdris.nix new file mode 100644 index 000000000..e5e8dd593 --- /dev/null +++ b/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} + ''; + }); +} diff --git a/nix/init.el b/nix/init.el new file mode 100644 index 000000000..728000bc8 --- /dev/null +++ b/nix/init.el @@ -0,0 +1 @@ +(require 'idris2-mode) diff --git a/package.nix b/nix/package.nix similarity index 86% rename from package.nix rename to nix/package.nix index b642898c8..e3223ba20 100644 --- a/package.nix +++ b/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" ''; } diff --git a/nix/templates/pkg/Foo.idr b/nix/templates/pkg/Foo.idr new file mode 100644 index 000000000..acd9ae164 --- /dev/null +++ b/nix/templates/pkg/Foo.idr @@ -0,0 +1,4 @@ +module Foo + +main : IO () +main = printLn "Foo" diff --git a/nix/templates/pkg/default.nix b/nix/templates/pkg/default.nix new file mode 100644 index 000000000..b22e926ea --- /dev/null +++ b/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 diff --git a/nix/templates/pkg/flake.nix b/nix/templates/pkg/flake.nix new file mode 100644 index 000000000..2d91e0d52 --- /dev/null +++ b/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" + ''; + }; + } + ); +} diff --git a/nix/templates/pkg/mypkg.ipkg b/nix/templates/pkg/mypkg.ipkg new file mode 100644 index 000000000..f1489f310 --- /dev/null +++ b/nix/templates/pkg/mypkg.ipkg @@ -0,0 +1,5 @@ +package mypkg + +modules = Foo +main = Foo +executable = runMyPkg diff --git a/nix/templates/pkgWithDeps/Bar.idr b/nix/templates/pkgWithDeps/Bar.idr new file mode 100644 index 000000000..9ee179a43 --- /dev/null +++ b/nix/templates/pkgWithDeps/Bar.idr @@ -0,0 +1,6 @@ +module Bar + +import Foo + +main : IO () +main = printLn "Bar" diff --git a/nix/templates/pkgWithDeps/default.nix b/nix/templates/pkgWithDeps/default.nix new file mode 100644 index 000000000..b22e926ea --- /dev/null +++ b/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 diff --git a/nix/templates/pkgWithDeps/flake.nix b/nix/templates/pkgWithDeps/flake.nix new file mode 100644 index 000000000..4c7ae8d80 --- /dev/null +++ b/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" + ''; + }; + } + ); +} diff --git a/nix/templates/pkgWithDeps/pkgWithDeps.ipkg b/nix/templates/pkgWithDeps/pkgWithDeps.ipkg new file mode 100644 index 000000000..29dafee58 --- /dev/null +++ b/nix/templates/pkgWithDeps/pkgWithDeps.ipkg @@ -0,0 +1,7 @@ +package mypkg2 + +depends = mypkg + +modules = Bar +main = Bar +executable = runMyPkg2 diff --git a/nix/test.nix b/nix/test.nix new file mode 100644 index 000000000..305d434e6 --- /dev/null +++ b/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 diff --git a/nix/text-editor.nix b/nix/text-editor.nix new file mode 100644 index 000000000..1f699fc24 --- /dev/null +++ b/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 $@ + ''; +}