Test with Lean nightly #18

	name: Test with Lean nightly

	on:
	workflow_dispatch:
	schedule:
	- cron: '0 0 * * *' # Run every day at midnight

	jobs:
	nightly-test:
	runs-on: ubuntu-latest

	steps:
	- name: Install elan
	run: \|
	set -o pipefail
	curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \| sh -s -- -y --default-toolchain none
	echo "$HOME/.elan/bin" >> $GITHUB_PATH

	- name: Check out code
	uses: actions/checkout@v4

	- name: Get latest release tag from leanprover/lean4-nightly
	id: get-latest-release
	run: \|
	RELEASE_TAG="$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" \| jq -r '.[0].tag_name')"
	echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}"

	- name: Select Lean version ${{env.RELEASE_TAG}}
	run: \|
	echo "leanprover/lean4:${RELEASE_TAG}" > lean-toolchain

	- name: Build the project
	continue-on-error: true
	id: build
	run: \|
	lake build

	- name: Configure demo/test subproject
	if: always() && steps.build.outcome == 'success'
	continue-on-error: true
	id: config-test
	run: \|
	pushd demo
	lake update
	lake build :examples
	popd

	- name: Run tests
	if: always() && steps.config-test.outcome == 'success'
	continue-on-error: true
	id: test
	run: \|
	lake exe subverso-tests

	- name: Create/update issue on failure
	if: always() && (steps.build.outcome == 'failure') \|\| (steps.config-test.outcome == 'failure') \|\| (steps.test.outcome == 'failure')
	uses: JasonEtco/create-an-issue@v2
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	with:
	update_existing: true
	search_existing: open
	filename: .github/NIGHTLY_FAILURE.md

Provide feedback