1  {
  2    description = "Cornell - Verified Binary Format DSL in Lean4";
  3  
  4    inputs = {
  5      nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
  6      flake-utils.url = "github:numtide/flake-utils";
  7    };
  8  
  9    outputs =
 10      {
 11        self,
 12        nixpkgs,
 13        flake-utils,
 14      }:
 15      flake-utils.lib.eachDefaultSystem (
 16        system:
 17        let
 18          pkgs = nixpkgs.legacyPackages.${system};
 19  
 20          # Use elan to manage Lean toolchain (reads lean-toolchain file)
 21          elan = pkgs.elan;
 22  
 23          # C++ build for gRPC client
 24          cornell-cpp = pkgs.stdenv.mkDerivation {
 25            pname = "cornell-cpp";
 26            version = "0.1.0";
 27            src = ./cpp;
 28  
 29            nativeBuildInputs = with pkgs; [
 30              cmake
 31              pkg-config
 32              protobuf
 33              grpc
 34            ];
 35  
 36            buildInputs = with pkgs; [
 37              protobuf
 38              grpc
 39              abseil-cpp
 40              openssl
 41              zlib
 42              c-ares
 43              re2
 44            ];
 45  
 46            cmakeFlags = [
 47              "-DCMAKE_BUILD_TYPE=Release"
 48            ];
 49  
 50            doCheck = true;
 51            checkPhase = ''
 52              ctest --output-on-failure
 53            '';
 54          };
 55  
 56        in
 57        {
 58          packages = {
 59            default = pkgs.stdenv.mkDerivation {
 60              pname = "cornell";
 61              version = "0.1.0";
 62              src = ./.;
 63  
 64              nativeBuildInputs = [ elan ];
 65  
 66              buildPhase = ''
 67                export HOME=$(mktemp -d)
 68                export ELAN_HOME=$HOME/.elan
 69                elan default leanprover/lean4:v4.15.0
 70                lake build
 71              '';
 72  
 73              installPhase = ''
 74                mkdir -p $out
 75                cp -r .lake/build/* $out/
 76              '';
 77            };
 78  
 79            cpp = cornell-cpp;
 80          };
 81  
 82          devShells.default = pkgs.mkShell {
 83            buildInputs = [
 84              elan
 85              pkgs.git # lake needs git
 86  
 87              # C++ development
 88              pkgs.cmake
 89              pkgs.pkg-config
 90              pkgs.protobuf
 91              pkgs.grpc
 92              pkgs.abseil-cpp
 93              pkgs.openssl
 94              pkgs.zlib
 95              pkgs.c-ares
 96              pkgs.re2
 97            ];
 98            shellHook = ''
 99              echo "Cornell development environment"
100              echo "Run 'lake build' to build Lean4"
101              echo "Run 'cd cpp && cmake -B build && cmake --build build' to build C++"
102            '';
103          };
104        }
105      );
106  }