blob: 88823d6d724f3f8f46b23487d5030ef7ca38284b (
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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
TOPDIR=../../..
INCL= -I theories/Arith \
-I theories/Bool \
-I theories/Init \
-I theories/IntMap \
-I theories/Lists \
-I theories/Logic \
-I theories/Reals \
-I theories/Relations \
-I theories/Sets \
-I theories/Wellfounded \
-I theories/Zarith
MLNAMES=
CMONAMES=
include .names.ml
include .names.cmo
all: allml .depend allcmo
allml: .names.ml $(MLNAMES)
allcmo: .names.cmo $(CMONAMES)
.depend: Makefile
rm -f .depend; ocamldep $(INCL) theories/*/*.ml > .depend
.names.ml: Makefile v2ml
rm -f .names.ml; \
echo "MLNAMES= \\" > .names.ml; \
find theories -name \*.v -exec ./v2ml \{\} \; | \
sed -e "s/\.ml/.ml \\\\/" >> .names.ml
.names.cmo: .names.ml
rm -f .names.cmo; \
sed -e "1s/ML/CMO/" -e "s/\.ml/.cmo/" < .names.ml > .names.cmo
tree:
cp -fur $(TOPDIR)/theories .; rm -f theories/*/*.vo theories/*/*/*.vo
%.cmo:%.ml
ocamlc $(INCL) -c -i $<
%.ml: ml2v
./extract `./ml2v $@`
clean:
rm -f theories/*/*.ml theories/*/*.cm*
ml2v: ml2v.ml
ocamlc -o $@ $<
v2ml: v2ml.ml
ocamlc -o $@ $<
include .depend
|
