Revision 9101826bd08816a58ca06fb64701d6d41f173883 authored by Chris Hawblitzel on 10 May 2019, 20:34:05 UTC, committed by Chris Hawblitzel on 10 May 2019, 20:34:05 UTC
Makefile.common
# 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))
FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
# 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' --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
Computing file changes ...