For this project, it seems that continuous integration is overkill. I am inclined to removing it. I feel like crying every time I checkpoint a part of my development and this runs CI, when I know perfectly well now is not the time to check for a complete re-compilation of the whole project.
At the very least, we should not run CI on theories when the only changes happened in the documents/ directory. I have a vague memory that we already discussed this, probably on zulip, but I am unable to find a trace of this conversation.
For this project, it seems that continuous integration is overkill. I am inclined to removing it. I feel like crying every time I checkpoint a part of my development and this runs CI, when I know perfectly well now is not the time to check for a complete re-compilation of the whole project.
At the very least, we should not run CI on theories when the only changes happened in the documents/ directory. I have a vague memory that we already discussed this, probably on zulip, but I am unable to find a trace of this conversation.