Skip to content

Delete website main page #411

Delete website main page

Delete website main page #411

Workflow file for this run

name: Compile blueprint
on:
push:
branches:
- main # Trigger on pushes to the default branch
pull_request:
branches:
- main
workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface
# Cancel previous runs if a new commit is pushed to the same PR or branch
concurrency:
group: ${{ github.ref }} # Group runs by the ref (branch or PR)
cancel-in-progress: true # Cancel any ongoing runs in the same group
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
contents: read # Read access to repository contents
pages: write # Write access to GitHub Pages
id-token: write # Write access to ID tokens
issues: write # Write access to issues
pull-requests: write # Write access to pull requests
actions: write # Write access to GitHub Actions
jobs:
build_project:
runs-on: ubuntu-latest
name: Build project
steps:
- name: Cleanup to free disk space
uses: jlumbroso/free-disk-space@main
with:
tool-cache: false
android: true # saves approximately 12 GB
dotnet: false
haskell: false
large-packages: false
docker-images: false
swap-storage: false
- name: Checkout project
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
with:
fetch-depth: 0 # Fetch all history for all branches and tags
- name: Build and lint project
uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
with:
build: true
lint: false
mk_all-check: false
- name: Build Verso Documentation
run: |
./build_all.sh
# - name: Compile blueprint and documentation
# uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26
# with:
# homepage: home_page
# blueprint: true
# build-page: false
# deploy: false
- name: "Upload website (API documentation, blueprint and any home page)"
if: github.event_name == 'push'
uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3.0.1
with:
path: home_page/
- name: Deploy to GitHub Pages
if: github.event_name == 'push'
id: deployment
uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4.0.5