# 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 ?= .
# Put your local configuration (e.g. HACL_HOME, KREMLIN_HOME, etc.) in
# Makefile.config
-include $(HACL_HOME)/Makefile.config
KREMLIN_HOME ?= $(HACL_HOME)/../kremlin
FSTAR_HOME ?= $(HACL_HOME)/../FStar
VALE_HOME ?= $(HACL_HOME)/../vale
include $(HACL_HOME)/Makefile.include
INCLUDES = \
$(ALL_HACL_DIRS) \
$(FSTAR_HOME)/ulib/.cache \
$(KREMLIN_HOME)/kremlib
# 1. FStar
OUTPUT_DIR = obj
FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDES))
FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
# --trivial_pre_for_unannotated_effectful_fns false
# to not enforce trivial preconditions
# for top-level unannotated effectful functions
# 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 $(FSTAR_HINTS) \
--odir $(OUTPUT_DIR) --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
--already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247-272' \
--cache_dir obj --trivial_pre_for_unannotated_effectful_fns false
FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS)
%.fst-in %.fsti-in:
@echo $(FSTAR_INCLUDES)
# 2. Kremlin
KRML = $(KREMLIN_HOME)/krml