Skip to content

push away the sorry #334

push away the sorry

push away the sorry #334

Workflow file for this run

on:
push:
pull_request:
jobs:
update_lean_xyz_branch_and_build:
runs-on: ubuntu-latest
name: Build project
steps:
- name: checkout project
uses: actions/checkout@v3
with:
fetch-depth: 0
- name: update branch
if: github.ref == 'refs/heads/master'
uses: leanprover-contrib/update-versions-action@master
- name: Install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: install Python
uses: actions/setup-python@v1
with:
python-version: 3.8
- name: Install leanproject
run: |
python3 -m pip install --user pipx
python3 -m pipx ensurepath
source ~/.profile
pipx install mathlibtools
- name: Set up olean cache
uses: actions/cache@v3
with:
path: _cache
key: oleans
- name: Configure
run: |
leanpkg configure
leanproject get-mathlib-cache
leanproject get-cache --fallback=download-first || true
- name: Build
run: |
set -o pipefail
# TODO: allow noisy files in a better way
lean --json --make src | (python3 _target/deps/mathlib/scripts/detect_errors.py || true)
- name: Save olean cache
run: |
leanproject mk-cache
- name: Export symbols
run: |
leanproject mk-all
lean --run export.lean > lean-decl-info.tex
- uses: actions/upload-artifact@v3
with:
name: lean-decl-info
path: lean-decl-info.tex