Armada 606: GADTs + TypeFamilies (50+ theorems) #90

	name: CI

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

	jobs:
	build:
	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-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }}
	restore-keys: lake-${{ runner.os }}-

	- name: Build
	run: lake build

	- name: Check for sorry
	run: \|
	# Use lake's own environment to detect sorry axiom usage.
	# After a successful build, grep .ilean/.olean is complex,
	# so we do a text search that strips both line and block comments.
	#
	# Strategy: use Python to strip comments, then search for sorry.
	python3 - <<'PYEOF'
	import re, sys, pathlib

	sorry_re = re.compile(r'\bsorry\b')
	# Pattern to remove block comments (non-nested) and line comments
	comment_re = re.compile(r'/\-[\s\S]?\-/\|--[^\n]')

	found = False
	for p in sorted(pathlib.Path('Metatheory').rglob('*.lean')):
	try:
	src = p.read_text()
	except Exception:
	continue
	stripped = comment_re.sub('', src)
	for i, line in enumerate(stripped.splitlines(), 1):
	if sorry_re.search(line):
	print(f"{p}:{i}: {line.strip()}")
	found = True

	if found:
	print("\nERROR: sorry detected in source files!")
	sys.exit(1)
	else:
	print("No sorry found — all proofs complete.")
	PYEOF

Navigation Menu