Skip to content

indentation

indentation #24

Workflow file for this run

on:
push:
branches:
- master
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
contents: read
pages: write
id-token: write
jobs:
style_lint:
name: Lint style
runs-on: ubuntu-latest
steps:
- name: Check for long lines
if: always()
run: |
! (find LeanCondensed -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
- name: Don't 'import Mathlib', use precise imports
if: always()
run: |
! (find LeanCondensed -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@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 none
- name: Get cache
run: ~/.elan/bin/lake exe cache get || true
- name: Build project
run: ~/.elan/bin/lake build LeanCondensed
# - name: Cache mathlib docs
# uses: actions/cache@v3
# with:
# path: |
# .lake/build/doc/Init
# .lake/build/doc/Lake
# .lake/build/doc/Lean
# .lake/build/doc/Std
# .lake/build/doc/Mathlib
# .lake/build/doc/declarations
# !.lake/build/doc/declarations/declaration-data-LeanCondensed*
# key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
# restore-keys: |
# MathlibDoc-