Open Zimmi48 opened 3 years ago
What does this have to do with cachedMake
? I do not see a call to it and it is not used in the toolbox generated CI.
This build-doc
step is manually implemented (and inserted in the generated CI configuration). It does the following:
build-doc:
needs:
- hydra-battles-single
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v14
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup coq
uses: cachix/cachix-action@v10
with:
name: coq
- name: Cachix setup coq-community
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
name: coq-community
- name: Cachix setup math-comp
uses: cachix/cachix-action@v10
with:
name: math-comp
- name: Retrieve prebuilt vo files
run: |
nix-shell --run "make Makefile.coq"
nix-shell --run "cachedMake"
nix-shell --run "make -t"
- name: Build Alectryon snippets
run: nix-shell --run "make -C doc/movies -j $(nproc) all"
- name: Build coqdoc
run: nix-shell --run "make -j $(nproc) html"
- name: Compile LaTeX document
run: nix-shell --run "make pdf SOURCE_DATE_EPOCH=$(date +%s)"
- name: Extract PDF and Coqdoc
run: |
mkdir -p public/doc public/theories
cp doc/hydras.pdf public/doc/
cp -r theories/html public/theories/
# Depending on whether we are on master or not, we deploy to
# GitHub Pages or as an artifact
- name: Deploy to GitHub pages
if: github.event_name == 'push' && github.ref == 'refs/heads/master'
uses: crazy-max/ghaction-github-pages@v2
with:
build_dir: public
jekyll: false
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- name: Deploy artifact
if: github.event_name != 'push' || github.ref != 'refs/heads/master'
uses: actions/upload-artifact@v2
with:
path: public
Notice that the step "Retrieve prebuilt vo files" calls cachedMake
to retrieve prebuilt vo files.
In https://github.com/coq-community/hydra-battles/runs/4054266890?check_suite_focus=true, we got an error of the following form while building a coqdoc target:
In principle, the file should have been built in a previous job (
hydra-battles-single
) and retrieved withcachedMake
.Is this possible that this retrieval step led to an incomplete file?
Restarting the job made it pass.