{
  description = "RustCallLean";

  inputs = {
    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
    flake-parts.url = "github:hercules-ci/flake-parts";
    lean.url = "github:leanprover/lean4?ref=v4.1.0";
    rust-crate2nix = {
      url = "github:kolloch/crate2nix";
      flake = false;
    };
  };

  outputs = inputs @ {
    self,
    nixpkgs,
    flake-parts,
    lean,
    rust-crate2nix,
    ...
  } : flake-parts.lib.mkFlake { inherit inputs; } {
    flake = {
    };
    systems = [
      "x86_64-linux"
      "x86_64-darwin"
    ];
    perSystem = { system, pkgs, ... }: let
      leanPkgs = lean.packages.${system};
      callee = leanPkgs.buildLeanPackage {
        name = "Callee";
        roots = [ "Callee" ];
        src = ./Callee;
      };
      nativeBuildInputs = [
        pkgs.rustPlatform.bindgenHook
        pkgs.llvmPackages.clang
      ];
      buildInputs = [
        leanPkgs.lean-all
        pkgs.libiconv
      ];
      caller = let
        crateTools = pkgs.callPackage "${rust-crate2nix}/tools.nix" { inherit pkgs; };
      in import (crateTools.generatedCargoNix {
        name = "caller";
        src = ./.;
      }) {
        inherit pkgs;
        defaultCrateOverrides = pkgs.defaultCrateOverrides // {
          caller = attrs: {
            inherit nativeBuildInputs;
            inherit buildInputs;
            CALLEE_PATH = callee.sharedLib;
            LEAN_ROOT = leanPkgs.lean-all;
          };
        };
      };
    in rec {
      packages = {
        inherit (leanPkgs) lean iTree stage1 lean-all;
        callee = callee.sharedLib;
        caller = caller.rootCrate.build;
        bindgen = pkgs.rustPlatform.bindgenHook;
      };
      devShells.default = pkgs.mkShell {
        CALLEE_PATH = callee.sharedLib;
        LEAN_ROOT = leanPkgs.lean-all;
        inherit nativeBuildInputs;
        buildInputs = buildInputs ++ [
          pkgs.rustc
          # This is not needed for compilation. It is here for diagnostic purposes
          pkgs.rust-bindgen
        ];
      };
    };
  };
}