-
Notifications
You must be signed in to change notification settings - Fork 2
/
Makefile.coq.local
65 lines (58 loc) · 4.7 KB
/
Makefile.coq.local
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
INCLUDE=certicoq/plugin/runtime
GCDIR=certicoq/plugin/runtime
GLUE_FILES=examples/uint63z/glue.v examples/uint63nat/glue.v examples/compose/glue.v examples/array/glue.v examples/bytestring/glue.v
PRIMS_FILES=examples/uint63z/prims.v examples/uint63nat/prims.v examples/compose/prims.v examples/array/prims.v examples/bytestring/prims.v
GENERATED_VFILES= $(GLUE_FILES) $(PRIMS_FILES)
glue_files: $(GLUE_FILES)
prims_files: $(PRIMS_FILES)
generated_vfiles: $(GENERATED_VFILES)
examples/uint63nat/glue.c examples/uint63nat/glue.h examples/uint63nat/prog.c examples/uint63nat/prog.h : examples/uint63nat/gluegen.v examples/uint63nat/prog.vo
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
examples/uint63nat/gc_stack.o: $(GCDIR)/gc_stack.c $(GCDIR)/gc_stack.h $(GCDIR)/m.h $(GCDIR)/config.h $(GCDIR)/values.h
$(CC) $(CFLAGS) -I$(INCLUDE) -c $< -o $@
uint63nat-c: examples/uint63nat/prog.c examples/uint63nat/main.c examples/uint63nat/gc_stack.o examples/uint63nat/glue.c examples/uint63nat/prims.c
cd examples/uint63nat; $(CC) ../../$(INCLUDE) -w -g -o prog main.c gc_stack.o prog.c glue.c prims.c
examples/uint63nat/prims.v: examples/uint63nat/prims.c examples/uint63nat/glue.h
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/uint63nat/glue.v: examples/uint63nat/glue.c
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/uint63z/glue.c examples/uint63z/glue.h examples/uint63z/prog.c examples/uint63z/prog.h : examples/uint63z/gluegen.v examples/uint63z/prog.vo
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
examples/uint63z/gc_stack.o: $(GCDIR)/gc_stack.c $(GCDIR)/gc_stack.h $(GCDIR)/m.h $(GCDIR)/config.h $(GCDIR)/values.h
$(CC) $(CFLAGS) -I$(INCLUDE) -c $< -o $@
uint63z-c: examples/uint63z/prog.c examples/uint63z/main.c examples/uint63z/gc_stack.o examples/uint63z/glue.c examples/uint63z/prims.c
cd examples/uint63z; $(CC) ../../$(INCLUDE) -w -g -o prog main.c gc_stack.o prog.c glue.c prims.c
examples/uint63z/prims.v: examples/uint63z/prims.c examples/uint63z/glue.h
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/uint63z/glue.v: examples/uint63z/glue.c
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/array/glue.c examples/array/glue.h examples/array/prog.c examples/array/prog.h : examples/array/gluegen.v examples/array/prog.vo
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
examples/array/gc_stack.o: $(GCDIR)/gc_stack.c $(GCDIR)/gc_stack.h $(GCDIR)/m.h $(GCDIR)/config.h $(GCDIR)/values.h
$(CC) $(CFLAGS) -I$(INCLUDE) -c $< -o $@
array-c: examples/array/prog.c examples/array/main.c examples/array/gc_stack.o examples/array/glue.c examples/array/prims.c
cd examples/array; $(CC) ../../$(INCLUDE) -w -g -o prog main.c gc_stack.o prog.c glue.c prims.c
examples/array/prims.v: examples/array/prims.c examples/array/glue.h
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/array/glue.v: examples/array/glue.c
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/bytestring/glue.c examples/bytestring/glue.h examples/bytestring/prog.c examples/bytestring/prog.h : examples/bytestring/gluegen.v examples/bytestring/prog.vo
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
examples/bytestring/gc_stack.o: $(GCDIR)/gc_stack.c $(GCDIR)/gc_stack.h $(GCDIR)/m.h $(GCDIR)/config.h $(GCDIR)/values.h
$(CC) $(CFLAGS) -I$(INCLUDE) -c $< -o $@
bytestring-c: examples/bytestring/prog.c examples/bytestring/main.c examples/bytestring/gc_stack.o examples/bytestring/glue.c examples/bytestring/prims.c
cd examples/bytestring; $(CC) ../../$(INCLUDE) -w -g -o prog main.c gc_stack.o prog.c glue.c prims.c
examples/bytestring/prims.v: examples/bytestring/prims.c examples/bytestring/glue.h
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/bytestring/glue.v: examples/bytestring/glue.c
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/compose/glue.c examples/compose/glue.h examples/compose/prog.c examples/compose/prog.h : examples/compose/gluegen.v examples/compose/prog.vo
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
examples/compose/gc_stack.o: $(GCDIR)/gc_stack.c $(GCDIR)/gc_stack.h $(GCDIR)/m.h $(GCDIR)/config.h $(GCDIR)/values.h
$(CC) $(CFLAGS) -I$(INCLUDE) -c $< -o $@
compose-c: examples/compose/prog.c examples/compose/main.c examples/compose/gc_stack.o examples/compose/glue.c examples/compose/prims.c
cd examples/compose; $(CC) ../../$(INCLUDE) -w -g -o prog main.c gc_stack.o prog.c glue.c prims.c
examples/compose/prims.v: examples/compose/prims.c examples/compose/glue.h
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@
examples/compose/glue.v: examples/compose/glue.c
clightgen -I$(INCLUDE) -normalize -DVERIFFI -DCOMPCERT $< -o $@