# A shared set of local definitions for local Makefiles. See curve25519/Makefile
# for comments.
HACL_HOME ?= .
OUTPUT_DIR=$(HACL_HOME)/obj
# This uses the definition of ALL_HACL_DIRS, and transitively includes
# Makefile.include
include $(HACL_HOME)/Makefile.common
# All the files in the current directory ought to be verified.
FSTAR_ROOTS?=$(wildcard *.fst *.fsti)
# This is the right way to ensure the .depend file always gets re-built.
ifndef NODEPEND
ifndef MAKE_RESTARTS
.depend: .FORCE
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
--extract '-* +FStar.Kremlin.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector -Lib.RandomBuffer.Hardware +C' \
> $@
.PHONY: .FORCE
.FORCE:
endif
endif
include .depend
%.checked: FSTAR_FLAGS=
$(OUTPUT_DIR)/Vale.%.checked: FSTAR_FLAGS=$(VALE_FSTAR_FLAGS)
# Producing .checked and .krml.
%.checked:
$(FSTAR) $(FSTAR_FLAGS) $< --hint_file $(HACL_HOME)/hints/$(notdir $*).hints && \
touch -c $@
%.krml:
$(FSTAR) --codegen Kremlin \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
$(notdir $(subst .checked,,$<))
CODEGEN=OCaml
%.ml:
$(FSTAR) --codegen $(CODEGEN) \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
$(notdir $(subst .checked,,$<))
%.cmx: %.ml
$(OCAMLOPT) -c $< -o $@
# Useful definitions for C compilation
CFLAGS += -Idist -I$(KREMLIN_HOME)/include -I$(KREMLIN_HOME)/kremlib/dist/minimal
%.exe:
$(CC) $^ -o $@
# Tactic; sadly not shareable because obj vs. $(HACL_HOME)/obj
$(HACL_HOME)/obj/Meta_Interface.ml: CODEGEN = Plugin
$(HACL_HOME)/obj/Meta_Interface.ml: $(HACL_HOME)/obj/Meta.Interface.fst.checked
$(HACL_HOME)/obj/Hacl.Meta.%.checked: FSTAR_FLAGS += --load Meta.Interface
ifneq (,$(wildcard Hacl.Meta.*.fst))
$(patsubst %,$(HACL_HOME)/obj/%.checked,$(wildcard Hacl.Meta.*.fst)): $(HACL_HOME)/obj/Meta_Interface.ml
endif