Fix issues #10 and #11 and the remaining deferred items #18

	name: CI

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

	jobs:
	build-and-verify:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4

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

	- name: Cache .lake
	uses: actions/cache@v4
	with:
	path: .lake
	key: lake-${{ hashFiles('lean-toolchain', 'lakefile.lean', 'lake-manifest.json') }}

	- name: Build
	run: lake build

	# The `nng` course's solutions form a Lean library, so they are already
	# compiled (and thus verified) by `lake build` above. Here we check the
	# standalone `intro` solutions, compiled file-by-file together with each
	# exercise's hidden correctness checks (courses/intro/tests/), so the
	# reference answers are verified to actually satisfy the `#guard`s.
	- name: Verify intro solutions
	run: \|
	failed=0
	for f in $(find courses/intro/solutions -path '/.lean' \| sort); do
	rel=${f#courses/intro/solutions/}
	test="courses/intro/tests/$rel"
	tmp=$(mktemp /tmp/leanlings-XXXXXX.lean)
	cat "$f" > "$tmp"
	if [ -f "$test" ]; then printf '\n\n' >> "$tmp"; cat "$test" >> "$tmp"; fi
	if ! lean "$tmp" 2>&1; then
	echo "FAIL: $f"
	failed=$((failed + 1))
	fi
	rm -f "$tmp"
	done
	if [ $failed -gt 0 ]; then
	echo "$failed solution(s) failed"
	exit 1
	fi
	echo "All intro solutions verified against their checks"

Navigation Menu