Preserve `.git` folders in derivations

I’m making a wrapper for lake, Lean’s build system. Every package in lake’s dependency system has to have a .git folder during build time, which is enforced by lake.

When I create derivations containing this .git folder, it seems like mkDerivation and symlinkJoin will erase the .git folder, making it impossible for lake to proceed:

    stdenv.mkDerivation {
      inherit src name;
      buildInputs = [git lean];
      buildPhase = ''
        mkdir .lake
        ln -s ${lakePackages} .lake/packages
        if [ -d .lake/packages/batteries ]; then
          # doesn't show `.git`
          ls -alh .lake/packages/batteries/
        fi
        lake build
        git init
        git remote add origin ${url}
      '';
      installPhase = ''
        mkdir -p $out/${name}
        mv * $out/${name}/
        mv .git $out/${name}/
        mv .lake $out/${name}/
        if [ ! -d $out/${name}/.git ]; then
          exit 1
        fi
      '';
    };

Is there a way to prevent nix from deleting the .git directory?

The code is here: feat: Use lake builds by lenianiva · Pull Request #88 · lenianiva/lean4-nix · GitHub

You can but you shouldn’t, as leaveDotGit-esque behavior makes the derivation not-reproducible (and will break FOD hashes).

Also you can only fetch stuff in FODs, so what you’re doing won’t work.

I just need to trick lake into not trying to download more code from the internet. There are no fetching or committing involved. There’s a hard coded check in lake which compares the remote url with a known url. That’s all lake will do to this synthetic .git directory. There is no reproducibility problem here.

Edit: After further digging I decided to modify the lake manifest to not use git.