squash #6

	name: Functional Tests

	on: [push, workflow_dispatch]

	jobs:
	no-lake-test:
	runs-on: ubuntu-latest
	strategy:
	matrix:
	# run with and without `lake test'
	lake-test: ["true", "false"]
	# run for standalone package and one which depends on mathlib
	lake-init-command: ["init standalone", "init mathdep math"]
	steps:
	# TODO: once `lean-action` supports just setup use it here
	- 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 leanprover/lean4:v4.8.0-rc1
	echo "$HOME/.elan/bin" >> $GITHUB_PATH


	- uses: actions/checkout@v4

	- name: create standalone project
	run: \|
	lake ${{ matrix.lake-init-command }}
	ls

	- name: create dummy test
	if: ${{ matrix.lake-test == 'true' }}
	run: \|
	echo "@[test_runner]" >> lakefile.lean
	echo "script dummy_test do" >> lakefile.lean
	echo " println! \"Running fake tests...\"" >> lakefile.lean
	echo " println! \"Fake tests passed!\"" >> lakefile.lean
	echo " return 0" >> lakefile.lean

	- name: ls and pwd
	run: \|
	ls
	pwd

	- name: "run `lean-action` with on `lake ${{matrix.lake-init-command}}` with test: ${{ matrix.lake-test }}"
	uses: ./
	with:
	test: ${{ matrix.lake-test }}

Provide feedback