lake.nix

{pkgs}: let
  capitalize = s: let
    first = pkgs.lib.toUpper (builtins.substring 0 1 s);
    rest = builtins.substring 1 (-1) s;
  in
    first + rest;
  importLakeManifest = manifestFile: let
    manifest = pkgs.lib.importJSON manifestFile;
  in
    pkgs.lib.warnIf (manifest.version != "1.1.0") ("Unknown version: " + manifest.version) manifest;
  depToPackage = dep: let
    src = pkgs.lib.cleanSource (builtins.fetchGit {
      inherit (dep) url rev;
      shallow = true;
    });
  in {
    inherit src;
    manifestFile = "${src}/${dep.manifestFile}";
  };
  # Builds a Lean package by reading the manifest file.
  mkPackage = {
    # Path to the source
    src,
    # Path to the `lake-manifest.json` file
    manifestFile ? "${src}/lake-manifest.json",
    # Root module
    roots ? null,
    # Default dependencies
    deps ? with pkgs.lean; [Init Std Lean],
  }: let
    manifest = importLakeManifest manifestFile;
    # Build all dependencies using `buildLeanPackage`
    manifestDeps = builtins.map (dep: mkPackage (depToPackage dep)) manifest.packages;
  in
    pkgs.lean.buildLeanPackage {
      inherit (manifest) name;
      inherit src;
      roots =
        if builtins.isNull roots
        then [(capitalize manifest.name)]
        else roots;
      deps = deps ++ manifestDeps;
    };
in {
  inherit mkPackage;
}