{
  inputs = {
    nixpkgs.url = "nixpkgs/nixos-23.11";
    flake-utils.url = "github:numtide/flake-utils";

    crane = {
      url = "github:ipetkov/crane";
      inputs.nixpkgs.follows = "nixpkgs";
    };

    fenix = {
      url = "github:nix-community/fenix";
      inputs.nixpkgs.follows = "nixpkgs";
    };
  };

  outputs = {
    self,
    crane,
    fenix,
    flake-utils,
    nixpkgs,
  }:
    flake-utils.lib.eachDefaultSystem (system: let
      ocamlFlambda = _: prev: rec {
        ocamlPackages_4_14 = prev.ocamlPackages.overrideScope' (_: prev: {
          ocaml = prev.ocaml.override {flambdaSupport = true;};
        });
        coqPackages_8_17 = prev.coqPackages_8_17.overrideScope' (_: prev: {
          coq = prev.coq.override {
            ocamlPackages_4_14 = ocamlPackages_4_14;
          };
        });
      };
      overlays = [fenix.overlays.default ocamlFlambda];
      pkgs = import nixpkgs {inherit overlays system;};

      name = "refinedrust";
      version = "0.1.0";

      coq = {
        pkgs = pkgs.coqPackages_8_17;
        toolchain = [coq.pkgs.coq] ++ coq.pkgs.coq.nativeBuildInputs;
        version = coq.pkgs.coq.coq-version;

        stdpp = {
          version = "4be5fd62ddbd5359f912e2cebb415b015c37e565";
          sha256 = "sha256-9pNWjPy1l1EovcKZchC/23FwlllD/Oa3jEOtN5tDzik=";
        };

        iris = {
          version = "1de1b3112754e14a4968534572e118a23344eafe";
          sha256 = "sha256-Cimb3XxnchPSWVGMSyWmJdLQqHMilw11o2hq/4h8dVQ=";
        };

        lambda-rust = {
          version = "4ec2733cce240e3595c37cb926eb000455be77a4";
          sha256 = "sha256-kX9NIPPOoajuJDVly9qGUCCd3lt8Da2k0dZnDY2zKbY=";
        };
      };

      meta = with pkgs.lib; {
        homepage = "https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev";
        license = licenses.bsd3;
      };

      rust = {
        toolchain = pkgs.fenix.fromToolchainFile {
          file = ./rust-toolchain.toml;
          sha256 = "sha256-0NR5RJ4nNCMl9ZQDA6eGAyrDWS8fB28xIIS1QGLlOxw=";
        };

        env = let
          cargo-bindeps = pkgs.symlinkJoin {
            name = "cargo-bindeps";
            paths = [pkgs.cargo];
            nativeBuildInputs = [pkgs.makeWrapper];
            postBuild = ''
              wrapProgram $out/bin/cargo \
                --add-flags "-Zbindeps"
            '';
          };

          craneLib = (crane.mkLib pkgs).overrideScope (_: prev: {
            downloadCargoPackageFromGit = prev.downloadCargoPackageFromGit.override (args: {
              pkgsBuildBuild = args.pkgsBuildBuild // {cargo = cargo-bindeps;};
            });
          });
        in
          craneLib.overrideToolchain rust.toolchain;

        lib = "${rust.toolchain}/lib/rustlib/$(rustc -Vv | grep '^host:' | cut -d' ' -f2)/lib";
        src = "${rust.toolchain}/lib/rustlib/rustc-src/rust/compiler";
      };
    in rec {
      packages = let
        fetchCoqDeps = with pkgs.lib;
          drv: [drv] ++ flatten (map fetchCoqDeps drv.propagatedBuildInputs);

        mkDepCoqDerivation = pin: {
          pname,
          propagatedBuildInputs ? [],
          owner ? "iris",
        }:
          coq.pkgs.mkCoqDerivation {
            inherit pname propagatedBuildInputs owner;

            domain = "gitlab.mpi-sws.org";
            preBuild = "patchShebangs coq-lint.sh";

            release.${pin.version}.sha256 = "${pin.sha256}";
            version = pin.version;
          };
      in {
        theories = let
          stdpp = mkDepCoqDerivation coq.stdpp {
            pname = "stdpp";
          };

          iris = mkDepCoqDerivation coq.iris {
            pname = "iris";

            propagatedBuildInputs = [stdpp];
          };

          lambda-rust = mkDepCoqDerivation coq.lambda-rust {
            pname = "lambda-rust";
            owner = "lgaeher";

            propagatedBuildInputs = [iris];
          };
        in
          coq.pkgs.mkCoqDerivation {
            inherit meta version;

            pname = name;
            opam-name = name;

            src = ./theories;

            propagatedBuildInputs = with coq.pkgs; [coq-record-update equations lambda-rust];

            preBuild = "dune() { command dune $@ --display=short; }";
            useDune = true;
          };

        frontend = let
          src = ./rr_frontend;
          pname = "cargo-${name}";

          cargoArtifacts = rust.env.buildDepsOnly {
            inherit meta pname src version;
          };
        in
          rust.env.buildPackage rec {
            inherit cargoArtifacts meta pname src version;

            buildInputs = [rust.toolchain pkgs.gnupatch];
            nativeBuildInputs = with pkgs;
              [makeWrapper]
              ++ lib.optionals stdenv.isDarwin [libzip libiconv];

            postInstall = with pkgs.lib.strings; ''
              wrapProgram $out/bin/refinedrust-rustc \
                --set LD_LIBRARY_PATH "${rust.lib}" \
                --set DYLD_FALLBACK_LIBRARY_PATH "${rust.lib}"

              wrapProgram $out/bin/${pname} \
                --set PATH "${makeSearchPath "bin" buildInputs}"
            '';

            doCheck = false;
          };

        stdlib = coq.pkgs.mkCoqDerivation {
          inherit meta version;

          pname = "refinedrust-stdlib";
          opam-name = "refinedrust-stdlib";
          src = ./stdlib;

          buildInputs = [packages.frontend rust.toolchain];
          propagatedBuildInputs = [packages.theories];

          preBuild = ''
            dune() { command dune $@ --display=short; }
            make generate_stdlib
          '';
          useDune = true;
        };

        default = pkgs.buildEnv {
          inherit meta;

          name = "cargo-${name}";
          paths = coq.toolchain ++ [packages.frontend rust.toolchain];

          pathsToLink = ["/bin"];
          nativeBuildInputs = [pkgs.makeWrapper];
          postBuild = with pkgs.lib.strings; ''
            wrapProgram $out/bin/dune \
              --set COQPATH "${makeSearchPath "lib/coq/${coq.version}/user-contrib" (fetchCoqDeps packages.stdlib)}"
          '';
        };
      };

      devShells.default = pkgs.mkShell {
        inputsFrom = with packages; [frontend theories];

        packages = with pkgs; [gnumake gnupatch gnused];

        shellHook = ''
          export LD_LIBRARY_PATH=''${LD_LIBRARY_PATH}:${rust.lib}
          export DYLD_FALLBACK_LIBRARY_PATH=''${DYLD_FALLBACK_LIBRARY_PATH}:${rust.lib}
          export RUST_SRC_PATH=${rust.src}/rustc_driver/Cargo.toml
        '';
      };

      formatter = pkgs.alejandra;
    });
}