diff options
| author | Ben Gamari <ben@smart-cactus.org> | 2021-07-25 15:45:34 -0400 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-09-23 16:00:17 -0400 |
| commit | ca88d91c055d877412626f92973b1f896bcb8b79 (patch) | |
| tree | a61079da867b105b513d6777750a7ba84dd2e96e /.gitlab/ci.sh | |
| parent | aafda13d3746ca8185c89f2f3eca77470f09b746 (diff) | |
| download | haskell-ca88d91c055d877412626f92973b1f896bcb8b79.tar.gz | |
ci: Consolidate handling of cabal cache
Previously the cache persistence was implemented as various ad-hoc `cp`
commands at the end of the individual CI scripts. Here we move all of
this logic into `ci.sh`.
Diffstat (limited to '.gitlab/ci.sh')
| -rwxr-xr-x | .gitlab/ci.sh | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/.gitlab/ci.sh b/.gitlab/ci.sh index a89ec93a93..b3522f59e6 100755 --- a/.gitlab/ci.sh +++ b/.gitlab/ci.sh @@ -20,6 +20,20 @@ CABAL_CACHE="$TOP/${CABAL_CACHE:-cabal-cache}" source "$TOP/.gitlab/common.sh" +function time_it() { + local name="$1" + shift + local start=$(date +%s) + local res=0 + $@ || res=$? + local end=$(date +%s) + local delta=$(expr $end - $start) + + echo "$name took $delta seconds" + printf "%15s | $delta" > ci-timings + return $res +} + function usage() { cat <<EOF $0 - GHC continuous integration driver @@ -31,6 +45,7 @@ Common Modes: configure Run ./configure. clean Clean the tree shell Run an interactive shell with a configured build environment. + save_cache Preserve the cabal cache Make build system: @@ -610,7 +625,7 @@ case $1 in perf_test) run_perf_test ;; cabal_test) cabal_test ;; clean) clean ;; - save-cache) save_cache ;; + save_cache) save_cache ;; shell) shell "$@" ;; *) fail "unknown mode $1" ;; esac |