For the Coq tasks, I plan on only having a private check file (because the check file is not easily consumable by users, and I decided that I don't want to try to generate Coq check files from it).
At the moment, the frontend does not seem to allow the public check file to be empty -- it would be nice if it could. And if the check file is empty, then it shouldn't be included in the downloadable archive for the task.
Armael
commented
5 years ago
For the Coq tasks, I plan on only having a private check file (because the check file is not easily consumable by users, and I decided that I don't want to try to generate Coq check files from it).
At the moment, the frontend does not seem to allow the public check file to be empty -- it would be nice if it could. And if the check file is empty, then it shouldn't be included in the downloadable archive for the task.