Skip to content

Unbounded π-finite types #8343

Unbounded π-finite types

Unbounded π-finite types #8343

Workflow file for this run

name: agda-unimath CI
on:
# To run this workflow manually
workflow_dispatch:
inputs:
ref:
description: the repository ref to build
required: true
default: master
push:
branches:
- master
pull_request:
branches:
- master
types:
- opened
- reopened
- synchronize
- ready_for_review
# Cancel previous runs of the same branch
concurrency:
group: '${{ github.workflow }}-${{ github.head_ref || github.run_id }}'
cancel-in-progress: true
jobs:
typecheck:
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [macOS-13, ubuntu-latest]
agda: ['2.6.4']
steps:
- name: Checkout our repository
uses: actions/checkout@v3
with:
path: master
- name: Setup Agda
uses: wenkokke/setup-agda@v2.1.0
with:
agda-version: ${{ matrix.agda }}
- uses: actions/cache/restore@v3
id: cache-agda-formalization
name: Restore Agda formalization cache
with:
path: master/_build
key:
${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-${{
hashFiles('master/src/**') }}
restore-keys: |
${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-
${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}-
- name: Typecheck library
run: |
cd master
make check
- name: Save Agda build cache
uses: actions/cache/save@v3
with:
path: master/_build
key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}'
# Install Python and friends for website generation only where needed
- uses: actions/setup-python@v4
if: ${{ matrix.os == 'ubuntu-latest' }}
with:
python-version: '3.8'
check-latest: true
cache: 'pip'
- run: python3 -m pip install -r master/scripts/requirements.txt
if: ${{ matrix.os == 'ubuntu-latest' }}
# We need to run the sources through Agda not only to get the highlighting
# (which is irrelevant for checking links), but because it flattens the
# directory structure to a format which is expected in the links we write.
# We don't need to produce this artifact for more than one configuration.
- name: Produce syntax highlighted markdown
if: ${{ matrix.os == 'ubuntu-latest' }}
run: |
cd master
make website-prepare
# The lifetime of this cache is for one CI run only, so it's indexed by
# the run ID. According to the docs, caches are immutable, so we can't
# keep the same key for a branch and update it on pushes.
- name: Save pre-website cache
if: ${{ matrix.os == 'ubuntu-latest' }}
uses: actions/cache/save@v3
with:
key: pre-website-${{ github.run_id }}
path: master/docs
# We're only running the linkcheck renderer, so we don't need to install
# any other packages; that gives a warning during building, but doesn't
# fail the build.
link-check:
needs: typecheck
permissions:
actions: write
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
with:
path: master
- uses: peaceiris/actions-mdbook@v1
with:
mdbook-version: '0.4.34'
- uses: baptiste0928/cargo-install@v2
with:
crate: mdbook-linkcheck
version: '0.7.7'
# Install Python and friends for website generation only where needed
- uses: actions/setup-python@v4
with:
python-version: '3.8'
check-latest: true
cache: 'pip'
- run: python3 -m pip install -r master/scripts/requirements.txt
- uses: actions/cache/restore@v3
with:
key: pre-website-${{ github.run_id }}
path: master/docs
# Tell mdbook to use only the linkcheck backend
- name: Check website links and bibtex references
env:
MDBOOK_OUTPUT: '{"linkcheck":{}}'
run: |
cd master
mdbook build
- name: Delete website cache
if: ${{ always() }}
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
# Note that the cleanup currently fails, because we don't give the
# `actions:write` permission to actions; hence the `set +e` to ignore
# the error
run: |
gh extension install actions/gh-actions-cache
REPO=${{ github.repository }}
BRANCH="refs/pull/${{ github.event.pull_request.number }}/merge"
set +e
gh actions-cache delete pre-website-${{ github.run_id }} -R $REPO -B $BRANCH --confirm
# The previous command failing would report an error even with `set -e`
exit 0
pre-commit:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- uses: actions/setup-python@v4
with:
python-version: '3.8'
check-latest: true
cache: 'pip'
- run: python3 -m pip install -r scripts/requirements.txt
- uses: pre-commit/action@v3.0.0