feat: lake: conditional cache overwrites

[tydeu]

This PR refines when and how Lake decides to overwrite data while caching, and has Lake prefer outputs in a local trace file over those stored in the cache.

Key details

• Introduces an overwrite toggle controlled by the new options --no-overwrite and --force-overwrite. The default for lake cache add is --force-overwrite and the default for lake cache stage/unstage is --no-overwrite.
• With --force-overwrite, already existing mappings and artifacts are overwritten. With --no-overwrite, they are not.
• Existing trace's outputs will not overwrite an existing cached input-to-output mapping (so they may diverge). This avoids writing to the cache on every trace read.
• The ltar output is retained in the module's cached input-to-output mapping after unpacking from the cache.

Closes #13997.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-06-12 21:08:16)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-14036 build this PR didn't complete normally. (2026-06-12 22:01:09) View Log
• ✅ Mathlib branch lean-pr-testing-14036 has successfully built against this PR. (2026-06-12 22:49:01) View Log
• ✅ Mathlib branch lean-pr-testing-14036 has successfully built against this PR. (2026-06-13 02:35:50) View Log
• ✅ Mathlib branch lean-pr-testing-14036 has successfully built against this PR. (2026-06-13 04:04:57) View Log
• ✅ Mathlib branch lean-pr-testing-14036 has successfully built against this PR. (2026-06-13 05:23:35) View Log
• ✅ Mathlib branch lean-pr-testing-14036 has successfully built against this PR. (2026-06-13 21:12:13) View Log