coq-timing-diff.yml

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