# This Makefile can be safely included from sub-directories for the purposes of
# defining the .fst-in targets, as long as the sub-directory defines HACL_HOME.

HACL_HOME 	?= .
KREMLIN_HOME 	?= $(HACL_HOME)/../kremlin
FSTAR_HOME	?= $(HACL_HOME)/../FStar
VALE_HOME	?= $(HACL_HOME)/../vale

include $(HACL_HOME)/Makefile.include

INCLUDES = \
  $(ALL_HACL_DIRS) \
  $(KREMLIN_HOME)/kremlib

# 1. FStar

OUTPUT_DIR = obj

FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDES))

# 272: top-level bindings must be total
# 247: checked file not written because some of its dependencies...
# 241: corrupt cache file AND stale cache file (argh!) we wish to make the
#      former fatal, and the latter non-fatal if it's the file we're about to
#      verify... see https://github.com/FStarLang/FStar/issues/1652
FSTAR_NO_FLAGS = $(FSTAR_HOME)/bin/fstar.exe --use_hints --record_hints --use_hint_hashes \
  --odir $(OUTPUT_DIR) --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
  --already_cached 'Prims FStar LowStar C Spec.Loops TestLib' --warn_error '+241@247-272' \
  --cache_dir obj

FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS)

%.fst-in %.fsti-in:
	@echo $(FSTAR_INCLUDES)

# 2. Kremlin

KRML = $(KREMLIN_HOME)/krml