Skip to content

Commit 2c3d166

Browse files
committed
doc: add extra documentation to CI
1 parent e4a52ad commit 2c3d166

File tree

3 files changed

+10
-3
lines changed

3 files changed

+10
-3
lines changed

.github/actions/checkout_workspace/action.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
name: "Checkout Workspace Directory"
2-
description: ""
2+
description: "Can be invoked multiple times. Depends on `prepare_workspace`."
33

44
inputs:
55
CHECKOUT_BASE:

.github/actions/prepare_workspace/action.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
name: "Prepare to Checkout Workspace Directory"
2-
description: ""
2+
description: "Invoked exactly once per job. Depends on 'Download CI files' step."
33

44
inputs:
55
FM_CI_TOKEN:

.github/workflows/main.yml

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,9 @@ env:
2626
OPAM_PACKAGES: opam pin | grep /fmdeps/ | grep -v rocq-test-suite
2727

2828
jobs:
29+
2930
gen-job:
31+
name: "Choose commits to compare"
3032
runs-on:
3133
group: FM
3234
container:
@@ -71,7 +73,10 @@ jobs:
7173
workspace_checkout/.github/workflows/*
7274
7375
76+
# MR merging can require this check to succeed, to depend on all of CI.
77+
# MAINTENANCE NOTE: Must depend on all "actual" jobs
7478
workspace-success:
79+
name: "Check if CI succeeded"
7580
needs: [opam-build, full-build, python-build]
7681
if: always()
7782
runs-on: ubuntu-latest
@@ -86,7 +91,8 @@ jobs:
8691
echo "Checking that python-build succeeded"
8792
${{ needs.python-build.result == 'success' && 'true' || 'false' }}
8893
89-
94+
# Regular jobs [should] follow the template of `opam-build` up to
95+
# `checkout_workspace`, and then add their payload.
9096
opam-build:
9197
needs: gen-job
9298
defaults:
@@ -231,6 +237,7 @@ jobs:
231237
uv --directory ${{ matrix.project-dir }} run task ${{ matrix.task }}
232238
233239
240+
# Unlike opam-build, this job invokes checkout_workspace twice not once.
234241
full-build:
235242
needs: gen-job
236243
defaults:

0 commit comments

Comments
 (0)