Skip to content

whitepaper: add section about quick compilation requirement #67

whitepaper: add section about quick compilation requirement

whitepaper: add section about quick compilation requirement #67

Workflow file for this run

name: Book
on:
push:
branches:
- main
pull_request:
jobs:
book:
name: Build and deploy
runs-on: ubuntu-latest
permissions:
contents: write
steps:
- name: Checkout repository and submodules
uses: actions/checkout@v3
with:
fetch-depth: 0
submodules: recursive
- name: Cache build artifacts
uses: actions/cache@v3
with:
path: |
~/.cargo/bin/
~/.cargo/registry/index/
~/.cargo/registry/cache/
~/.cargo/git/db/
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
${{ runner.os }}-
- name: Install mdbook
uses: peaceiris/actions-mdbook@v1
with:
mdbook-version: '0.4.10'
- name: Install mdbook-linkcheck
run: |
version="v0.7.4"
file="mdbook-linkcheck"
zip_file="mdbook-linkcheck.${version}.x86_64-unknown-linux-gnu.zip"
curl -sSL https://github.com/Michael-F-Bryan/mdbook-linkcheck/releases/download/${version}/${zip_file} --output ${zip_file}
unzip -d bin ${zip_file} ${file}
chmod +x bin/${file}
rm ${zip_file}
echo "$(pwd)/bin" >> ${GITHUB_PATH}
- name: Report versions
run: |
mdbook --version
mdbook-linkcheck --version
# Remove book directory cache before publishing.
- name: Clean book build directory before publishing
if: github.event_name == 'push' && github.ref == 'refs/heads/main'
run: mdbook clean
- name: Build book
run: mdbook build
- name: Run spell check
uses: streetsidesoftware/cspell-action@v2
with:
config: './cspell.json'
files: './src/**'
incremental_files_only: false
# Enforce strict spell check except on push to main branch.
strict: ${{ !(github.event_name == 'push' && github.ref == 'refs/heads/main') }}
# Move build artifacts to publish directory on push to main branch.
- name: Move build artifacts
if: github.event_name == 'push' && github.ref == 'refs/heads/main'
run: |
rm -rf ./github_pages/
mv ./book/html/ ./github_pages/
# Deploy on push to main branch.
- name: Deploy
if: github.event_name == 'push' && github.ref == 'refs/heads/main'
uses: peaceiris/actions-gh-pages@v3
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
commit_message: ${{ github.event.head_commit.message }}
publish_branch: github_pages
publish_dir: ./github_pages