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

fix: handle lakefile.toml #224

	name: CI

	on:
	push:
	branches: [ main ]
	pull_request:
	branches: [ main ]

	workflow_dispatch:

	jobs:
	build:
	name: ${{ matrix.name }}
	runs-on: ${{ matrix.os }}
	defaults:
	run:
	shell: ${{ matrix.shell \|\| 'sh' }}
	strategy:
	fail-fast: false
	matrix:
	include:
	- name: Ubuntu
	os: ubuntu-latest
	- name: macOS
	os: macos-latest
	- name: Windows
	os: windows-latest
	shell: pwsh
	steps:
	# Fix CR/LF mangling on Windows
	- name: Disable autocrlf in git
	run: git config --global core.autocrlf false

	# Checkout repository
	- uses: actions/checkout@v2

	# Install elan with nightly toolchain
	- name: Install Elan (macOS)
	if: matrix.os == 'macos-latest'
	run: \|
	set -o pipefail
	curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \| sh -s -- --default-toolchain none -y
	echo "$HOME/.elan/bin" >> $GITHUB_PATH

	- name: Install Elan (Ubuntu)
	if: matrix.os == 'ubuntu-latest'
	run: \|
	curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \| sh -s -- --default-toolchain none -y
	echo "$HOME/.elan/bin" >> $GITHUB_PATH

	- name: Install Elan (Windows)
	if: matrix.os == 'windows-latest'
	run: \|
	curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
	.\elan-init.ps1 -NoPrompt 1 -DefaultToolchain none
	echo "$HOME\.elan\bin" >> $env:GITHUB_PATH

	# Build and test
	- name: Build LeanInk
	run: lake build

	# Upload artifact
	- name: Upload artifacts
	uses: actions/upload-artifact@v2
	with:
	name: ${{ matrix.os }}
	path: build

	- name: Run tests
	run: lake script run tests

Provide feedback