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: $(TUTORS) 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