toolchain #24

	on:
	push:
	branches-ignore:
	# ignore tmp branches used by bors
	- 'staging.tmp*'
	- 'trying.tmp*'
	- 'staging*.tmp'
	pull_request:

	name: ci

	jobs:
	build:
	name: Build
	runs-on: ubuntu-latest
	steps:
	- name: install elan
	run: \|
	set -o pipefail
	curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz \| tar xz
	./elan-init -y --default-toolchain none
	echo "$HOME/.elan/bin" >> $GITHUB_PATH

	- uses: actions/checkout@v2

	- name: update Std.lean
	run: \|
	find Std -name "*.lean" \| LC_ALL=C sort \| sed 's/\.lean//;s,/,.,g;s/^/import /' > Std.lean

	- name: build std
	run: lake build

	- name: test std
	run: make test

	- name: lint std
	run: make lint

	- name: check that all files are imported
	run: git diff --exit-code

	- name: Check for forbidden character ↦
	run: \|
	if grep -r -n --include=\*.lean -e '↦' . ; then
	echo "Error: Found forbidden character ↦"
	exit 1
	fi

	- name: Check for long lines
	run: \|
	! (find . -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; \| grep -v -E 'https?://')

Provide feedback