diff options
| author | Son HO | 2024-03-08 16:51:40 +0100 |
|---|---|---|
| committer | GitHub | 2024-03-08 16:51:40 +0100 |
| commit | 169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (patch) | |
| tree | ed8953634d14313d5b7d6ad204343d64eb990baf /backends/fstar/split/Makefile | |
| parent | b604bb9935007a1f0e9c7f556f8196f0e14c85ce (diff) | |
| parent | 873deb005b394aca3090497e6c21ab9f8c2676be (diff) | |
Merge pull request #83 from AeneasVerif/son/backs
Remove the option to split the forward/backward functions
Diffstat (limited to 'backends/fstar/split/Makefile')
| -rw-r--r-- | backends/fstar/split/Makefile | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/backends/fstar/split/Makefile b/backends/fstar/split/Makefile deleted file mode 100644 index a16b0edb..00000000 --- a/backends/fstar/split/Makefile +++ /dev/null @@ -1,47 +0,0 @@ -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/* |