RFC: Exclude .lake directory from backups with CACHEDIR.TAG

[henkkuli]

Proposal

The .lake/ directory contains remote sources and build artifacts for a project. Hence its contents can be automatically recreated from the rest of the project source. Such directories should be marked with a CACHEDIR.TAG file. This allows automatic backup tools (e.g. Restic, Borg and GNU tar) to ignore the contents of the directory when instructed (e.g. --exclude-caches flag on tar).

The only effect on users should be that their automatic backups may get smaller as the contents of .lake/ directory get excluded. In the rare case that files should be recovered from backups, the user needs to recompile their Lean projects. I would argue that this is a relatively minor inconvenience, and if this is a problem, the user should not have excluded caches from backups in the first place.

Other programming languages are already doing this. For example, Rust is excluding both target/ and ~/.cargo/{git,registry}/ directories.

Community Feedback

The feature was first proposed in the Lean Zulip. It got green light from @semorrison and @tydeu.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.