export CLOUD_VERIFY:=true
HACL_HOME:=$(abspath $(dir $(lastword $(MAKEFILE_LIST)))/..)
include $(HACL_HOME)/Makefile.include

Z3?=$(shell which z3)
ifeq ($(strip $(Z3)),)
  $(error No z3 found in $$PATH or $$Z3)
endif

ifdef BATCH_ID_FILE
  export BATCH_ID_FILE:=$(abspath $(HACL_HOME)/$(BATCH_ID_FILE))
else
  export BATCH_ID_FILE:=$(HACL_HOME)/batch_id.tmp
endif

BATCH_DATA_DIR?=$(HACL_HOME)/batch_results

BATCH_CONTENT:=$(Z3) \
	"$(FSTAR_HOME)|*.exe,*.fst,*.fsti,Makefile,Makefile.include,*.mk" \
	"$(HACL_HOME)|*.fst,*.fsti,Makefile,Makefile.include" \
	"$(KREMLIN_HOME)|*.fst,*.fsti"

ifdef HINTS_ENABLED
  BATCH_CONTENT+="$(FSTAR_HOME)|*.hints" "$(HACL_HOME)|*.hints" "$(KREMLIN_HOME)|*.hints"
endif

all: cloud-verify

$(BATCH_ID_FILE):
	$(info Creating new Batch job ...)
	$(EABC) create -n "HaCl*" $(addprefix -i ,$(BATCH_CONTENT)) > $@

cloud-awwait:
	$(EABC) await -j $(BATCH_JOB_ID) -t $(BATCH_DATA_DIR) -s

cloud-verify: $(BATCH_ID_FILE)
	$(MAKE) -C $(HACL_HOME) verify
	# $(EABC) await -j $(BATCH_JOB_ID) -t $(BATCH_DATA_DIR) -s
	rm $(BATCH_ID_FILE)