Makefile.config

SKIP_BEDROCK2?=

VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)

BINDIR?=/usr/local/bin
# or $(shell opam config var bin) ?

MOD_NAME := Crypto
SRC_DIR  := src

INSTALLDEFAULTROOT := Crypto

PERF_RECORD?=perf record -g -o "$@.perf.data" --

WITH_PERF?=

RED:=\033[0;31m
# No Color
NC:=\033[0m
GREEN:=\033[0;32m
BOLD:=$(shell tput bold)
NORMAL:=$(shell tput sgr0)

# Time the Coq process (set to non empty), and how (see default value)
TIMED?=
TIMECMD?=
# Use command time on linux, gtime on Mac OS
TIMEFMT?="$(if $(findstring undefined, $(flavor 1)),$@,$(1)) (real: %e, user: %U, sys: %S, mem: %M ko)"
ifneq (,$(TIMED))
ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?))
STDTIME?=command time -f $(TIMEFMT)
else
ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?))
STDTIME?=gtime -f $(TIMEFMT)
else
STDTIME?=command time
endif
endif
else
STDTIME?=command time -f $(TIMEFMT)
endif

TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))

ifneq ($(SKIP_BEDROCK2),1)
if_SKIP_BEDROCK2 = $(2)
else
if_SKIP_BEDROCK2 = $(1)
endif

BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction
BEDROCK2_STANDALONE := $(addprefix bedrock2_,$(BASE_STANDALONE)) $(addprefix with_bedrock2_,$(BASE_STANDALONE))
STANDALONE := $(BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_STANDALONE) $(WITH_BEDROCK2_STANDALONE))
PERF_STANDALONE := perf_unsaturated_solinas perf_word_by_word_montgomery

STANDALONE_OCAML := $(STANDALONE) $(PERF_STANDALONE)
STANDALONE_HASKELL := $(STANDALONE)

OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/%)
HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/%)

WITH_BEDROCK2_OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%)
WITH_BEDROCK2_HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%)