icarus/Makefile at main · mcaney006/icarus · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
SHELL := /bin/bash
.SHELLFLAGS := -o pipefail -c
DETECT := bash tools/detect-toolchains.sh
PY := $(or $(shell $(DETECT) --path python3),python3)

define with_tool
@tool=$$($(DETECT) --path $(1)); \
if [ -z "$$tool" ]; then echo "[$(2)] SKIP ($(1) missing)"; else $(3); fi
endef

.PHONY: toolchains fixtures bootstrap reference lean idris fstar ats build verify audit negative simulate \
        selftest crosscheck satcheck experiments benchmark test format ci clean

toolchains:
	@$(DETECT)

fixtures:
	@$(PY) tools/gen_fixtures.py

bootstrap: toolchains fixtures

reference:
	@$(PY) reference/icarus_ref.py --selfcheck

lean:
	$(call with_tool,lake,lean,cd lean && "$$tool" build)

idris:
	$(call with_tool,idris2,idris,cd idris && "$$tool" --build icarus.ipkg)

fstar:
	$(call with_tool,fstar,fstar,$(MAKE) -C fstar FSTAR="$$tool")

ats:
	$(call with_tool,patscc,ats,$(MAKE) -C ats PATSCC="$$tool")

build: reference lean idris fstar ats

verify: lean fstar idris negative audit

audit:
	@bash tools/audit-holes.sh

negative:
	@bash negative/run.sh

simulate:
	$(call with_tool,patscc,ats,$(MAKE) -C ats simulate PATSCC="$$tool")

selftest:
	@if [ -x idris/build/exec/icarus ]; then idris/build/exec/icarus --selftest | tail -1; else echo "[idris] SKIP selftest (not built)"; fi
	@if [ -x ats/build/icarus_selftest ]; then ats/build/icarus_selftest | tail -1; else echo "[ats] SKIP selftest (not built)"; fi

crosscheck:
	@$(PY) tools/crosscheck.py $(STRICT)

satcheck:
	@$(PY) tools/satcheck.py $(STRICT)

experiments:
	@$(PY) tools/fixed_point_experiment.py

benchmark:
	@$(PY) tools/benchmark.py

test: reference selftest crosscheck satcheck

format:
	@git diff --check $$(git hash-object -t tree /dev/null) HEAD
	$(call with_tool,ruff,python,"$$tool" format --check --quiet reference tools && "$$tool" check --quiet reference tools)
	@echo "format: clean"

ci:
	@$(DETECT) --require-all
	@$(MAKE) format bootstrap
	@git diff --exit-code --stat fixtures/
	@$(MAKE) build verify test simulate STRICT=--strict

clean:
	@rm -rf dist lean/.lake idris/build fstar/out ats/build
	@find . \( -name '*.checked' -o -name '*_dats.c' -o -name '*_sats.c' \) -not -path './.git/*' -delete