summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
authorSon Ho2024-02-09 17:23:57 +0100
committerSon Ho2024-02-09 17:23:57 +0100
commitdd41ce4d968222824d36a295194a0de003d7a822 (patch)
treeab7c8d7dd3aa62e16e2cf84467da3d5fbb156711 /tests/fstar
parentc285a3ff4fa6e7f8de182e574a7eb6d164cbee46 (diff)
Remove a file which shouldn't have been added
Diffstat (limited to '')
-rw-r--r--tests/fstar-split/betree_back_stateful/Makefile49
1 files changed, 0 insertions, 49 deletions
diff --git a/tests/fstar-split/betree_back_stateful/Makefile b/tests/fstar-split/betree_back_stateful/Makefile
deleted file mode 100644
index fa7d1f36..00000000
--- a/tests/fstar-split/betree_back_stateful/Makefile
+++ /dev/null
@@ -1,49 +0,0 @@
-# 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/*