PYTHON ?= python3

.PHONY: check python lean lean-replay pdf integrity
check: python lean

python:
	PYTHONDONTWRITEBYTECODE=1 $(PYTHON) companion/tests/run_reference_tests.py --output companion/results/reproduced_reference_tests.json
	PYTHONDONTWRITEBYTECODE=1 $(PYTHON) companion/tests/run_graph_tests.py --output companion/results/reproduced_graph_tests.json
	PYTHONDONTWRITEBYTECODE=1 $(PYTHON) companion/tests/run_revision_tests.py --output companion/results/reproduced_revision_tests.json
	PYTHONDONTWRITEBYTECODE=1 $(PYTHON) companion/tests/run_upgrade_tests.py --output companion/results/reproduced_upgrade_tests.json
	PYTHONDONTWRITEBYTECODE=1 $(PYTHON) companion/tests/run_review_tests.py --output companion/results/reproduced_review_tests.json

lean:
	cd lean && lake build
	cd lean && lake env lean -DautoImplicit=false -DwarningAsError=true PublicationScope.lean

# Recheck stored proofs and their imports using Lean's own kernel.
# This is not an independent kernel implementation.
lean-replay: lean
	cd lean && lake env leanchecker --fresh -v Erdos278

pdf:
	tectonic --outdir output/pdf output/latex/erdos-278-publication-v1.tex

integrity:
	$(PYTHON) verify_manifest.py
