test: add tests for lakefile-toml-schema.json

[maxwell3025]

This pull request adds tests to make sure that lakefile-toml-schema has no false positives and minimal false negatives (or the other way around? Maintainer please confirm/deny).

As discussed in this pull request, tests for the lakefile.toml schema are placed here since the tests in this repo are better maintained and this location avoids adding another dependency to the test suite for the main project.

[maxwell3025]

If I'm parsing the logs correctly, CI is failing because the test runner is slow and timing out on a separate test (Missing "The Lean Server has stopped processing this file" in infoview after 60 seconds). The PR runs are working on my fork, so I think this PR is fine as far as CI is concerned.

[mhuisi]

I wonder if there is something a little more robust we could do here, like listening for diagnostic changes before opening the document and then using the first set of diagnostics that is reported by even-better-toml (or timing out after 60s), which would rely on the assumption that even-better-toml only reports diagnostics once, but the limitations of the VS Code API ensure that we won't really have a perfectly robust solution here either way.

If the 5s delay works consistently, then I'm fine with it :-)

[mhuisi]

Thanks! Happy to merge if you have no further comments.

This pull request adds tests to make sure that lakefile-toml-schema has no false positives and minimal false negatives (or the other way around? Maintainer please confirm/deny).

The schema has the following goals:

• Provide helpful auto-completion
• Do not reject valid lakefile.tomls (I think this is what you refer to as "no false positives")
• As long as it does not clash with providing helpful auto-completion, reject invalid lakefile.tomls within the scope of the capabilities of even-better-toml (but if it clashes, prefer helpful auto-completion over trying to accurately reject all invalid lakefile.tomls)

tests for the lakefile.toml schema are placed here since the tests in this repo are better maintained and this location avoids adding another dependency to the test suite for the main project.

It's more of the latter and less of the former :-) The tests in this repo are not maintained very well, but test breakages here won't be annoying to everyone else working on core.

If I'm parsing the logs correctly, CI is failing because the test runner is slow and timing out on a separate test (Missing "The Lean Server has stopped processing this file" in infoview after 60 seconds). The PR runs are working on my fork, so I think this PR is fine as far as CI is concerned.

Yes, the PR is fine. The tests are known to be a little flaky, but I haven't had much time to investigate why.

[maxwell3025]

Yeah no further comments :)