Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merging new commits to master causes numerous CI cache misses #1209

Closed
2 tasks
lisanna-dettwyler opened this issue Jun 2, 2021 · 0 comments
Closed
2 tasks
Labels
build system Related to Cryptol's build system CI Continuous integration

Comments

@lisanna-dettwyler
Copy link
Contributor

lisanna-dettwyler commented Jun 2, 2021

Building HEAD of master takes a long time when there are significant cache misses. This mostly affects macOS and docker image building. When a change is merged that causes cache misses in master, these misses also arise in subsequent rebuilds of pull requests even if they haven't been rebased/updated since. Some things that can be done about this:

  • Additionally use the git merge-base as a cache key, which remains fixed if the pull request remains fixed:
    - id: merge-base
      shell: bash
      run: |
        MERGE_BASE=$(git merge-base ${{ github.head_ref }} ${{ github.base_ref }})
        echo "::set-output name=ref::$MERGE_BASE"
    - uses: actions/cache@v2
      key: ${{ github.head_ref }}
      restore-keys: |
        ${{ steps.merge-base.outputs.ref }}
        ${{ github.base_ref }})
  • Generate build cache for master faster (on: push: master), i.e., significantly reign-in compile times
@lisanna-dettwyler lisanna-dettwyler added the build system Related to Cryptol's build system label Jun 2, 2021
@lisanna-dettwyler lisanna-dettwyler changed the title Merging new commits to master causes numerous cache problems Merging new commits to master causes numerous CI cache problems Jun 2, 2021
@kquick kquick added the CI Continuous integration label Aug 13, 2021
@kquick kquick changed the title Merging new commits to master causes numerous CI cache problems Merging new commits to master causes numerous CI cache misses Aug 13, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
build system Related to Cryptol's build system CI Continuous integration
Projects
None yet
Development

No branches or pull requests

3 participants