agda-stuff/flake.nix at main · ncfavier/agda-stuff · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
{
  inputs = {
    # nixpkgs.url = "nixpkgs/nixpkgs-unstable";
    nixpkgs.url = "github:ncfavier/nixpkgs/agda-parallel";
    agda.url = "github:agda/agda/2e59d81d60a4518a3176e01b62aba8e082aacdfa";
    agda-stdlib = {
      url = "github:agda/agda-stdlib";
      flake = false;
    };
    the1lab = {
      url = "github:the1lab/1lab";
      flake = false;
    };
  };

  outputs = inputs@{ self, nixpkgs, ... }: let
    system = "x86_64-linux";
    pkgs = import nixpkgs {
      inherit system;
      overlays = [
        inputs.agda.overlays.default
        (final: prev: {
          haskell = prev.haskell // {
            packageOverrides = final.lib.composeExtensions prev.haskell.packageOverrides
              (hfinal: hprev: {
                Agda = final.haskell.lib.enableCabalFlag hprev.Agda "debug";
              });
          };
        })
        (self: super: {
          agdaPackages = super.agdaPackages.overrideScope (aself: asuper: {
            standard-library = asuper.standard-library.overrideAttrs {
              version = "unstable-${inputs.agda-stdlib.shortRev}";
              src = inputs.agda-stdlib;
            };
            _1lab = asuper._1lab.overrideAttrs {
              version = "unstable-${inputs.the1lab.shortRev}";
              src = inputs.the1lab;
            };
          });
        })
      ];
    };

    agdaLibs = libs: [
      libs.standard-library
      libs.cubical
      libs._1lab
    ];
    agda = pkgs.agda.withPackages agdaLibs;
    AGDA_LIBRARIES_FILE = pkgs.agdaPackages.mkLibraryFile agdaLibs;

    texlive = pkgs.texlive.combine {
      inherit (pkgs.texlive)
        collection-basic
        collection-latex
        xcolor
        preview
        pgf tikz-cd pgfplots
        mathpazo
        varwidth xkeyval standalone;
    };

    deps = [
      pkgs.pandoc-katex
      texlive
      pkgs.poppler-utils
    ];

    PANDOC_KATEX_CONFIG_FILE = pkgs.writeText "katex-config.toml" ''
      trust = true
      throw_on_error = true

      [macros]
      "\\bN" = "\\mathbb{N}"
      "\\bZ" = "\\mathbb{Z}"
    '';

    shakefile = pkgs.haskellPackages.callCabal2nix "agda-stuff-shake" ./shake {};
  in {
    devShells.${system} = {
      default = self.packages.${system}.default.overrideAttrs (old: {
        nativeBuildInputs = old.nativeBuildInputs or [] ++ [ agda ];
        Agda = pkgs.haskellPackages.Agda; # prevent garbage collection
      });

      shakefile = pkgs.haskellPackages.shellFor {
        packages = _: [ shakefile ];
        nativeBuildInputs = deps ++ [
          pkgs.haskell-language-server
        ];
        inherit AGDA_LIBRARIES_FILE PANDOC_KATEX_CONFIG_FILE;
      };
    };

    packages.${system} = {
      default = pkgs.stdenv.mkDerivation {
        name = "agda-stuff";
        src = self;
        nativeBuildInputs = deps ++ [ shakefile ];
        inherit AGDA_LIBRARIES_FILE PANDOC_KATEX_CONFIG_FILE;
        LC_ALL = "C.UTF-8";
        buildPhase = ''
          agda-stuff-shake
          mv _build/site "$out"
        '';
      };

      inherit shakefile;
    };
  };
}