diff options
author | Son HO | 2024-02-03 00:23:30 +0100 |
---|---|---|
committer | GitHub | 2024-02-03 00:23:30 +0100 |
commit | eb8bddcbd120f666f74023de9a23c48e1a55833d (patch) | |
tree | 1d8290e4b947e431c3d8d3a9f8575f23c3afe5e1 /tests/fstar-split/arrays/Makefile | |
parent | 0960ad16838a43da3746f47cf5b640bfbb783d84 (diff) | |
parent | 9cc912e2414870df85ffc4dd346ade5dba2b5c37 (diff) |
Merge pull request #68 from AeneasVerif/son/update_lean
Update Lean to v4.6.0-rc1
Diffstat (limited to 'tests/fstar-split/arrays/Makefile')
-rw-r--r-- | tests/fstar-split/arrays/Makefile | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/tests/fstar-split/arrays/Makefile b/tests/fstar-split/arrays/Makefile new file mode 100644 index 00000000..fa7d1f36 --- /dev/null +++ b/tests/fstar-split/arrays/Makefile @@ -0,0 +1,49 @@ +# This file was automatically generated - modify ../Makefile.template instead +INCLUDE_DIRS = . + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints + +FSTAR_OPTIONS = $(FSTAR_HINTS) \ + --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --warn_error '+241@247+285-274' \ + +FSTAR_EXE ?= fstar.exe +FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj + +FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) + +# The F* roots are used to compute the dependency graph, and generate the .depend file +FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) + +# Build all the files +all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS))) + +# This is the right way to ensure the .depend file always gets re-built. +ifeq (,$(filter %-in,$(MAKECMDGOALS))) +ifndef NODEPEND +ifndef MAKE_RESTARTS +.depend: .FORCE + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend +endif + +# For the interactive mode +%.fst-in %.fsti-in: + @echo $(FSTAR_OPTIONS) + +# Generete the .checked files in batch mode +%.checked: + $(FSTAR) $(FSTAR_OPTIONS) $< && \ + touch -c $@ + +.PHONY: clean +clean: + rm -f obj/* |