32 lines
1.0 KiB
Makefile
32 lines
1.0 KiB
Makefile
ISABELLE ?= isabelle
|
|
|
|
.PHONY: all check measure payload guest clean
|
|
|
|
all: .build/ready
|
|
|
|
.build/ready: ROOT $(wildcard src/*.thy src/core/*.thy) cli/driver.ML Makefile
|
|
@test "$$('$(ISABELLE)' version)" = Isabelle2026
|
|
"$(ISABELLE)" build -D . -j 1 -o threads=1 -o parallel_proofs=0
|
|
"$(ISABELLE)" export -n -d . -O .build -x 'Remy.Export:code/remy.ML' Remy
|
|
REMY_ROOT="$(CURDIR)" "$$('$(ISABELLE)' getenv -b POLYML_HOME)/$$('$(ISABELLE)' getenv -b ISABELLE_PLATFORM64)/polyc" -o .build/remy cli/driver.ML
|
|
@touch $@
|
|
|
|
check: all
|
|
python3 tests/native.py
|
|
python3 tests/cli.py
|
|
python3 tests/live.py
|
|
|
|
measure: all
|
|
python3 tests/measure.py
|
|
|
|
payload: all
|
|
@mkdir -p .build/payload
|
|
@set -e; for name in Rings Weave Cells; do .build/remy examples/$$name.remy .build/payload/$$name.BIN; .build/remy vectors examples/$$name.remy .build/payload/$$name.DAT; cp examples/$$name.remy .build/payload/$$name.TXT; done
|
|
cp guest/Remy.HC .build/payload/Remy.HC
|
|
|
|
guest: payload
|
|
python3 tests/guest.py "$(TEMPLE_ISO)"
|
|
|
|
clean:
|
|
rm -rf .build
|