blob: c51246ee030f2315729097def051992765b46179 (
plain)
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
|
name: documentation update
on:
push:
paths:
- '.github/**'
- 'docs/**'
- 'examples/**'
- 'src/api/**'
pull_request_target:
paths:
- '.github/**'
- 'docs/**'
- 'examples/**'
- 'src/api/**'
# When run by pull_request_target (in comparison to pull_request), the action
# has access to the repository secrets so that we can push the generated docs.
# To allow this, the action is run in the context of the master branch instead
# of the PR. We therefore obtain the changes from the PR manually,
# but need to be very careful to not pull any changes to files that are executed
# during configuration or build. At the same time, we try to include as many
# files as possible that may change how the documentations looks like.
# To ensure this, we only checkout a very selected set of files from the PR
# branch:
# - docs/**.(bib|rst)
# - src/api/**.(cpp|h|java|py)
# - examples/**.(cpp|h|java|py|smt2)
# In particular, we should not checkout any CMakeLists.txt files or any python
# files used by sphinx.
jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- name: Install Packages
run: |
sudo apt-get update
sudo apt-get install -y \
build-essential \
libgmp-dev \
doxygen \
python3-docutils python3-jinja2
python3 -m pip install \
setuptools toml pytest \
sphinxcontrib-bibtex sphinx-tabs sphinx-rtd-theme \
breathe
python3 -m pip install \
Cython==0.29.* --install-option="--no-cython-compile"
echo "$(python3 -m site --user-base)/bin" >> $GITHUB_PATH
- name: Checkout PR
run: |
git config --global user.email "docbot@cvc5"
git config --global user.name "DocBot"
if [ "${{ github.event_name }}" == "push" ] ; then
NAME=$(echo "${GITHUB_REF}" | sed "s,refs/heads/,,")
echo "Identified branch $NAME"
elif [ "${{ github.event_name }}" == "pull_request_target" ] ; then
NAME="${{ github.event.number }}"
PRHASH="${{ github.event.pull_request.head.sha }}"
echo "Identified PR #$NAME (from $PRHASH)"
NAME="pr$NAME"
# be careful here, see explanation above!
git fetch
git checkout "${PRHASH}" -- \
`git ls-tree "${PRHASH}" --name-only -r docs/ | grep -E ".*\.(rst|bib)"` \
`git ls-tree "${PRHASH}" --name-only -r src/api/ | grep -E ".*\.(h|cpp|java|py)"` \
`git ls-tree "${PRHASH}" --name-only -r examples/ | grep -E ".*\.(h|cpp|java|py|smt2)"`
fi
echo "NAME=$NAME" >> $GITHUB_ENV
- name: Configure
run: ./configure.sh production --docs --all-bindings
- name: Build
run: make -j2 docs-gh
working-directory: build
- name: Setup Deploy Key
env:
SSH_AUTH_SOCK: /tmp/ssh_agent.sock
run: |
ssh-agent -a $SSH_AUTH_SOCK > /dev/null
ssh-add - <<< "${{ secrets.CVC5_DOCS_TOKEN }}"
- name: Update docs
continue-on-error: true
env:
SSH_AUTH_SOCK: /tmp/ssh_agent.sock
run: |
git clone git@github.com:cvc5/docs-ci.git target/
if [ -n "$NAME" ]; then
rsync -a --delete build/docs/sphinx-gh/ target/docs-$NAME-${{ github.sha }}
cd target/
rm -f docs-$NAME
ln -s docs-$NAME-${{ github.sha }} docs-$NAME
git add docs-$NAME docs-$NAME-${{ github.sha }}
python3 genindex.py
git add README.md
git commit -m "Update docs for $NAME"
git push
else
echo "Ignored run"
fi
|
