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
|
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../bin/why3.opt
WHY3SHARE=../../share
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
include $(WHY3SHARE)/Makefile.config
ifeq ($(BENCH),yes)
INCLUDE += -I ../../lib/why3
endif
MAIN=main
OBJ=split_string
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))
OCAMLOPT=ocamlopt -noassert -inline 1000
all: $(MAIN).$(OCAMLBEST)
extract: $(ML)
doc:
$(WHY3) doc ../split_string.mlw
$(WHY3) session html .
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc $(INCLUDE) zarith.cma -o $@ $^
$(MAIN).opt: $(CMX) $(MAIN).cmx
$(OCAMLOPT) $(INCLUDE) zarith.cmxa -o $@ $^
$(MAIN).cmx: $(CMX)
$(ML): ../split_string.mlw
$(WHY3) extract -D ocaml64 -L . -L .. -D split_string.drv -o $@ split_string.SplitStringOCaml
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
%.cmo: %.ml
ocamlc $(INCLUDE) -annot -c $<
%.cmi: %.mli
ocamlc $(INCLUDE) -annot -c $<
clean::
rm -f $(ML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
|
