Skip to content

chore: bump (v4.14.0-rc2) #526

chore: bump (v4.14.0-rc2)

chore: bump (v4.14.0-rc2) #526

Workflow file for this run

on:
pull_request:
jobs:
style_lint:
name: Lint style
runs-on: ubuntu-latest
steps:
- name: Don't 'import Mathlib', use precise imports
if: always()
run: |
! (find Carleson -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
build_project:
runs-on: ubuntu-latest
name: Build project
steps:
- name: Checkout project
uses: actions/checkout@v4
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
- name: Get cache
run: ~/.elan/bin/lake exe cache get || true
- name: Build project
run: ~/.elan/bin/lake build Carleson
- name: Build blueprint and copy to `docs/blueprint`
uses: xu-cheng/texlive-action@v2
with:
docker_image: ghcr.io/xu-cheng/texlive-full:20231201
run: |
export PIP_BREAK_SYSTEM_PACKAGES=1
apk update
apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
git config --global --add safe.directory $GITHUB_WORKSPACE
git config --global --add safe.directory `pwd`
python3 -m venv env
source env/bin/activate
pip install --upgrade pip requests wheel
pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
pip install leanblueprint
leanblueprint pdf
leanblueprint web
- name: Check declarations
run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls