Makefile 1.17 KB
Newer Older
1

2 3 4
BENCH ?= no

ifeq ($(BENCH),yes)
5
  WHY3=../../bin/why3.opt
6 7
  WHY3SHARE=../../share
else
8 9 10 11 12
  ifeq ($(BINDIR),)
    WHY3=why3
  else
    WHY3=$(BINDIR)/why3
  endif
13
  WHY3SHARE=$(shell $(WHY3) --print-datadir)
14
endif
MARCHE Claude's avatar
MARCHE Claude committed
15 16 17

include $(WHY3SHARE)/Makefile.config

18 19 20 21
ifeq ($(BENCH),yes)
  INCLUDE += -I ../../lib/why3
endif

22 23 24 25 26 27 28 29 30
MAIN=main
OBJ=vstte10_max_sum__MaxAndSum2 vstte10_max_sum__TestCase

ML  = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))

OCAMLOPT=ocamlopt -noassert -inline 1000

31
all: $(MAIN).$(OCAMLBEST)
32 33 34

extract: $(ML)

35 36 37 38
doc:
	$(WHY3) doc ../vstte10_max_sum.mlw
	$(WHY3) session html .

39
$(MAIN).byte: $(CMO)  $(MAIN).cmo
MARCHE Claude's avatar
MARCHE Claude committed
40
	ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
41 42

$(MAIN).opt: $(CMX)  $(MAIN).cmx
MARCHE Claude's avatar
MARCHE Claude committed
43
	$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
44 45 46 47

$(MAIN).cmx: $(CMX)

$(ML): ../vstte10_max_sum.mlw
48
	$(WHY3) extract -D ocaml32 ../vstte10_max_sum.mlw -o .
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64

%.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
	rm -f why3__*.ml* vstte10_max_sum__*.ml* int__*.ml*