Skip to content

Commit

Permalink
CI: delete .git of downloaded projects to reduce artifact size
Browse files Browse the repository at this point in the history
fiat-crypto artifacts seem to hover around 500MB (zipped) which seems
to be the limit. This should reduce that by over 100MB.

(Notably I see pack-dd3467f8c46a76be48de952ac01a5396f376deb6.pack with
compressed size 150MB in the artifacts of https://gitlab.inria.fr/coq/coq/-/jobs/3599481)
  • Loading branch information
SkySkimmer committed Nov 19, 2023
1 parent 3c53872 commit 2c0127f
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion dev/ci/ci-common.sh
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,9 @@ set -x
# in [$CI_BUILD_DIR/project] if the folder does not exist already;
# if it does, it will do nothing except print a warning (this can be
# useful when building locally).
# Note: when $FORCE_GIT is set to 1 or when $CI is unset or empty
# Note: when there is an overlay, $WITH_SUBMODULES is set to 1 or $CI is unset or empty
# (local build), it uses git clone to perform the download.
# If $CI is nonempty it then removes the .git (to reduce artifact size)
git_download()
{
local project=$1
Expand Down Expand Up @@ -135,6 +136,9 @@ git_download()
if [ "$WITH_SUBMODULES" = 1 ]; then
git submodule update --init --recursive
fi
if [ "$CI" ]; then
rm -rf .git
fi
popd
else # When possible, we download tarballs to reduce bandwidth and latency
local archiveurl_var="${project}_CI_ARCHIVEURL"
Expand Down

0 comments on commit 2c0127f

Please sign in to comment.