blob: 42b2414475576bba5ba912d1d6a4b8638df23f6f (
plain)
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
|
########################################################################
## This file is intended to developers: please do not use it ##
## directly, rather use the "configure.sh" script. ##
########################################################################
test :
cd ../unit-tests; make cleanvo; make
ztest :
cd ../unit-tests; make cleanvo; make zchaff
vtest :
cd ../unit-tests; make cleanvo; make verit
lfsctest :
cd ../unit-tests; make cleanvo; make lfsc
paralleltest :
cd ../unit-tests; make parallel
clean::
cd ../unit-tests; make clean
cleanall::
rm -f ../3rdparty/alt-ergo/smtlib2_lex.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_parse.mli .lia.cache Makefile Makefile.conf Makefile.local Tactics.v _CoqProject g_smtcoq.ml4 lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli smtcoq_plugin.mlpack smtlib2/sExprLexer.ml smtlib2/sExprParser.ml smtlib2/sExprParser.mli verit/veritLexer.ml verit/veritParser.ml verit/veritParser.mli versions/standard/Array/PArray.v versions/standard/Int63/Int63.v versions/standard/Int63/Int63Axioms.v versions/standard/Int63/Int63Native.v versions/standard/Int63/Int63Op.v versions/standard/Int63/Int63Properties.v versions/standard/Structures.v
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
%.ml : %.mll
$(CAMLLEX) $<
%.ml %.mli : %.mly
$(CAMLYACC) $<
.PHONY: smtcoq_plugin.mlpack.d
smtcoq_plugin.mlpack.d : verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
|