-
Notifications
You must be signed in to change notification settings - Fork 710
fix: add table variant for require.git field in lakefile.toml schema
#11536
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Conversation
require.git Field in lakefile.toml Schemarequire.git field in lakefile.toml schema
|
Mathlib CI status (docs):
|
|
Reference manual CI status:
|
|
I don't have the permissions necessary to add labels, but this should have the label |
| @@ -0,0 +1,16 @@ | |||
| #!/usr/bin/env bash | |||
| TAPLO_URL=https://github.com/tamasfe/taplo/releases/latest/download/taplo-linux-x86_64.gz | |||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure if we really want the core test suite to depend on Taplo, which is apparently currently not being actively maintained anymore.
I'd be happy to have these tests in leanprover/vscode-lean4, though, which is after all also the actual component that depends on Taplo :-)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, they also mentioned this on Zulip. Should lakefile-toml-schema.json be moved to vscode-lean4 instead? It seems like it would be awkward to have the tests and the component being tested in different repos.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should
lakefile-toml-schema.jsonbe moved to vscode-lean4 instead?
I'd still keep it here.
It seems like it would be awkward to have the tests and the component being tested in different repos.
I maintain both, so I suspect that this will not be much of a problem in practice. We can revisit this later if it does turn out to be a problem.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've made a draft pull request at vscode-lean4.
This PR corrects the JSON Schema at
src/lake/schemas/lakefile-toml-schema.jsonto allow the table variant of therequire.gitfield inlakefile.tomlas specified in the reference.Closes #11535