Skip to content

Language翻訳

Language翻訳 #27

Workflow file for this run

on:
push:
branches:
- main
pull_request:
workflow_dispatch:
permissions:
contents: read
pages: write
id-token: write
concurrency:
group: "pages"
cancel-in-progress: false
name: Build and deploy sites
jobs:
build:
name: Build site and generate HTML
runs-on: ubuntu-latest
steps:
- name: Install deps for figures (OS packages)
run: |
sudo apt update && sudo apt install -y poppler-utils
- name: Install deps for figures (TeX)
uses: teatimeguest/setup-texlive-action@v3
with:
packages: |
scheme-minimal
latex-bin
fontspec
standalone
pgf
pdftexcmds
luatex85
infwarerr
ltxcmds
xcolor
fontawesome
spath3
inter
epstopdf-pkg
tex-gyre
sourcecodepro
- name: Install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
- uses: actions/checkout@v4
- name: Lean Version
run: |
lean --version
- name: Cache .lake
uses: actions/cache@v4
with:
path: .lake
key: ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{ github.sha }}
restore-keys: |
${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{ github.sha }}
${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}
${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-
- name: Build
run: |
lake build
- name: Generate HTML
run: |
lake exe generate-manual --depth 2 --with-word-count "words.txt"
- name: Generate proofreading HTML
if: github.event_name == 'pull_request'
run: |
lake exe generate-manual --depth 2 --with-word-count "words.txt" --draft --output "_out/draft"
- name: Report word count
run: |
echo "Word Counts"
echo "-----------"
cat words.txt
- name: Save word count
run: |
echo "# Word Counts" >> $GITHUB_STEP_SUMMARY
echo "" >> $GITHUB_STEP_SUMMARY
echo "\`\`\`" >> $GITHUB_STEP_SUMMARY
cat words.txt >> $GITHUB_STEP_SUMMARY
echo "\`\`\`" >> $GITHUB_STEP_SUMMARY
- name: Offline link checker
uses: lycheeverse/lychee-action@v1.9.0
with:
fail: true
args: --base './_out/html-multi/' --no-progress --offline './_out/html-multi/**/*.html'
- name: Upload artifact
uses: actions/upload-pages-artifact@v3
with:
path: _out/html-multi
# Deployment job
deploy:
if: github.ref == 'refs/heads/main'
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
runs-on: ubuntu-latest
needs: build
steps:
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v4
check-links:
name: Check links
runs-on: ubuntu-latest
needs: [build]
steps:
- uses: actions/checkout@v4
with:
sparse-checkout: |
.skip-link-check
- name: Online link checker
uses: filiph/linkcheck@2.0.23
continue-on-error: true
with:
arguments: --skip-file .skip-link-check -e ${{ needs.build.outputs.ref-url }}