lake does not validate lakefile.toml

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

lake silently ignores bad option combinations in lakefile.toml, for instance a version field for a require from git.

Context

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/invalid.20atom/near/491387823

Steps to Reproduce

Create a new project with lakefile.toml containing:

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
version = "v4.14.0"

and run lake update.

Expected behavior:

Expected behavior: lake should at least emit a warning saying git and version are incompatible, maybe even suggesting to replace version by rev and explain that rev is intended for reservoir require.

Actual behavior:

lake silently ignores the version field and updates mathlib to git master.

Versions

Lean 4.14.0 on Linux.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Create the reported lakefile.toml and run the lake update entry point to reproduce the silent handling of incompatible require fields. Trace the validation or parsing path for git and version options; done means lake warns about their incompatibility and explains the appropriate alternative.