Incorrect Types in TOML Schema for lakefile.toml #11535
Description
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
When specifying a dependency in lakefile.toml using a subdirectory in a Git repository, the Even Better TOML extension flags this as a type error ({"url":"https://github.com/User/repo","subDir":"subdirectory"} is not of type "string") despite the Lean Language Reference stating that this is a valid configuration.
This is caused by src/lake/schemas/lakefile-toml-schema.json having an incorrect type for dependencyConfig.git.
According to https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#Lake___Dependency-git, the git field in a require block in lakefile.toml may either be a string or a table with the shape
{
url: String,
subDir: String
}Context
This came up when I was trying to add Aeneas as a dependency in a project.
I noticed that the standard installation procedure led to a lakefile.toml that had errors, but still compiled
Steps to Reproduce
- Either install Even Better TOML or install Taplo CLI.
- Create a Lean package that requires a Lean package from a subdirectory on Git. I've created an example repository at https://github.com/maxwell3025/lake-toml-minimal-example.
- Check
lakefile.tomlusing the schema provided by Lean 4.
taplo lint --schema https://raw.githubusercontent.com/leanprover/lean4/refs/heads/master/src/lake/schemas/lakefile-toml-schema.json lakefile.tomlExpected behavior:
No errors should be displayed
Actual behavior:
INFO taplo:lint_files:collect_files: found files total=1 excluded=0 files=["/home/maxwell/Repositories/lake-toml-minimal-example/lakefile.toml"] cwd="/home/maxwell/Repositories/lake-toml-minimal-example"
error: {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
┌─ /home/maxwell/Repositories/lake-toml-minimal-example/lakefile.toml:9:7
│
9 │ git = { url = "https://github.com/AeneasVerif/aeneas", subDir = "backends/lean" }
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
error: {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
┌─ /home/maxwell/Repositories/lake-toml-minimal-example/lakefile.toml:9:9
│
9 │ git = { url = "https://github.com/AeneasVerif/aeneas", subDir = "backends/lean" }
│ ^^^ {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
error: {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
┌─ /home/maxwell/Repositories/lake-toml-minimal-example/lakefile.toml:9:15
│
9 │ git = { url = "https://github.com/AeneasVerif/aeneas", subDir = "backends/lean" }
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
error: {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
┌─ /home/maxwell/Repositories/lake-toml-minimal-example/lakefile.toml:9:56
│
9 │ git = { url = "https://github.com/AeneasVerif/aeneas", subDir = "backends/lean" }
│ ^^^^^^ {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
error: {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
┌─ /home/maxwell/Repositories/lake-toml-minimal-example/lakefile.toml:9:65
│
9 │ git = { url = "https://github.com/AeneasVerif/aeneas", subDir = "backends/lean" }
│ ^^^^^^^^^^^^^^^ {"url":"https://github.com/AeneasVerif/aeneas","subDir":"backends/lean"} is not of type "string"
ERROR taplo:lint_files: invalid file error=schema validation failed path="/home/maxwell/Repositories/lake-toml-minimal-example/lakefile.toml"
ERROR operation failed error=some files were not valid
Versions
Tested with
- Lake version 5.0.0-src (Lean version 4.27.0-nightly-2025-12-06)
- Ubuntu 24.04.3 LTS
- taplo 0.10.0
- tamasfe.even-better-toml 0.21.2 (VS Code Extension)
- VS Code 1.106.2
Additional Information
N/A
Impact
This affects DX.
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.