helm/hbugs/tutors/Makefile

   1 METADIR = ../meta
   2 REQUIRES = threads hbugs-common helm-cic_proof_checking helm-tactics helm-getter
   3 COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
   4 OCAMLFIND = ocamlfind
   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
  10 GENERATED_TUTORS = \
  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
  16 CTL = ./sabba.sh
  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))
  21
  22 all: byte
  23 world: byte opt
  24 byte: $(TUTORS)
  25 opt: $(TUTORS_OPT)
  26 start:
  27         $(CTL) start
  28 stop:
  29         $(CTL) stop
  30
  31 $(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX)
  32         $(BUILD_TUTORS)
  33 %_tutor: $(COMMON) %_tutor.ml
  34         $(OCAMLC) $(LINK_OPTIONS) -o $@ $^
  35 %_tutor.opt: $(COMMON_OPT) %_tutor.ml
  36         $(OCAMLOPT) $(LINK_OPTIONS) -o $@ $^
  37
  38 hbugs_tutors_common.cmi: hbugs_tutors_common.mli
  39         $(OCAMLC) -c $<
  40 $(COMMON): hbugs_tutors_common.ml hbugs_tutors_common.cmi
  41         $(OCAMLC) -c $<
  42 $(COMMON_OPT): hbugs_tutors_common.ml
  43         $(OCAMLOPT) -c $<
  44
  45 clean:
  46         rm -f *.cm[aixo] *.cmxa *.[oa] $(TUTORS) $(TUTORS_OPT) $(GENERATED_TUTORS_SRC)
  47 distclean: clean
  48         rm -f run/*
  49 .PHONY: all world byte opt clean start stop
  50