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: Upload Docs
on:
workflow_run:
workflows: ["CI"]
types:
- completed
jobs:
upload-docs:
name: upload-docs
runs-on: ubuntu-latest
continue-on-error: true
if: github.repository == 'cvc5/cvc5' && github.event.workflow_run.conclusion == 'success'
steps:
- name: Setup git config
run: |
git config --global user.email "docbot@cvc5"
git config --global user.name "DocBot"
- name: Download artifact
uses: actions/github-script@v8
with:
script: |
var artifacts = await github.rest.actions.listWorkflowRunArtifacts({
owner: context.repo.owner,
repo: context.repo.repo,
run_id: ${{github.event.workflow_run.id }},
});
var matchArtifact = artifacts.data.artifacts.filter((artifact) => {
return artifact.name == "documentation"
})[0];
var download = await github.rest.actions.downloadArtifact({
owner: context.repo.owner,
repo: context.repo.repo,
artifact_id: matchArtifact.id,
archive_format: 'zip',
});
var fs = require('fs');
fs.writeFileSync('${{github.workspace}}/download.zip', Buffer.from(download.data));
- name: Unpack artifact
run: unzip download.zip -d docs-new/
# disabled, causes websites like gmplib.org to trigger their anti-dos
# measure, which causes the action to time out
#- name: Check for broken links
# continue-on-error: true
# run: |
# python3 -m pip install linkchecker
# linkchecker --check-extern docs-new/index.html
# This workflow is run for commits in PRs (from branches in forks), commits
# (from branches in main repo, usually main branch) and tags. Unfortunately,
# there are only two properties in the github context that can be used here:
# - workflow_run.event is "pull_request" for PRs and "push" otherwise
# - workflow_run.head_branch contains the branch or tag name
# We can not reliably identify a tag from that, so we simply match the
# head_branch against the naming pattern of our tags ("cvc5-*"). To prevent PRs
# with a matching branch name to be recognized as tags, we proceed as follows:
# - handle PRs (event == "pull_request")
# - handle tags (head_branch == "cvc5-*")
# - rest are regular commits
- name: Setup Context
run: |
HASH=${{ github.event.workflow_run.head_commit.id }}
ISRELEASE=false
if [ "${{ github.event.workflow_run.event }}" == "pull_request" ] ; then
NAME=$(cat docs-new/prnum)
rm docs-new/prnum
echo "Identified PR #$NAME (from $HASH)"
NAME="pr$NAME"
elif [ "${{ startsWith(github.event.workflow_run.head_branch, 'cvc5-') }}" == "true" ] ; then
ISRELEASE=true
NAME=${{ github.event.workflow_run.head_branch }}
echo "Identified tag $NAME"
elif [ "${{ github.event.workflow_run.event }}" == "push" ] ; then
NAME=${{ github.event.workflow_run.head_branch }}
echo "Identified branch $NAME"
fi
echo "NAME=$NAME" >> $GITHUB_ENV
echo "HASH=$HASH" >> $GITHUB_ENV
echo "ISRELEASE=$ISRELEASE" >> $GITHUB_ENV
- name: Update versions
continue-on-error: true
run: |
python3 -m pip install beautifulsoup4 lxml
eval $(ssh-agent -s)
ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}"
git clone git@github.com:cvc5/docs.git target-releases/
TARGET_DIR=
if [ "$ISRELEASE" = true ]; then
TARGET_DIR=target-releases/$NAME
else
TARGET_DIR=target-releases/cvc5-main
fi
cp -r docs-new "${TARGET_DIR}"
pushd target-releases/
python3 genversions.py
popd
cp -rf "${TARGET_DIR}" docs-new
- name: Update docs
continue-on-error: true
run: |
if [ -n "$NAME" ]; then
eval $(ssh-agent -s)
ssh-add - <<< "${{ secrets.CVC5_DOCS_TOKEN }}"
git clone git@github.com:cvc5/docs-ci.git target/
cp -r docs-new target/docs-$NAME-$HASH
cd target/
isdiff=$(diff -r -x "*.zip" docs-main/ docs-$NAME-$HASH >&2; echo $?; exit 0)
if [[ ("$ISRELEASE" != true) && ($isdiff = 0) ]]
then
echo "Ignored run, documentation is the same as for current main"
else
rm -f docs-$NAME
ln -s docs-$NAME-$HASH docs-$NAME
git add docs-$NAME docs-$NAME-$HASH
python3 genindex.py
git add README.md
git commit -m "Update docs for $NAME"
git push
fi
else
echo "Ignored run"
fi
- name: Update docs for release
continue-on-error: true
run: |
if [ "$ISRELEASE" = true ]; then
eval $(ssh-agent -s)
ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}"
cd target-releases/
rm -f latest
ln -s $NAME latest
git add .
git commit -m "Update docs for $NAME"
git push
else
echo "Ignored run"
fi
|
