Makefile.common

ZETA_HOME ?= .
FSTAR_HOME ?= $(realpath $(dir $(shell which fstar.exe))/..)
KRML_HOME ?= $(FSTAR_HOME)/../karamel
STEEL_HOME ?= $(FSTAR_HOME)/../steel

# FSTAR_HOME ?= everest/FStar
# KRML_HOME ?= everest/karamel

# List the files that should be verified by verify-extra and verify-all
EXTRA=

# List the files that should NOT be verified at all
FLAKY=

# List additional directories for the include path
SRC_DIRS ?=

# List the files that should be verified by verify-core and verify-all
# Those files are the roots from where all dependencies are computed
FSTAR_FILES ?=

OTHERFLAGS+=$(PROFILE)

# Backward compatibility with pre typed indexed effects (see F* PR 2760)
# and F* PR 3253
OTHERFLAGS+=--compat_pre_typed_indexed_effects --ext 'compat:injectivity'

# 271: theory symbols in smt patters
WARN_ERROR=--warn_error -271
SMT_OPTIONS=--z3cliopt 'timeout=600000' --z3cliopt 'smt.arith.nl=false' \
            --smtencoding.elim_box true \
            --smtencoding.l_arith_repr native \
            --smtencoding.nl_arith_repr wrapped
OTHERFLAGS+=$(WARN_ERROR) $(SMT_OPTIONS)
ALREADY_CACHED_LIST ?= Prims,FStar,LowStar,Steel
ALREADY_CACHED = --already_cached $(ALREADY_CACHED_LIST)

# A place to put all the emitted .ml files
OUTPUT_DIRECTORY ?= $(ZETA_HOME)/_output
CACHE_DIRECTORY = $(OUTPUT_DIRECTORY)/cache
DIST_DIRECTORY=$(ZETA_HOME)/steel/dist

INCLUDE_PATHS+=$(OUTPUT_DIRECTORY) $(SRC_DIRS) $(KRML_HOME)/krmllib $(KRML_HOME)/krmllib/obj $(STEEL_HOME)/lib/steel

LOAD_PLUGIN ?= --load_cmxs steel
FSTAR_OPTIONS=--odir $(OUTPUT_DIRECTORY) \
		 $(OTHERFLAGS) \
		 --cache_dir $(CACHE_DIRECTORY) \
	         $(addprefix --include , $(INCLUDE_PATHS)) \
		 --cache_checked_modules \
		 --cmi \
                 $(LOAD_PLUGIN)

FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(FSTAR_OPTIONS) $(ALREADY_CACHED)

.depend: $(FSTAR_FILES)
	mkdir -p $(CACHE_DIRECTORY)
	$(FSTAR) $(FSTAR_DEP_OPTIONS) --dep full $(notdir $(FSTAR_FILES)) > .depend.aux
	mv .depend.aux .depend

depend: .depend

include .depend


# a.fst(i).checked is the binary, checked version of a.fst(i)
$(CACHE_DIRECTORY)/%.checked:
	$(FSTAR) $<
	touch -c $@

%.krml:
	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
	  --extract_module $(basename $(notdir $(subst .checked,,$<)))
	touch -c $@

verify: $(ALL_CHECKED_FILES)

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

.PHONY: verify clean depend all world