Skip to content

Commit

Permalink
Track reproducibility index history
Browse files Browse the repository at this point in the history
Use a separate branch, and a similar workflow to that used for Rust
documentation, using GitHub Actions to push changes.

Ref project-oak#861
  • Loading branch information
tiziano88 committed Apr 30, 2020
1 parent 01d4558 commit 4f4edc3
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/build_rust_docs.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ jobs:
- name: Generate docs
run: ./scripts/docker_run ./scripts/build_gh_pages ./out

# From the "out" folder, commit the results and push to gh-pages.
# From the "out" folder, commit the results and push to the `gh-pages` branch.
# This step only applies to `push` events (not `pull_request`), and only if there are actual
# changes to commit in the "out" folder.
- name: Commit and push (post-merge only)
Expand Down
38 changes: 38 additions & 0 deletions .github/workflows/reproducibility.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,18 @@ jobs:
- name: Checkout branch
uses: actions/checkout@v2

- name: Checkout hashes
uses: actions/checkout@v2
with:
ref: hashes
path: out

# We need to set up git user details before we can perform git operations.
- name: Git setup
run: |
git config --global user.email "actions@github.com"
git config --global user.name "GitHub Actions"
# Build Docker image, caching from the latest version from the remote repository.
- name: Docker build
timeout-minutes: 30
Expand All @@ -32,10 +44,36 @@ jobs:
- name: Generate Reproducibility Index
run: ./scripts/docker_run ./scripts/build_reproducibility_index

# Remove all files from the "out" folder.
- name: Clear "out" folder
run: rm --recursive --force ./out/*

- name: Copy Reproducibility Index
run: cp ./reproducibility_index ./out/

- name: Diff Reproducibility Index
run: |
cd ./out
echo test
git diff
# Print out the index to the logs of the action.
- name: Print Reproducibility Index
run: cat ./reproducibility_index

# From the "out" folder, commit the results and push to the `hashes` branch.
# This step only applies to `push` events (not `pull_request`), even if there are no actual
# changes to commit in the "out" folder (in which case the commit will be empty, but it will
# still be part of the history).
- name: Commit and push (post-merge only)
if: github.event_name == 'push'
run: |
cd ./out
git diff
git add .
git commit --allow-empty --message="Update hashes from ${GITHUB_SHA}"
git push
# Also post a reply on the PR thread with the contents of the index, after merge.
- name: Post Reproducibility Index (post-merge only)
uses: actions/github-script@0.9.0
Expand Down

0 comments on commit 4f4edc3

Please sign in to comment.