-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMakefile
44 lines (36 loc) · 994 Bytes
/
Makefile
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
# Directories
OBJ_DIR = obj
BUILD_DIR = build
# Name
NAME = hello
# Files
FST_FILE = code/Impl.Hello.fst
KRML_OUTPUT = $(OBJ_DIR)/$(NAME).krml
C_OUTPUT = $(BUILD_DIR)/$(NAME).c
H_OUTPUT = $(BUILD_DIR)/$(NAME).h
EXE_OUTPUT = $(BUILD_DIR)/$(NAME)
# Default target
all: $(C_OUTPUT) $(H_OUTPUT)
# Generate the .krml file from F* code
$(KRML_OUTPUT): $(FST_FILE)
mkdir --parent $(OBJ_DIR)
install -m 664 $(KRML_HOME)/krmllib/obj/* $(OBJ_DIR)
fstar.exe \
--cache_dir $(OBJ_DIR) \
--codegen krml \
--include $(KRML_HOME)/krmllib \
--cache_checked_modules \
--already_cached 'Prims FStar LowStar C TestLib' \
--warn_error '+241@247+285' \
--krmloutput $(KRML_OUTPUT) \
$(FST_FILE)
# Generate C and H files from .krml
$(C_OUTPUT) $(H_OUTPUT): $(KRML_OUTPUT)
krml -tmpdir $(BUILD_DIR) -no-prefix $(basename $(notdir $(FST_FILE))) $(KRML_OUTPUT) -o $(EXE_OUTPUT)
# Clean up generated files
clean:
rm -rf $(OBJ_DIR) $(BUILD_DIR)
run:
@$(EXE_OUTPUT)
# Phony targets
.PHONY: all clean