METADIR = ../meta
REQUIRES = threads hbugs-common helm-cic_proof_checking helm-getter \
        helm-cic_textual_parser \
        helm-mathql helm-mathql_interpreter helm-tactics  
COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
OCAMLFIND = ocamlfind
OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS)
OCAMLOPT = $(OCAMLFIND) opt -thread $(COMMONOPTS)
OCAMLDEP = $(OCAMLFIND) ocamldep -package "$(REQUIRES)"
LINK_OPTIONS = -thread -package threads -linkpkg
TUTORS_TEMPLATE = hbugs_tutor.TPL.ml
TUTORS_INDEX = INDEX.xml
GENERATED_TUTORS = \
	ring_tutor fourier_tutor reflexivity_tutor symmetry_tutor \
	assumption_tutor contradiction_tutor exists_tutor split_tutor \
	left_tutor right_tutor
TUTORS = $(GENERATED_TUTORS) search_pattern_apply_tutor
BUILD_TUTORS = ./build_tutors.ml
CTL = ./sabba.sh
TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS))
GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS))
COMMON = hbugs_deity.cmo hbugs_tutors_common.cmo
COMMON_OPT = $(patsubst %.cmo,%.cmx,$(COMMON))

DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES))
DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES))

all: byte
world: byte opt
byte: $(COMMON) $(TUTORS)
opt: $(COMMON_OPT) $(TUTORS_OPT)
start:
	$(CTL) start
stop:
	$(CTL) stop

$(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX)
	$(BUILD_TUTORS)
%_tutor: $(DEPS) $(COMMON) %_tutor.ml
	$(OCAMLC) $(LINK_OPTIONS) -o $@ $(COMMON) $*_tutor.ml
%_tutor.opt: $(DEPSOPT) $(COMMON_OPT) %_tutor.ml
	$(OCAMLOPT) $(LINK_OPTIONS) -o $@ $(COMMON_OPT) $*_tutor.ml

%.cmi: %.mli
	$(OCAMLC) -c $<
%.cmo: %.ml %.cmi
	$(OCAMLC) -c $<
%.cmx: %.ml %.cmi
	$(OCAMLOPT) -c $<

clean:
	rm -f *.cm[aixo] *.cmxa *.[oa] $(TUTORS) $(TUTORS_OPT) $(GENERATED_TUTORS_SRC)
distclean: clean
	rm -f run/*
.PHONY: all world byte opt clean start stop
.PRECIOUS: %.cmi