CI (Coq, timing-diff, docker, dev) #6
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: true | |
| 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.event.inputs.target_repository || github.repository }}-${{ github.event.inputs.target_branch || github.ref }}-${{ github.event.inputs.build_target }}${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| steps: | |
| - name: record inputs to summary | |
| run: | | |
| printf "%s@%s make %s\n\n" "${{ github.event.inputs.target_repository || github.repository }}" "${{ github.event.inputs.target_branch || github.ref }}" "${{ github.event.inputs.build_target }}" | |
| printf "%s@%s make %s\n\n" "${{ github.event.inputs.target_repository || github.repository }}" "${{ github.event.inputs.target_branch || github.ref }}" "${{ github.event.inputs.build_target }}" >> $GITHUB_STEP_SUMMARY | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - 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 | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| # Get the current branch name | |
| CURRENT_BRANCH=${{ github.event.inputs.target_branch }} | |
| 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') | |
| # Add remote for target repository if specified | |
| if [[ -n "${{ github.event.inputs.target_repository }}" && "${{ github.event.inputs.target_repository }}" != "${{ github.repository }}" ]]; then | |
| echo "Adding remote for target repository: ${{ github.event.inputs.target_repository }}" | |
| git remote add target_repo "https://github.com/${{ github.event.inputs.target_repository }}.git" | |
| git fetch target_repo $CURRENT_BRANCH || true | |
| git checkout -b $CURRENT_BRANCH target_repo/$CURRENT_BRANCH | |
| else | |
| git fetch origin $CURRENT_BRANCH || true | |
| git checkout -b $CURRENT_BRANCH origin/$CURRENT_BRANCH | |
| fi | |
| 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 | |
| git fetch origin $BASE_BRANCH || true | |
| BASE_SHA=$(git merge-base target_repo/$BASE_BRANCH $CURRENT_BRANCH) | |
| 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" | |
| git fetch origin master || true | |
| BASE_SHA=$(git merge-base master $CURRENT_BRANCH) | |
| 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 |