docs: candid paper-viability review (referee-strength self-assessment) #87

	name: verify
	# Type-checks the seed Rocq statement only. No LLM calls, no secrets.
	on:
	push:
	pull_request:

	jobs:
	rocq-seed:
	runs-on: ubuntu-latest
	# checkout runs on the host; docker-coq-action mounts the workspace and runs
	# coqc inside the coq container with the opam env loaded (avoids the
	# non-root EACCES issue of running checkout inside coqorg/coq directly).
	steps:
	- uses: actions/checkout@v4
	- uses: coq-community/docker-coq-action@v1
	with:
	coq_version: "8.18"
	custom_script: \|
	ws="$PWD"
	startGroup "coqc every rocq target"
	# Compile each in its own writable temp dir: the mounted workspace
	# is host-owned (coqc runs as user `coq` and can't write .vo/.glob
	# next to the sources), and per-file dirs avoid name collisions.
	# Globbing picks up new units automatically.
	for v in work-units//targets/rocq/.v; do
	dd="$(mktemp -d)"; cp "$v" "$dd/"
	( cd "$dd" && coqc -q "$(basename "$v")" )
	done
	endGroup
	startGroup "coqc the framework library"
	for v in framework/*.v; do
	dd="$(mktemp -d)"; cp "$v" "$dd/"
	( cd "$dd" && coqc -q "$(basename "$v")" )
	done
	endGroup
	startGroup "certify the decomposed (leaf) proofs"
	# each assemble.sh resolves its own dir and compiles in a temp dir.
	for a in "$ws"/work-units/*/decomposition/assemble.sh; do
	bash "$a"
	done
	endGroup

	coordinator-typecheck:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	- uses: actions/setup-node@v4
	with:
	node-version: "20"
	- working-directory: coordinator
	run: \|
	npm install
	npm run typecheck

Provide feedback