Modifying gitignore on update

Stream: lean4

[Adam Topaz]

When updating mathlib with lake update mathlib in a project that depends on it, I noticed that lake will modify the lean toolchain file automatically which is nice. However, when switching to 4.3.0-rc2 from an older version, it seems that all the build artifacts end up in a new folder called .lake, while .lake is not added to the .gitignore file automatically. This could bite new users.

Should the this update process also add a new line to .gitignore with .lake? What do people think about this?

[Scott Morrison]

I'm inclined to say this is a once off (please!?) issue, and the extra complication in the update hook outweighs the total inconvenience.

[Adam Topaz]

Yeah I guess it won’t be an issue for too long. I just think it’s likely to bite some new users

[Adam Topaz]

Anyway, having a non-optimal gitignore on some third party repos isn’t much of a problem anyway. I’ll just make sure to mention this to my students