Skip to content

Commit

Permalink
Add useful comments
Browse files Browse the repository at this point in the history
  • Loading branch information
pitmonticone committed Jul 6, 2024
1 parent 0fc58f3 commit 9c78d44
Showing 1 changed file with 10 additions and 6 deletions.
16 changes: 10 additions & 6 deletions .github/workflows/push.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ jobs:
name: Lint style
runs-on: ubuntu-latest
steps:
# Check for long lines in .lean files and report if any lines exceed 100 characters
- name: Check for long lines
if: always()
run: |
Expand All @@ -24,14 +25,15 @@ jobs:
runs-on: ubuntu-latest
name: Build project
steps:

- name: Checkout project
uses: actions/checkout@v2
with:
fetch-depth: 0

- name: Install elan
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 # Install Lean 4
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
- name: Update docgen4
run: ~/.elan/bin/lake -R -Kenv=dev update doc-gen4
Expand All @@ -42,6 +44,7 @@ jobs:
- name: Build project
run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis

# Cache the documentation for Mathlib to save rebuild time
- name: Cache mathlib docs
uses: actions/cache@v3
with:
Expand All @@ -55,25 +58,26 @@ jobs:
!.lake/build/doc/declarations/declaration-data-BonnAnalysis*
key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
restore-keys: |
MathlibDoc- # Cache Mathlib documentation to save rebuild time
MathlibDoc-
- name: Build documentation
run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs # Build project documentation
run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs

- name: Install Python
uses: actions/setup-python@v4
with:
python-version: '3.9'
cache: 'pip'

# Install required apt packages for blueprint
- name: Install blueprint apt dependencies
run: |
sudo apt-get update -qq
sudo apt-get install -y --no-install-recommends graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
- name: Install blueprint dependencies
run: |
cd blueprint && pip install -r requirements.txt # Install Python dependencies for blueprint
cd blueprint && pip install -r requirements.txt
- name: Build blueprint and copy to `docs/blueprint`
run: inv all
Expand All @@ -86,7 +90,7 @@ jobs:
- name: Copy documentation to `docs/docs`
run: |
sudo chown -R runner docs
cp -r .lake/build/doc docs/docs # Copy the built documentation to the correct directory
cp -r .lake/build/doc docs/docs
- name: Bundle dependencies
uses: ruby/setup-ruby@v1
Expand All @@ -97,7 +101,7 @@ jobs:

- name: Bundle website
working-directory: docs
run: JEKYLL_ENV=production bundle exec jekyll build # Build the Jekyll site for production
run: JEKYLL_ENV=production bundle exec jekyll build

- name: Upload docs & blueprint artifact
uses: actions/upload-pages-artifact@v1
Expand Down

0 comments on commit 9c78d44

Please sign in to comment.