Using a base image for CI jobs #2927
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
See the logs here https://github.com/FStarLang/FStar/actions/runs/4973169264/jobs/8898832659. Building the base took 8m28s and running CI took 9m7s. We didn't get a Slack message, since apparently this ran without the secret. |
mtzguido
force-pushed
the
guido_ci_baseimage
branch
from
fd4195a
to
364533a
Compare
This enables performance monitoring (as in building with `RESOURCEMONITOR=1`) for CI builds. It is conditioned by the `FSTAR_CI_RESOURCEMONITOR` variable. It must be set to `1` in the variables for the repository (Settings -> Secrets and variables -> Actions -> Variables) for the monitoring to be enabled. It is currently already enabled even without this PR. In detail: 0) The workflow will pass the RESOURCEMONITOR=1 file to the Docker build command, this will cause our Makefiles to create .runlim files everywhere. 1) build-standalone.sh will, after running CI, create an `rmon/` directory and place relevant information there, including the summary generated by `.scripts/res_summary.sh` as well as all of the individual `.runlim` files ordered by path. 2) The workflow picks this directory up, and uploads two Github build artifacts, one with the summary and one with the tarball of all .runlim files. 3) Two lines added to the Slack message with total CPU and memory usage (to be seen how robust this measurement will be). Plus, a link to the resource summary pasted into sprunge.us, for a one-click view. Github makes a .zip archive of an artifact when one tries to download it (even if it contains a single file), which is annoying, but I don't think there's an alternative currently. Also, zipping seems to be slow, and can add minutes(!) to the build. So we make a compressed tarball of the .runlim files first, and upload that.
mtzguido
force-pushed
the
guido_ci_baseimage
branch
from
62e0dfe
to
d5d0997
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR makes CI jobs (only the regular CI workflow on Linux; releases and others are unaffected) start from a base docker image instead of from scratch. This saves time as we don't have to install dependencies (which includes building Z3) on every push.
This change is rather annoying to make as there is no (to my knowledge) way of doing this kind of thing with buildx, especially if we need to avoid this. So, this PR changes the workflow to not use buildx for normal CI jobs. Other workflows still can use it.
The main benefit we got from buildx is safely passing a secret while the image is being built, which we use for the github token so we can advance hints. I've worked around that by building the image without any such secret nor advancing hints, and using
docker run, which runs a container from an image, after the fact (passing the secret) to push to github. This container is not published anywhere.The base image is rebuilt nightly (2AM UTC) and, if F* CI passes on it, it is tagged. If CI fails we do not tag, so CI jobs can still run, but we get a notification in Slack so we can fix the base. This is intended to not block people when some upstream dependency breaks.
Note that this slightly relies on the fact that we run all CI jobs on the same machine. The image rebuilding workflow affects the state of the docker installation on the machine so it can be taken by other workflows. If we have more than one machine runner, we would have to run this job once for every machine. Perhaps a cron job is more appropriate.
This also supersedes #2919. However the numbers we are getting vary quite wildly, so maybe we should disable it for now.
I've been testing this on a local runner and CI time reduces by about 50%.