nix

flake.lock

@@ -2,11 +2,11 @@
   "nodes": {
     "flake-utils": {
       "locked": {
-        "lastModified": 1623875721,
+        "lastModified": 1631561581,
-        "narHash": "sha256-A8BU7bjS5GirpAUv4QA+QnJ4CceLHkcXdRp4xITDB0s=",
+        "narHash": "sha256-3VQMV5zvxaVLvqqUrNz3iJelLw30mIVSfZmAaauM3dA=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "f7e004a55b120c02ecb6219596820fcd32ca8772",
+        "rev": "7e5bf3925f6fbdfaf50a2a7ca0be2879c4261d19",
         "type": "github"
       },
       "original": {
@@ -16,6 +16,21 @@
       }
     },
     "nixpkgs": {
+      "locked": {
+        "lastModified": 1634090417,
+        "narHash": "sha256-GGRQSC+dBFtynnwHCG65bdzygXK058NJ92boHGXz8Gg=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "c9ddb803ce95c0ec2ab4d57ba29f136b8ce9fe71",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-agda": {
       "locked": {
         "lastModified": 1624913309,
         "narHash": "sha256-HHZTzHgLuoOmTrHckl9eGG8UWTp32pYXmCoOjgQYIB4=",
@@ -44,6 +59,7 @@
       "original": {
         "owner": "plfa",
         "repo": "plfa.github.io",
+        "rev": "8fec0eb208e48401908414347d060767af48309f",
         "type": "github"
       }
     },
@@ -51,6 +67,7 @@
       "inputs": {
         "flake-utils": "flake-utils",
         "nixpkgs": "nixpkgs",
+        "nixpkgs-agda": "nixpkgs-agda",
         "plfa": "plfa"
       }
     }

flake.nix

@@ -1,62 +1,31 @@
 {
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc";
+    nixpkgs.url = "github:nixos/nixpkgs";
     flake-utils.url = "github:numtide/flake-utils";
 
+    nixpkgs-agda.url = "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc";
     plfa = {
       flake = false;
-      url = "github:plfa/plfa.github.io";
+      url = "github:plfa/plfa.github.io?rev=8fec0eb208e48401908414347d060767af48309f";
     };
   };
 
-  outputs = { self, nixpkgs, flake-utils, plfa }:
+  outputs = { self, nixpkgs, nixpkgs-agda, flake-utils, plfa }:
     flake-utils.lib.eachDefaultSystem (system:
     let
       pkgs = nixpkgs.legacyPackages.${system};
 
-      agda = pkgs.agda.withPackages (p: [
+      myPkgs = rec {
-        p.standard-library
+        agda = import ./nix/agda.nix {
-        (p.mkDerivation {
+          inherit system plfa;
-          pname = "plfa";
+          nixpkgs = nixpkgs-agda;
-          meta = null;
-          version = "1.0.0";
-          buildInputs = [ p.standard-library ];
-          preBuild = ''
-            echo "module Everything where" > Everything.agda
-			find src -name '*.lagda.md' | sed -e 's/src\///' -e 's/\.lagda\.md//' -e 's/\//\./g' -e 's/^/import /' | grep -Ev '^import plfa\.part1\.Equality|Naturals$' >> Everything.agda
-            export LANG=C.UTF-8
-          '';
-          src = plfa;
-        })
-      ]);
-
-      nvim-agda = pkgs.callPackage ./nix/nvim-agda {};
-
-      fix-whitespace = "";
-      # fix-whitespace = pkgs.stdenvNoCC.mkDerivation {
-      #   name = "fix-whitespace";
-      #   src = pkgs.fetchFromGitHub {
-      #     owner = "agda";
-      #     repo = "fix-whitespace";
-      #     rev = "a02f03a097943188a7b9aeaee8369edfc455c4fd";
-      #     sha256 = "TGj3DqOJTHRb9TwwGiDRlaXLseuv8mizYP20IR4YVFs=";
-      #   };
-      # };
-
-      neovim = pkgs.neovim.override {
-        configure = {
-          plug = {
-            plugins = with pkgs.vimPlugins; [
-              nvim-agda
-              nerdtree
-              vim-polyglot
-            ];
-          };
-
-          customRC = ''
-            set cursorline
-          '';
         };
+        nvim-agda = import ./nix/nvim-agda {
+          inherit system;
+          nixpkgs = nixpkgs-agda;
+        };
+
+        neovim = pkgs.callPackage ./nix/neovim.nix { inherit nvim-agda; };
       };
 
       vscode-agda-mode = pkgs.vscode-utils.extensionFromVscodeMarketplace {
@@ -83,11 +52,12 @@
       '';
     in
     {
+      packages = flake-utils.lib.flattenTree myPkgs;
+
       devShell = pkgs.mkShell {
-        buildInputs = with pkgs; [
+        buildInputs = with pkgs; with myPkgs; [
           agda
           vscodium
-          fix-whitespace
           neovim
           nvim-agda
           lua51Packages.luautf8

nix/agda.nix

@@ -0,0 +1,20 @@
+{ nixpkgs, system, plfa, ... }:
+
+let
+  pkgs = nixpkgs.legacyPackages.${system};
+in
+pkgs.agda.withPackages (p: [
+  p.standard-library
+  (p.mkDerivation {
+    pname = "plfa";
+    meta = null;
+    version = "1.0.0";
+    buildInputs = [ p.standard-library ];
+    preBuild = ''
+      echo "module Everything where" > Everything.agda
+      find src -name '*.lagda.md' | sed -e 's/src\///' -e 's/\.lagda\.md//' -e 's/\//\./g' -e 's/^/import /' | grep -Ev '^import plfa\.part1\.Equality|Naturals$' >> Everything.agda
+      export LANG=C.UTF-8
+    '';
+    src = plfa;
+  })
+])

nix/neovim.nix

@@ -0,0 +1,39 @@
+{ neovim, vimPlugins, luajitPackages, nvim-agda }:
+
+neovim.override {
+  configure = {
+    plug = {
+      plugins = with vimPlugins; [
+        ctrlp-vim
+        nerdtree
+        nvim-agda
+        vim-code-dark
+        vim-polyglot
+      ];
+    };
+
+    customRC = ''
+      lua << EOF
+        package.cpath = package.cpath .. ";${luajitPackages.luautf8}/lib/lua/5.1/lua-utf8.so"
+      EOF
+
+      set hidden
+      set cursorline
+      set number
+      set splitright
+      set modeline
+      set expandtab
+      set colorcolumn=80
+      syntax on
+      filetype on
+      filetype plugin indent on
+      colorscheme codedark
+
+      let mapleader = ";"
+      let maplocalleader = ";"
+
+      nnoremap <C-n> :NERDTreeToggle<CR>
+      imap kj <Esc>
+    '';
+  };
+}

nix/nvim-agda/default.nix

@@ -1,5 +1,8 @@
-{ pkgs, ... }:
+{ nixpkgs, system, ... }:
 
+let
+  pkgs = nixpkgs.legacyPackages.${system};
+in
 pkgs.vimUtils.buildVimPlugin rec {
   pname = "nvim-agda";
   version = "2bed0b9a1d42f20438d22a3229c59faaf2b6a8df";

src/Homework2.agda

@@ -74,4 +74,4 @@ to∘from (n II) =
     inc ((to (from n)) I)
   ≡⟨ cong inc (cong _I (to∘from n)) ⟩
     n II
-  ∎
+  ∎