This repository has been archived by the owner on Aug 29, 2024. It is now read-only.

feat: finish PHPDemo proof #15

	on:
	push:
	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: build
	id: build
	run: lake build -Kwerror

	- name: test
	if: steps.build.outcome == 'success'
	run: make test

	# No point linting until we write some doc-strings.
	# - name: lint
	# if: steps.build.outcome == 'success'
	# run: make lint

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

	- name: Don't 'import Lean', use precise imports
	if: always()
	run: \|
	! (find . -name "*.lean" -type f -print0 \| xargs -0 grep -E -n '^import Lean$')

Provide feedback