Package plfa with Nix

flake.lock

@@ -0,0 +1,60 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1623875721,
+        "narHash": "sha256-A8BU7bjS5GirpAUv4QA+QnJ4CceLHkcXdRp4xITDB0s=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "f7e004a55b120c02ecb6219596820fcd32ca8772",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1624913309,
+        "narHash": "sha256-HHZTzHgLuoOmTrHckl9eGG8UWTp32pYXmCoOjgQYIB4=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "860b56be91fb874d48e23a950815969a7b832fbc",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "860b56be91fb874d48e23a950815969a7b832fbc",
+        "type": "github"
+      }
+    },
+    "plfa": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1628614312,
+        "narHash": "sha256-e5wLKKjabrZesjAd5p5sXeYW28LXoZPGY2jp6cnB9qM=",
+        "owner": "plfa",
+        "repo": "plfa.github.io",
+        "rev": "8fec0eb208e48401908414347d060767af48309f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "plfa",
+        "repo": "plfa.github.io",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs",
+        "plfa": "plfa"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -1,18 +1,37 @@
 {
+  inputs.nixpkgs.url = "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc";
   inputs.flake-utils.url = "github:numtide/flake-utils";
+  inputs.plfa.url = "github:plfa/plfa.github.io";
+  inputs.plfa.flake = false;
 
-  outputs = { self, nixpkgs, flake-utils }:
+  outputs = { self, nixpkgs, flake-utils, plfa }:
     flake-utils.lib.eachDefaultSystem
     (system:
-    let pkgs = nixpkgs.legacyPackages.${system}; in {
+    let
+      pkgs = nixpkgs.legacyPackages.${system};
+      agda = 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;
+        })
+      ]);
+    in {
       devShell =
         pkgs.mkShell {
-          buildInputs = 
+          buildInputs = [
-          with pkgs; [
+            pkgs.emacs
-            emacs
             agda
           ];
         };
       });
-}
+    }