core/flake.nix at master · cubical-mini/core · 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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
{
  description = "A non-standard library for Cubical Agda";

  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs";
    flake-parts.url = "github:hercules-ci/flake-parts";
    agda = {
      url = "github:cubical-mini/agda?ref=agda-forester";
      inputs.nixpkgs.follows = "nixpkgs";
      inputs.flake-parts.follows = "flake-parts";
    };
    forest-theme = {
      url = "github:cubical-mini/forest-theme?ref=agda-forester";
      flake = false;
    };
    forester.url = "sourcehut:~jonsterling/ocaml-forester";
    treelist.url = "github:samtoth/treelist";
  };

  outputs = inputs@{ flake-parts , forest-theme , forester , treelist , ... }:
    flake-parts.lib.mkFlake { inherit inputs; } {
      perSystem = { pkgs , system, ... }: let

        name = "cm-core";

        minimalFS = [
          ./cm-core.agda-lib
          ./src
        ];

        mkCore = extraFS: pkgs.agdaPackages.mkDerivation {
          pname = name;
          version = "0.1.0";
          src = pkgs.lib.fileset.toSource {
            root = ./. ;
            fileset = pkgs.lib.fileset.unions (minimalFS ++ extraFS);
          };
          meta.description = "cubical-mini core library";
        };

        minimal = mkCore [];
        extra = mkCore [ ./extra ]; # interactive doc included

        scripts = pkgs.stdenv.mkDerivation {
          name = "${name} scripts";
          src = ./bin ;
          installPhase = ''
            mkdir -p $out/bin
            cp * $out/bin
            chmod +x $out/bin
          '';
        };

        html = pkgs.stdenv.mkDerivation {
          name = "${name} html";
          src = ./.;
          buildInputs = [
            extra
            forester.packages.${system}.default
            pkgs.agda
            scripts
            treelist.packages.${system}.default
          ];
          installPhase = ''
            cp -R "${forest-theme}" theme/
            prepare-output.sh
            agda-gen-everything.sh
            agda-render.sh
            forest-rebuild.sh
            mkdir -p $out/
            cp -R output/core/* $out/
          '';
        };

        tex = (pkgs.texlive.combine {
          inherit (pkgs.texlive)
            scheme-small
            latexindent
            dvisvgm
            pgf
            tikz-cd
            spath3
            mathtools
            amsfonts
            stmaryrd
            standalone
          ;
        });

      in {
        _module.args.pkgs = import inputs.nixpkgs {
          inherit system;
          overlays = [ inputs.agda.overlays.default ];
        };

        packages = {
          default = minimal;
          inherit extra html;
        };

        devShells.default = pkgs.mkShell {
          packages = [
            forester.packages.${system}.default
            pkgs.agda
            pkgs.bashInteractive
            pkgs.emacs
            pkgs.fswatch
            pkgs.haskellPackages.fix-whitespace
            pkgs.haskellPackages.wai-app-static
            pkgs.ibm-plex
            pkgs.tmux
            scripts
            tex
            treelist.packages.${system}.default
          ];
          shellHook = ''
            export PR=$PWD

            $PR/.devenv/startup.sh
          '';
        };

        # checks.default = core-test;
      };

      systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ];
    };
}