Modernize SpecSync: TypeScript, CI, docs #1

	name: Lean4 specs

	on:
	pull_request:
	paths:
	- "specs/**"
	- "lakefile.lean"
	- "lean-toolchain"
	- ".github/workflows/lean4-ci.yml"
	push:
	branches: [main, master]
	paths:
	- "specs/**"
	- "lakefile.lean"
	- "lean-toolchain"

	jobs:
	lean4-specs:
	runs-on: ubuntu-latest
	permissions:
	contents: read
	pull-requests: write

	steps:
	- name: Checkout
	uses: actions/checkout@v4

	- name: Build specs (lake via lean-action)
	uses: leanprover/lean-action@v1
	with:
	auto-config: "true"
	test: "false"

	- name: Comment on PR with build summary
	if: github.event_name == 'pull_request' && success()
	uses: actions/github-script@v7
	with:
	script: \|
	const body = [
	'## Lean4 build',
	'',
	'`lake build` completed successfully for this change.',
	'',
	`Workflow: ${context.workflow} run [\`${context.runId}\`](${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId})`
	].join('\n');
	const { data: comments } = await github.rest.issues.listComments({
	owner: context.repo.owner,
	repo: context.repo.repo,
	issue_number: context.issue.number
	});
	const marker = '<!-- specsync-lean4-ci -->';
	const existing = comments.find(c => c.body && c.body.includes(marker));
	const fullBody = marker + '\n' + body;
	if (existing) {
	await github.rest.issues.updateComment({
	owner: context.repo.owner,
	repo: context.repo.repo,
	comment_id: existing.id,
	body: fullBody
	});
	} else {
	await github.rest.issues.createComment({
	owner: context.repo.owner,
	repo: context.repo.repo,
	issue_number: context.issue.number,
	body: fullBody
	});
	}

Navigation Menu