Skip to content

CI/Lint: refactor

Arvid Jakobsson requested to merge arvid@ci-lint-refactor into dev
  • show error messages if linting fails
  • split linting to separate stage

I've set the build stages to run out-of-order w.r.t. the build stage. this means that the build stages will proceed even if linting fails. the advantage of this is that we can split in stages without making the critical path of the CI longer. OTOH, this introduces the possibility that the builds are run even though something is wrong with the configure files.

Compare: https://gitlab.com/nomadic-labs/mi-cho-coq/-/pipelines/282717927 pl-11281034-282717927

With: https://gitlab.com/nomadic-labs/mi-cho-coq/-/pipelines/282714155 pl-11281034-282714155

Spoiler: the difference in run-time is minimal. But it doesn't really make sense to run the same linters in different versions of coq ;)

Edited by Arvid Jakobsson

Merge request reports