helm/hbugs/tutors/Makefile

   1 METADIR = ../meta
   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)"
   6 OCAMLFIND = ocamlfind
   7 OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS)
   8 OCAMLOPT = $(OCAMLFIND) opt -thread $(COMMONOPTS)
   9 OCAMLDEP = $(OCAMLFIND) ocamldep -package "$(REQUIRES)"
  10 LINK_OPTIONS = -thread -package threads -linkpkg
  11 TUTORS_TEMPLATE = hbugs_tutor.TPL.ml
  12 TUTORS_INDEX = INDEX.xml
  13 GENERATED_TUTORS = \
  14         ring_tutor fourier_tutor reflexivity_tutor symmetry_tutor \
  15         assumption_tutor contradiction_tutor exists_tutor split_tutor \
  16         left_tutor right_tutor
  17 TUTORS = $(GENERATED_TUTORS) search_pattern_apply_tutor
  18 BUILD_TUTORS = ./build_tutors.ml
  19 CTL = ./sabba.sh
  20 TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS))
  21 GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS))
  22 COMMON = hbugs_deity.cmo hbugs_tutors_common.cmo
  23 COMMON_OPT = $(patsubst %.cmo,%.cmx,$(COMMON))
  24
  25 DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES))
  26 DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES))
  27
  28 all: byte
  29 world: byte opt
  30 byte: $(COMMON) $(TUTORS)
  31 opt: $(COMMON_OPT) $(TUTORS_OPT)
  32 start:
  33         $(CTL) start
  34 stop:
  35         $(CTL) stop
  36
  37 $(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX)
  38         $(BUILD_TUTORS)
  39 %_tutor: $(DEPS) $(COMMON) %_tutor.ml
  40         $(OCAMLC) $(LINK_OPTIONS) -o $@ $(COMMON) $*_tutor.ml
  41 %_tutor.opt: $(DEPSOPT) $(COMMON_OPT) %_tutor.ml
  42         $(OCAMLOPT) $(LINK_OPTIONS) -o $@ $(COMMON_OPT) $*_tutor.ml
  43
  44 %.cmi: %.mli
  45         $(OCAMLC) -c $<
  46 %.cmo: %.ml %.cmi
  47         $(OCAMLC) -c $<
  48 %.cmx: %.ml %.cmi
  49         $(OCAMLOPT) -c $<
  50
  51 clean:
  52         rm -f *.cm[aixo] *.cmxa *.[oa] $(TUTORS) $(TUTORS_OPT) $(GENERATED_TUTORS_SRC)
  53 distclean: clean
  54         rm -f run/*
  55 .PHONY: all world byte opt clean start stop
  56 .PRECIOUS: %.cmi
  57