CI (Coq, timing-diff, docker, dev) #1
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
| name: CI (Coq, timing-diff, docker, dev) | |
| on: | |
| workflow_dispatch: | |
| inputs: | |
| build_target: | |
| description: 'Build target for timing diff' | |
| required: false | |
| default: 'standalone-ocaml lite-generated-files' | |
| type: string | |
| target_repository: | |
| description: 'Target repository to checkout (e.g., username/repo)' | |
| required: false | |
| default: '' | |
| type: string | |
| target_branch: | |
| description: 'Target branch to checkout' | |
| required: false | |
| default: '' | |
| type: string | |
| jobs: | |
| build: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev", DOCKER_OCAML_VERSION: "default", SKIP_VALIDATE: "" , COQCHKEXTRAFLAGS: "-bytecode-compiler yes", EXTRA_GH_REPORTIFY: "--warnings", ALLOW_DIFF: "1", CI: "1" } | |
| os: 'ubuntu-latest' | |
| runs-on: ${{ matrix.os }} | |
| env: ${{ matrix.env }} | |
| name: docker-${{ matrix.env.COQ_VERSION }} | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| repository: ${{ github.event.inputs.target_repository || github.repository }} | |
| ref: ${{ github.event.inputs.target_branch || github.ref }} | |
| - name: echo host build params | |
| run: etc/ci/describe-system-config.sh | |
| - name: echo container build params | |
| uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | |
| ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | |
| export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY | |
| custom_script: | | |
| eval $(opam env) | |
| etc/ci/describe-system-config.sh | |
| - name: compute base sha and current branch | |
| id: git_ids | |
| run: | | |
| git remote add upstream https://github.com/mit-plv/fiat-crypto.git | |
| git remote update | |
| # Get the current branch name | |
| CURRENT_BRANCH=${GITHUB_REF#refs/heads/} | |
| echo "Current branch: $CURRENT_BRANCH" | |
| # Check if this is a PR | |
| # Check if this branch has an associated PR | |
| PR_NUMBER=$(gh pr list --repo mit-plv/fiat-crypto --head $CURRENT_BRANCH --json number --jq '.[0].number') | |
| if [[ -n "$PR_NUMBER" ]]; then | |
| # Get the base branch from the PR | |
| BASE_BRANCH=$(gh pr view $PR_NUMBER --json baseRefName --jq '.baseRefName') | |
| echo "This branch has PR #$PR_NUMBER from $CURRENT_BRANCH to $BASE_BRANCH" | |
| # Get the merge-base of the base branch and current commit | |
| BASE_SHA=$(git merge-base origin/$BASE_BRANCH $GITHUB_SHA) | |
| else | |
| # For non-PRs, use merge-base of current branch and master as base_sha | |
| echo "This is not a PR, using merge-base with master" | |
| BASE_SHA=$(git merge-base origin/master $GITHUB_SHA) | |
| fi | |
| echo "Using base SHA: $BASE_SHA" | |
| git log --oneline $BASE_SHA..$CURRENT_BRANCH | |
| echo "base_sha=${BASE_SHA}" >> $GITHUB_OUTPUT | |
| echo "current_branch=${CURRENT_BRANCH}" >> $GITHUB_OUTPUT | |
| - name: deps | |
| uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | |
| ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | |
| export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY | |
| custom_script: etc/ci/github-actions-docker-make.sh COQBIN="$(dirname "$(which coqc)")/" -j2 deps | |
| - name: all-except-generated-and-js-of-ocaml | |
| uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | |
| ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | |
| export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY | |
| custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated-and-js-of-ocaml | |
| - name: pre-standalone-extracted | |
| uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | |
| ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | |
| export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY | |
| custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 pre-standalone-extracted | |
| - name: run timing diff | |
| uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | |
| ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | |
| export: CI ALLOW_DIFF COQCHKEXTRAFLAGS GITHUB_STEP_SUMMARY | |
| custom_script: | | |
| BASE_SHA=${{ steps.git_ids.outputs.base_sha }} | |
| CURRENT_BRANCH=${{ steps.git_ids.outputs.current_branch }} | |
| # Run the timing diff script | |
| eval $(opam env) | |
| etc/coq-scripts/timing/make-pretty-timed-diff-branch.sh "$BASE_SHA" "$CURRENT_BRANCH" ${{ github.event.inputs.build_target }} | |
| - name: Display commits between base and current | |
| run: | | |
| BASE_SHA=${{ steps.git_ids.outputs.base_sha }} | |
| CURRENT_BRANCH=${{ steps.git_ids.outputs.current_branch }} | |
| echo "### Commits between base and current branch" >> $GITHUB_STEP_SUMMARY | |
| echo "" >> $GITHUB_STEP_SUMMARY | |
| # Get each commit hash between base and current branch | |
| COMMIT_HASHES=$(git log --pretty=format:"%H" $BASE_SHA..$CURRENT_BRANCH) | |
| # For each commit, create a separate details/summary section | |
| for COMMIT in $COMMIT_HASHES; do | |
| # Get commit details | |
| COMMIT_SHORT=$(git log -1 --pretty=format:"%h" $COMMIT) | |
| COMMIT_SUBJECT=$(git log -1 --pretty=format:"%s" $COMMIT) | |
| COMMIT_FULL=$(git log -1 --pretty=format:"%B" $COMMIT) | |
| # Add to step summary - just oneline in summary | |
| printf "<details>\n" >> $GITHUB_STEP_SUMMARY | |
| printf "<summary>%s: %s</summary>\n" "$COMMIT_SHORT" "$COMMIT_SUBJECT" >> $GITHUB_STEP_SUMMARY | |
| printf "\n" >> $GITHUB_STEP_SUMMARY | |
| # printf "```\n" >> $GITHUB_STEP_SUMMARY | |
| printf "%s\n" "$COMMIT_FULL" >> $GITHUB_STEP_SUMMARY | |
| # printf "```\n" >> $GITHUB_STEP_SUMMARY | |
| printf "</details>\n" >> $GITHUB_STEP_SUMMARY | |
| printf "\n" >> $GITHUB_STEP_SUMMARY | |
| # Output to GitHub Actions log with groups - oneline in group name | |
| printf "::group::%s: %s\n" "$COMMIT_SHORT" "$COMMIT_SUBJECT" | |
| git log -1 --pretty=fuller $COMMIT | |
| printf "::endgroup::\n" | |
| done |