{ 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;
  })
])