-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathMakefile
111 lines (98 loc) · 2.99 KB
/
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
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
106
107
108
109
110
111
.PHONY: all install plugin check checker clean development-without-install revert-development-without-install
-include Makefile.coq.conf
all : Makefile.coq
$(MAKE) -f Makefile.coq $@
install : Makefile.coq
test ! theories -ef $(COQMF_COQLIB)/user-contrib/codegen || ( echo "$(COQMF_COQLIB)/user-contrib/codegen is linked to theories. No need to install."; false )
$(MAKE) -f Makefile.coq $@
uninstall : Makefile.coq
test ! theories -ef $(COQMF_COQLIB)/user-contrib/codegen || ( echo "$(COQMF_COQLIB)/user-contrib/codegen is linked to theories. Use revert-development-without-install."; false )
$(MAKE) -f Makefile.coq $@
ifdef COQMF_COQLIB
development-without-install : revert-development-without-install
ln -s ../src/META.coq-codegen theories
ln -s ../src/codegen_plugin.cmi theories
ln -s ../src/codegen_plugin.cmxs theories
ln -s ../src/codegen_plugin.cmxa theories
ln -s ../src/codegen_plugin.cmx theories
ln -s `pwd`/theories $(COQMF_COQLIB)/user-contrib/codegen
revert-development-without-install :
rm -f "$(COQMF_COQLIB)/user-contrib/codegen" || ( echo "Do 'make uninstall' first"; false )
rm -f theories/META.coq-codegen
rm -f theories/codegen_plugin.cmi
rm -f theories/codegen_plugin.cmxs
rm -f theories/codegen_plugin.cmxa
rm -f theories/codegen_plugin.cmx
else
development-without-install :
@echo 'COQMF_COQLIB not defined. run "make" first.'
revert-development-without-install :
@echo 'COQMF_COQLIB not defined. run "make" first.'
endif
plugin : Makefile.coq
$(MAKE) -f Makefile.coq src/codegen_plugin.cmxs
.merlin : Makefile.coq
$(MAKE) -f Makefile.coq .merlin
# Makefile.coq.conf is also generated by coq_makefile.
Makefile.coq : _CoqProject
coq_makefile -f _CoqProject -o Makefile.coq
check checker:
cd test; $(MAKE) $@
coqc test/test_verify.v
run-sample:
coqtop -batch -l sample/ind.v
coqtop -batch -l sample/genc.v
coqc -Q theories codegen -I src sample/pow.v
gcc -g -Wall sample/pow.c -o sample/pow
sample/pow
coqc -Q theories codegen -I src sample/rank.v
gcc -g -Wall sample/rank.c -o sample/rank
sample/rank 11011110001010101111
coqc -Q theories codegen -I src sample/sprintf.v
gcc -g -Wall sample/sprintf.c -o sample/sprintf
sample/sprintf
(cd sample/lseq; make clean all; ./test_lseq)
clean :
rm -f \
.Makefile.coq.d \
src/g_codegen.ml \
src/*.o \ \
src/*.cmi \
src/*.cmo \
src/*.cmx \
src/*.cma \
src/*.cmt \
src/*.cmti \
src/*.cmxa \
src/*.cmxs \
src/*.a \
src/*.d \
src/*.annot \
theories/*.glob \
theories/*.vo \
theories/*.vok \
theories/*.vos \
theories/*.d \
theories/.*.aux \
test/*.cache \
test/test_codegen \
test/*.cmi \
test/*.cmx \
test/*.o \
test/oUnit-* \
sample/pow \
sample/rank \
sample/*.vo \
sample/*.vok \
sample/*.vos \
sample/*.glob \
sample/.*.aux \
oUnit-*
distclean : clean
rm -f \
Makefile.coq \
Makefile.coq.conf \
theories/codegen_plugin.cmi \
theories/codegen_plugin.cmx \
theories/codegen_plugin.cmxa \
theories/codegen_plugin.cmxs