Add Nix flakes (#800)

* added nix flake files

* added nix installation

* added install

* added default.nix

* added installPhase

* Renamed Build to Nix

* changed cubical derivation

* added FinWeak

* added more indentation

* removed useless {n}

* added more indentation

* added agdaWithCubical in flake.nix

* removed unnecessary FinWeak

* added nix flake in install.md

* changed CI to master

* changed name to nix flakes instructions

* improved nix flakes

* nixpkgs is referred to nixos-22.05

* changed defaultPackage to default

* updated flake.nix

* added install.md instruction

* updated nix flakes

* changed to flake-compat

.github/workflows/ci-nix.yml

@@ -0,0 +1,18 @@
+name: Nix
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    paths:
+      - '**.nix'
+      - 'flake.lock'
+
+jobs:
+  deploy:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - uses: cachix/install-nix-action@v17
+      - name: Build
+        run:  nix build -v --print-build-logs

INSTALL.md

@@ -282,3 +282,42 @@ cubical
 $ cat .agda/libraries
 /path/to/cubical.agda-lib
 ```
+
+Nix flakes instructions
+=======================
+
+Create a nix flake like this one:
+```nix
+{
+  inputs.cubical = {
+    url = "github:agda/cubical";
+    inputs.nixpkgs.follows = "nixpkgs";
+  };
+  outputs = { self, nixpkgs, cubical }:
+  let system = "x86_64-linux";
+      cub-packages = cubical.packages.${system};
+      cubical-lbry = cub-packages.cubical;
+  in
+  with import nixpkgs { system = system; };
+  rec {
+    packages.${system} = {
+      cubical = cubical-lbry;
+      agda = agda.withPackages [cubical-lbry];
+    };
+    defaultPackage.${system} = packages.${system}.agda;
+  };
+}
+```
+cubical-lbry is the cubical library that you have to add in Agda packages.
+
+You can test if Agda with the cubical library is working after adding this file:
+`test.agda`
+```agda
+{-# OPTIONS --cubical #-}
+open import Cubical.Foundations.Prelude
+```
+And running:
+```shell
+nix --extra-experimental-features "nix-command flakes" shell
+agda -l cubical -i . test.agda
+```

RELEASE.md

@@ -14,3 +14,7 @@ Post-release
    include: .
    depend:
   ```
+
+* Increment the `version` field in `flake.nix`.
+
+* Update flake inputs by running `nix flake update`.

default.nix

@@ -0,0 +1,10 @@
+(import
+  (
+    let lock = builtins.fromJSON (builtins.readFile ./flake.lock); in
+    fetchTarball {
+      url = "https://github.com/edolstra/flake-compat/archive/${lock.nodes.flake-compat.locked.rev}.tar.gz";
+      sha256 = lock.nodes.flake-compat.locked.narHash;
+    }
+  )
+  { src = ./.; }
+).defaultNix

flake.nix

@@ -0,0 +1,54 @@
+{
+  description = "Cubical Agda";
+
+  inputs.nixpkgs.url = "nixpkgs/nixpkgs-unstable";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+  inputs.flake-compat = {
+    url = "github:edolstra/flake-compat";
+    flake = false;
+  };
+
+  outputs = { self, flake-compat, flake-utils, nixpkgs }:
+    let
+      inherit (nixpkgs.lib) cleanSourceWith hasSuffix;
+      overlay = final: prev: {
+        cubical = final.agdaPackages.mkDerivation rec {
+          pname = "cubical";
+          version = "0.4";
+
+          src = cleanSourceWith {
+            filter = name: type:
+              !(hasSuffix ".nix" name)
+            ;
+            src = ./.;
+          };
+
+
+          LC_ALL = "C.UTF-8";
+
+          # The cubical library has several `Everything.agda` files, which are
+          # compiled through the make file they provide.
+          nativeBuildInputs = [ final.ghc ];
+          buildPhase = ''
+            make
+          '';
+          meta = {
+            description = "An experimental library for Cubical Agda";
+            homepage = "https://github.com/agda/cubical";
+            license = "MIT License";
+          };
+        };
+        agdaWithCubical = final.agdaPackages.agda.withPackages [final.cubical];
+      };
+      overlays = [ overlay ];
+    in
+    { overlays.default = overlay; } //
+    flake-utils.lib.eachDefaultSystem (system:
+      let pkgs = import nixpkgs { inherit system overlays; };
+      in rec {
+        packages = with pkgs; rec {
+          inherit cubical agdaWithCubical;
+          default = cubical;
+        };
+      });
+}