examples_in_progress/sudoku_reloaded/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 GEN = map__Map sudoku_reloaded__Grid sudoku_reloaded__TheClassicalSudokuGrid sudoku_reloaded__Solver
  24 OBJ=$(GEN)
  25
  26 GENML = $(addsuffix .ml, $(GEN))
  27 ML = $(addsuffix .ml, $(OBJ))
  28 CMO = $(addsuffix .cmo, $(OBJ))
  29 CMX = $(addsuffix .cmx, $(OBJ))
  30
  31 OCAMLOPT = ocamlopt -noassert -inline 1000
  32
  33 all: $(MAIN).opt
  34
  35 extract: $(GENML)
  36
  37 doc:
  38         $(WHY3) doc ../sudoku_reloaded.mlw
  39         $(WHY3) session html .
  40
  41 $(MAIN).byte: $(CMO) $(MAIN).cmo
  42         ocamlc -g $(INCLUDE) zarith.cma why3extract.cma -o $@ $^
  43
  44 $(MAIN).opt: $(CMX) $(MAIN).cmx
  45         $(OCAMLOPT) $(INCLUDE) zarith.cmxa why3extract.cmxa -o $@ $^
  46
  47 $(MAIN).cmx: $(CMX)
  48
  49 $(GENML): ../sudoku_reloaded.mlw
  50         $(WHY3) extract -D ocaml32 ../sudoku_reloaded.mlw -o .
  51
  52 # javascript
  53
  54
  55 JSMAIN=jsmain
  56
  57 JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
  58           -syntax camlp4o
  59
  60 $(JSMAIN).js: $(JSMAIN).byte
  61         js_of_ocaml $(JSMAIN).byte
  62
  63 $(JSMAIN).byte: $(CMO) $(JSMAIN).cmo
  64         $(JSOCAMLC) $(INCLUDE) zarith.cma why3extract.cma -o $@ -linkpkg $^
  65
  66 %.cmo: %.ml
  67         $(JSOCAMLC) $(INCLUDE) -annot -c $<
  68
  69 %.cmi: %.mli
  70         $(JSOCAMLC) $(INCLUDE) -annot -c $<
  71
  72 %.cmx: %.ml
  73         $(OCAMLOPT) $(INCLUDE) -annot -c $<
  74
  75 clean::
  76         rm -f $(GENML) *.annot *.o *.cm[xio] $(MAIN).opt $(MAIN).byte
  77         rm -f sudoku__*.ml why3__*.ml
  78         rm -f int__Int.ml map__Map.ml array__Array.ml