When task resources for multiple proof assistants shall be added, the script is rather inconvenient
because one would end up with three task.yaml files that contain a lot of duplicated information.
One solution would be to allow resource.yaml files where the missing information is automatically discovered from a task.yaml file before pushing.
When task resources for multiple proof assistants shall be added, the script is rather inconvenient because one would end up with three
task.yaml
files that contain a lot of duplicated information.One solution would be to allow
resource.yaml
files where the missing information is automatically discovered from atask.yaml
file before pushing.