diff options
author | Son Ho | 2022-11-11 21:34:29 +0100 |
---|---|---|
committer | Son HO | 2022-11-14 14:21:04 +0100 |
commit | 6db835db88c4bcf0e00ce1a7a6bc396382b393c3 (patch) | |
tree | 3b2a9d46467cf313e3af641cd164e61af2a09541 /tests/fstar/hashmap_on_disk/Makefile | |
parent | b191070501ceafdd49c999385c4410848249fe18 (diff) |
Reorganize the project to prepare for new backends
Diffstat (limited to 'tests/fstar/hashmap_on_disk/Makefile')
-rw-r--r-- | tests/fstar/hashmap_on_disk/Makefile | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile new file mode 100644 index 00000000..a16b0edb --- /dev/null +++ b/tests/fstar/hashmap_on_disk/Makefile @@ -0,0 +1,47 @@ +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_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/* |