examples/split_string/Makefile

   1
   2 BENCH ?= no
   3
   4 ifeq ($(BENCH),yes)
   5   WHY3=../../bin/why3.opt
   6   WHY3SHARE=../../share
   7 else
   8   ifeq ($(BINDIR),)
   9     WHY3=why3
  10   else
  11     WHY3=$(BINDIR)/why3
  12   endif
  13   WHY3SHARE=$(shell $(WHY3) --print-datadir)
  14 endif
  15
  16 include $(WHY3SHARE)/Makefile.config
  17
  18 ifeq ($(BENCH),yes)
  19   INCLUDE += -I ../../lib/why3
  20 endif
  21
  22 MAIN=main
  23 OBJ=split_string
  24
  25 ML  = $(addsuffix .ml, $(OBJ))
  26 CMO = $(addsuffix .cmo, $(OBJ))
  27 CMX = $(addsuffix .cmx, $(OBJ))
  28
  29 OCAMLOPT=ocamlopt -noassert -inline 1000
  30
  31 all: $(MAIN).$(OCAMLBEST)
  32
  33 extract: $(ML)
  34
  35 doc:
  36         $(WHY3) doc ../split_string.mlw
  37         $(WHY3) session html .
  38
  39 $(MAIN).byte: $(CMO)  $(MAIN).cmo
  40         ocamlc $(INCLUDE) zarith.cma -o $@ $^
  41
  42 $(MAIN).opt: $(CMX)  $(MAIN).cmx
  43         $(OCAMLOPT) $(INCLUDE) zarith.cmxa -o $@ $^
  44
  45 $(MAIN).cmx: $(CMX)
  46
  47 $(ML): ../split_string.mlw
  48         $(WHY3) extract -D ocaml64 -L . -L .. -D split_string.drv -o $@ split_string.SplitStringOCaml
  49
  50 %.cmx: %.ml
  51         $(OCAMLOPT) $(INCLUDE) -annot -c $<
  52
  53 %.cmo: %.ml
  54         ocamlc $(INCLUDE) -annot -c $<
  55
  56 %.cmi: %.mli
  57         ocamlc $(INCLUDE) -annot -c $<
  58
  59 clean::
  60         rm -f $(ML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte