2 REQUIRES = threads hbugs-common helm-cic_proof_checking helm-getter \
3 helm-cic_textual_parser \
4 helm-mathql helm-mathql_interpreter helm-tactics
5 COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
7 OCAMLC = $(OCAMLFIND) ocamlc $(COMMONOPTS)
8 OCAMLOPT = $(OCAMLFIND) opt $(COMMONOPTS)
9 LINK_OPTIONS = -thread -package threads -linkpkg
10 TUTORS_TEMPLATE = hbugs_tutor.TPL.ml
11 TUTORS_INDEX = INDEX.xml
13 ring_tutor fourier_tutor reflexivity_tutor symmetry_tutor \
14 assumption_tutor contradiction_tutor exists_tutor split_tutor \
15 left_tutor right_tutor
16 TUTORS = $(GENERATED_TUTORS) search_pattern_apply_tutor
17 BUILD_TUTORS = ./build_tutors.ml
19 TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS))
20 GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS))
21 COMMON = hbugs_deity.cmo hbugs_tutors_common.cmo
22 COMMON_OPT = $(patsubst %.cmo,%.cmx,$(COMMON))
24 DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES))
25 DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES))
36 $(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX)
38 %_tutor: $(DEPS) $(COMMON) %_tutor.ml
39 $(OCAMLC) $(LINK_OPTIONS) -o $@ $(COMMON) $*_tutor.ml
40 %_tutor.opt: $(DEPSOPT) $(COMMON_OPT) %_tutor.ml
41 $(OCAMLOPT) $(LINK_OPTIONS) -o $@ $(COMMON_OPT) $*_tutor.ml
51 rm -f *.cm[aixo] *.cmxa *.[oa] $(TUTORS) $(TUTORS_OPT) $(GENERATED_TUTORS_SRC)
54 .PHONY: all world byte opt clean start stop