2 REQUIRES = threads hbugs-common helm-cic_proof_checking helm-tactics helm-getter
3 COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
5 OCAMLC = $(OCAMLFIND) ocamlc $(COMMONOPTS)
6 OCAMLOPT = $(OCAMLFIND) opt $(COMMONOPTS)
7 LINK_OPTIONS = -thread -package threads -linkpkg
8 TUTORS_TEMPLATE = hbugs_tutor.TPL.ml
9 TUTORS_INDEX = INDEX.xml
11 ring_tutor fourier_tutor reflexivity_tutor symmetry_tutor \
12 assumption_tutor contradiction_tutor exists_tutor split_tutor \
13 left_tutor right_tutor
14 TUTORS = $(GENERATED_TUTORS) search_pattern_apply_tutor
15 BUILD_TUTORS = ./build_tutors.ml
17 TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS))
18 GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS))
19 COMMON = hbugs_tutors_common.cmo
20 COMMON_OPT = $(patsubst %.cmo,%.cmx,$(COMMON))
31 $(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX)
33 %_tutor: $(COMMON) %_tutor.ml
34 $(OCAMLC) $(LINK_OPTIONS) -o $@ $^
35 %_tutor.opt: $(COMMON_OPT) %_tutor.ml
36 $(OCAMLOPT) $(LINK_OPTIONS) -o $@ $^
38 hbugs_tutors_common.cmi: hbugs_tutors_common.mli
40 $(COMMON): hbugs_tutors_common.ml hbugs_tutors_common.cmi
42 $(COMMON_OPT): hbugs_tutors_common.ml
46 rm -f *.cm[aixo] *.cmxa *.[oa] $(TUTORS) $(TUTORS_OPT) $(GENERATED_TUTORS_SRC)
49 .PHONY: all world byte opt clean start stop