Rework timing diff workflog

JasonGross · Mar 4, 2025 · b8e499e · b8e499e
1 parent 77571a8
commit b8e499e
Showing 1 changed file with 38 additions and 29 deletions.
diff --git a/.github/workflows/coq-timing-diff.yml b/.github/workflows/coq-timing-diff.yml
@@ -35,29 +35,8 @@ jobs:
         custom_script: |
           eval $(opam env)
           etc/ci/describe-system-config.sh
-    - 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
-      id: timing_diff
+    - name: compute base sha and current branch
+      id: git_ids
       run: |
         # Get the current branch name
         CURRENT_BRANCH=${GITHUB_REF#refs/heads/}
@@ -79,18 +58,48 @@ jobs:
 
         echo "Using base SHA: $BASE_SHA"
         echo "Current branch: $CURRENT_BRANCH"
-
-        # Run the timing diff script
-        etc/coq-scripts/timing/make-pretty-timed-diff-branch.sh "$BASE_SHA" "$CURRENT_BRANCH"
+        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
+          etc/coq-scripts/timing/make-pretty-timed-diff-branch.sh "$BASE_SHA" "$CURRENT_BRANCH"
 
     - name: Display commits between base and current
-      id: display_commits
       run: |
-        BASE_SHA=${{ steps.timing_diff.outputs.base_sha }}
-        CURRENT_BRANCH=${{ steps.timing_diff.outputs.current_branch }}
+        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