lake does not validate lakefile.toml

[PatrickMassot]

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.

[tydeu]

While Lake is missing TOML validation, the example in question is not simply a TOML validation issue. It is equivalent to the following configuration in Lean (which is valid):

require "mathlib" @ "v4.14.0"
  from git "https://github.com/leanprover-community/mathlib4.git"

I see two ways to offer a user some correction (perhaps both are desirable):

• Since Lake does not yet support non-git versions, always warn if the version in a non-git version.
• Since we now have Reservoir requires for determining default sources, always require a git source to specify a revision (instead of just defaulting to master as we currently do).