2024-01-24 19:52:46 +01:00
|
|
|
|
|
|
|
|
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
|
2024-11-08 16:30:15 +01:00
|
|
|
ocamlc $(INCLUDE) zarith.cma -o $@ $^
|
2024-01-24 19:52:46 +01:00
|
|
|
|
|
|
|
|
$(MAIN).opt: $(CMX) $(MAIN).cmx
|
2024-11-08 16:30:15 +01:00
|
|
|
$(OCAMLOPT) $(INCLUDE) zarith.cmxa -o $@ $^
|
2024-01-24 19:52:46 +01:00
|
|
|
|
|
|
|
|
$(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
|
