From 455ba366f9c8d07a1f1848ec0960b1f2d161e7cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 18:47:50 +0100
Subject: Update the library for F*

---
 backends/fstar/merge/Makefile | 47 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 backends/fstar/merge/Makefile

(limited to 'backends/fstar/merge/Makefile')

diff --git a/backends/fstar/merge/Makefile b/backends/fstar/merge/Makefile
new file mode 100644
index 00000000..a16b0edb
--- /dev/null
+++ b/backends/fstar/merge/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/*
-- 
cgit v1.2.3