-
Notifications
You must be signed in to change notification settings - Fork 150
156 lines (141 loc) · 7 KB
/
coq-timing-diff.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
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.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
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
env:
GH_TOKEN: ${{ github.token }}
run: |
# 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