veir/flake.nix at main · opencompl/veir · 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
{
  description = "Verified Intermediate Representation";

  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05";

  outputs = { self, nixpkgs, ... }:
    let
      systems = [
        "aarch64-darwin"
        "aarch64-linux"
        "x86_64-darwin"
        "x86_64-linux"
      ];
      forAllSystems = nixpkgs.lib.genAttrs systems;
      llvmPackages = pkgs: pkgs.llvmPackages_23;

      developmentPackages = pkgs: with pkgs; [
        bash
        (llvmPackages pkgs).clang
        elan
        gmp
        gnumake
        (llvmPackages pkgs).llvm
        ((llvmPackages pkgs).mlir.overrideAttrs (oldAttrs: {
          # Nixpkgs does not enable MLIR's test dialect. VeIR's PDL tests
          # use that dialect when checking compatibility with mlir-opt.
          cmakeFlags = oldAttrs.cmakeFlags ++ [
            (lib.cmakeBool "MLIR_INCLUDE_TESTS" true)
          ];
        }))
        pkg-config
        uv
      ];

      makeApp = pkgs: target:
        let
          suffix = if target == null then "help" else target;
          command = if target == null then "make" else "make ${target}";
          package = pkgs.writeShellApplication {
            name = "veir-${suffix}";
            runtimeInputs = developmentPackages pkgs;
            text = ''
              export LEAN_AR="${(llvmPackages pkgs).llvm}/bin/llvm-ar"
              export LEAN_CC="${self}/ExArray/compiler"
              exec ${command} "$@"
            '';
          };
        in
        {
          type = "app";
          program = "${package}/bin/veir-${suffix}";
          meta.description =
            if target == null
            then "Show VeIR's Make targets"
            else "Run VeIR's make ${target} target";
        };

      makeLeanApp = pkgs: target:
        let
          package = pkgs.writeShellApplication {
            name = target;
            runtimeInputs = developmentPackages pkgs;
            text = ''
              export LEAN_AR="${(llvmPackages pkgs).llvm}/bin/llvm-ar"
              export LEAN_CC="${self}/ExArray/compiler"
              exec lake exe ${target} "$@"
            '';
          };
        in
        {
          type = "app";
          program = "${package}/bin/${target}";
          meta.description = "Run VeIR's ${target} executable";
        };
    in
    {
      devShells = forAllSystems (system:
        let
          pkgs = nixpkgs.legacyPackages.${system};
        in
        {
          default = pkgs.mkShell {
            packages = developmentPackages pkgs;

            # ExArray uses Clang LTO and therefore needs its compiler wrapper
            # together with LLVM's archiver.
            LEAN_AR = "${(llvmPackages pkgs).llvm}/bin/llvm-ar";
            LEAN_CC = "${self}/ExArray/compiler";
          };
        });

      apps = forAllSystems (system:
        let
          pkgs = nixpkgs.legacyPackages.${system};
        in
        {
          default = makeApp pkgs null;
          build = makeApp pkgs "build";
          tests = makeApp pkgs "tests";
          "veir-opt" = makeLeanApp pkgs "veir-opt";
          "veir-interpret" = makeLeanApp pkgs "veir-interpret";
          "veir2mir" = makeLeanApp pkgs "veir2mir";
          "run-benchmarks" = makeLeanApp pkgs "run-benchmarks";
        });
    };
}