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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
V=@
.PHONY: plugin install install-plugin clean quickChickTool compat
QCTOOL_DIR=quickChickTool
QCTOOL_EXE=quickChickTool.byte
QCTOOL_SRC=$(QCTOOL_DIR)/quickChickTool.ml \
$(QCTOOL_DIR)/quickChickToolTypes.ml \
$(QCTOOL_DIR)/quickChickToolLexer.mll \
$(QCTOOL_DIR)/quickChickToolParser.mly
INSTALLDIR?=$(dir $(shell which coqc))
# Here is a hack to make $(eval $(shell work
# (copied from coq_makefile generated stuff):
define donewline
endef
includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
$(call includecmdwithout@,$(COQBIN)coqtop -config)
all: quickChickTool plugin documentation-check
plugin: compat Makefile.coq
$(MAKE) -f Makefile.coq
documentation-check: plugin
coqc -R src QuickChick -Q doc doc -I plugin doc/QuickChickInterface.v
coqc -R src QuickChick -Q doc doc -I plugin doc/DocumentationCheck.v
TEMPFILE := $(shell mktemp)
install: quickChickTool plugin
$(V)$(MAKE) -f Makefile.coq install > $(TEMPFILE)
# Manually copying the remaining files
$(V)cp $(QCTOOL_DIR)/$(QCTOOL_EXE) $(INSTALLDIR)/quickChick
# $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick
# $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick
install-fuzz:
$(V)cp fuzz/alloc-inl.h $(COQLIB)/user-contrib/QuickChick/
$(V)cp fuzz/config.h $(COQLIB)/user-contrib/QuickChick/
$(V)cp fuzz/debug.h $(COQLIB)/user-contrib/QuickChick/
$(V)cp fuzz/types.h $(COQLIB)/user-contrib/QuickChick/
$(V)cp fuzz/SHM.c $(COQLIB)/user-contrib/QuickChick/
$(V)cp fuzz/Stub.ml $(COQLIB)/user-contrib/QuickChick/
$(V)cp fuzz/Main.ml $(COQLIB)/user-contrib/QuickChick/
$(V)cp fuzz/cmdprefix.pl $(COQLIB)/user-contrib/QuickChick/
$(V)cp fuzz/cmdsuffix.pl $(COQLIB)/user-contrib/QuickChick/
install-plugin: Makefile.coq
$(V)$(MAKE) -f Makefile.coq install | tee $(TEMPFILE)
uninstall:
$(V)if [ -e Makefile.coq ]; then $(MAKE) -f Makefile.coq uninstall; fi
$(RM) $(INSTALLDIR)/quickChick
quickChickTool: $(QCTOOL_DIR)/$(QCTOOL_EXE)
$(QCTOOL_DIR)/$(QCTOOL_EXE): $(QCTOOL_SRC)
cd $(QCTOOL_DIR); ocamlbuild -use-ocamlfind -pkg str -pkg unix -use-ocamlfind $(QCTOOL_EXE)
tests:
$(MAKE) -C tutorials tutorials
$(MAKE) -C test
cd benchmarks/stlc; make clean && make
cd benchmarks/BST; make clean && make
cd examples/ifc-basic; make clean && make
$(MAKE) -C examples/RedBlack test
$(MAKE) -C examples/multifile-mutation test
# This takes too long.
# $(MAKE) -C examples/c-mutation test
# coqc examples/BSTTest.v
coqc examples/DependentTest.v
coqc examples/TacticExample.v
COMPATFILES:= \
plugin/depDriver.ml \
plugin/genericLib.ml \
plugin/mergeTypes.ml \
plugin/quickChick.mli \
plugin/quickChick.mlg \
plugin/unifyQC.ml \
plugin/unifyQC.mli \
plugin/tactic_quickchick.mlg \
plugin/weightmap.mlg \
src/Compat.v \
src/ExtractionQC.v \
src/QuickChick.v \
src/TacticsUtil.v \
_CoqProject
compat: $(COMPATFILES)
%: %.cppo
$(V)cppo -V OCAML:$(shell ocamlc -version) -V COQ:$(word 1, $(shell coqc -print-version)) -n -o $@ $^
Makefile.coq: _CoqProject
$(V)coq_makefile -f _CoqProject -o Makefile.coq
clean:
$Vif [ -e Makefile.coq ]; then $(MAKE) -f Makefile.coq clean; fi
$Vcd $(QCTOOL_DIR); ocamlbuild -clean
# This might not work on macs
find . -name '*.vo' -print -delete
find . -name '*.glob' -print -delete
find . -name *.d -print -delete
find . -name *.o -print -delete
find . -name *.cmi -print -delete
find . -name *.cmx -print -delete
find . -name *.cmxs -print -delete
find . -name *.cmo -print -delete
find . -name *.bak -print -delete
find . -name *~ -print -delete
find . -name *.conflicts -print -delete
find . -name *.output -print -delete
find . -name *.aux -print -delete
rm -f Makefile.coq Makefile.coq.conf
rm -f $(COMPATFILES)
bc:
coqwc src/*.v
coqwc examples/RedBlack/*.v
coqwc ../ifc/*.v
.merlin: Makefile.coq
make -f Makefile.coq .merlin
publish%:
opam publish --packages-directory=released/packages \
--repo=coq/opam-coq-archive --tag=v$* -v $* QuickChick/QuickChick
|
