I recently answered my own question for how to set up a Lean project with Mathlib dependencies. I realize I don't know everything about this. The route I follow starts by navigating to the correct folder in a terminal and running
lake +leanprover/lean4:nightly-2023-02-04 new my_project math
I then navigate to
lake exe cache get, and then
All this is according to the documentation. Will this project automatically update with Lean nightly changes? If not, how do I do this safely?