diff options
author | Ben Gamari <ben@smart-cactus.org> | 2020-07-04 22:32:15 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-08-18 15:40:05 -0400 |
commit | fdcf76450348d0554b7fd1768331f9efaf691e13 (patch) | |
tree | ba38d3e50e57b83b858c8973ac44fdbdb08f8f52 /.gitlab-ci.yml | |
parent | 194b25ee97d93bc4bcb5bed9a0454debba7f2b6a (diff) | |
download | haskell-fdcf76450348d0554b7fd1768331f9efaf691e13.tar.gz |
gitlab-ci: Use MR base commit as performance baseline
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r-- | .gitlab-ci.yml | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 73c8aa8481..aad9526648 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -26,12 +26,28 @@ stages: - testing # head.hackage correctness and compiler performance testing - deploy # push documentation +# Note [The CI Story] +# ~~~~~~~~~~~~~~~~~~~ +# +# There are two different types of pipelines: +# +# - marge-bot merges to `master`. Here we perform an exhaustive validation +# across all of the platforms which we support. In addition, we push +# performance metric notes upstream, providing a persistent record of the +# performance characteristics of the compiler. +# +# - merge requests. Here we perform a slightly less exhaustive battery of +# testing. Namely we omit some configurations (e.g. the unregisterised job). +# These use the merge request's base commit for performance metric +# comparisons. +# + workflow: - # N.B.Don't run on wip/ branches, instead on run on merge requests. + # N.B. Don't run on wip/ branches, instead on run on merge requests. rules: - if: $CI_MERGE_REQUEST_ID - if: $CI_COMMIT_TAG - - if: '$CI_COMMIT_BRANCH == "master"' + - if: '$CI_COMMIT_BRANCH == "wip/marge_bot_batch_merge_job"' - if: '$CI_COMMIT_BRANCH =~ /ghc-[0.9]+\.[0-9]+/' - if: '$CI_PIPELINE_SOURCE == "web"' |