forked from mit-plv/fiat-crypto
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Makefile.config
105 lines (89 loc) · 5.51 KB
/
Makefile.config
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
.SUFFIXES:
SKIP_BEDROCK2?=
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
BINDIR?=/usr/local/bin
JSWASM_BASEDIR?=fiat-html
JSDIR?=$(JSWASM_BASEDIR)
WASMDIR?=$(JSWASM_BASEDIR)/wasm
# or $(shell opam config var bin) ?
MOD_NAME := Crypto
SRC_DIR := src
INSTALLDEFAULTROOT := Crypto
PERF_RECORD?=perf record -g -o "[email protected]" --
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
UNIFIED_BASE_STANDALONE := fiat_crypto
SEPARATE_BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction
BASE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(UNIFIED_STANDALONE)
BEDROCK2_UNIFIED_STANDALONE := $(addprefix bedrock2_,$(UNIFIED_BASE_STANDALONE)) $(addprefix WithBedrock/,$(UNIFIED_BASE_STANDALONE))
BEDROCK2_SEPARATE_STANDALONE := $(addprefix bedrock2_,$(SEPARATE_BASE_STANDALONE)) $(addprefix WithBedrock/,$(SEPARATE_BASE_STANDALONE))
BEDROCK2_STANDALONE := $(BEDROCK2_UNIFIED_STANDALONE) $(BEDROCK2_SEPARATE_STANDALONE)
UNIFIED_STANDALONE := $(UNIFIED_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_UNIFIED_STANDALONE))
SEPARATE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_SEPARATE_STANDALONE))
STANDALONE := $(UNIFIED_STANDALONE) $(SEPARATE_STANDALONE)
PERF_STANDALONE := perf_unsaturated_solinas perf_word_by_word_montgomery
UNIFIED_STANDALONE_OCAML := $(UNIFIED_STANDALONE)
SEPARATE_STANDALONE_OCAML := $(SEPARATE_STANDALONE) $(PERF_STANDALONE)
STANDALONE_OCAML := $(UNIFIED_STANDALONE_OCAML) $(SEPARATE_STANDALONE_OCAML)
UNIFIED_STANDALONE_HASKELL := $(UNIFIED_STANDALONE)
SEPARATE_STANDALONE_HASKELL := $(SEPARATE_STANDALONE)
STANDALONE_HASKELL := $(UNIFIED_STANDALONE_HASKELL) $(SEPARATE_STANDALONE_HASKELL)
STANDALONE_JS_OF_OCAML := $(UNIFIED_STANDALONE)
BEDROCK2_STANDALONE_JS_OF_OCAML := $(BEDROCK2_UNIFIED_STANDALONE)
STANDALONE_WASM_OF_OCAML := $(UNIFIED_STANDALONE)
BEDROCK2_STANDALONE_WASM_OF_OCAML := $(BEDROCK2_UNIFIED_STANDALONE)
UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/%)
SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/%)
OCAML_BINARIES := $(UNIFIED_OCAML_BINARIES) $(SEPARATE_OCAML_BINARIES)
UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/%)
SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/%)
HASKELL_BINARIES := $(UNIFIED_HASKELL_BINARIES) $(SEPARATE_HASKELL_BINARIES)
JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.map)
WASM_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wat.gz)
WASM_OF_OCAML_BASEDIR := src/ExtractionJsOfOCaml/
WASM_OF_OCAML_EXTRA_FILES_WASM = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.assets/*.wasm)
WASM_OF_OCAML_EXTRA_FILES_WASM_MAP = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.wasm.map) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/%.assets/*.wasm.map)
WASM_OF_OCAML_EXTRA_FILES = $(WASM_OF_OCAML_EXTRA_FILES_WASM) $(WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)
WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%)
WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/WithBedrock/%)
WITH_BEDROCK2_OCAML_BINARIES := $(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES) $(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES)
WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/WithBedrock/%)
WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/WithBedrock/%)
WITH_BEDROCK2_HASKELL_BINARIES := $(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES) $(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES)
WITH_BEDROCK2_JS_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.map)
WITH_BEDROCK2_WASM_OF_OCAML_FILES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.js) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wat.gz)
WITH_BEDROCK2_WASM_OF_OCAML_BASEDIR := src/ExtractionJsOfOCaml/WithBedrock/
WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wasm) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.assets/*.wasm)
WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM_MAP = $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.wasm.map) $(UNIFIED_BASE_STANDALONE:%=src/ExtractionJsOfOCaml/WithBedrock/%.assets/*.wasm.map)
WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES = $(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM) $(WITH_BEDROCK2_WASM_OF_OCAML_EXTRA_FILES_WASM_MAP)