This commit was manufactured by cvs2svn to create branch

[helm.git] / helm / hbugs / tutors / Makefile

diff --git a/helm/hbugs/tutors/Makefile b/helm/hbugs/tutors/Makefile
deleted file mode 100644 (file)
index a585b0c..0000000
--- a/helm/hbugs/tutors/Makefile
+++ /dev/null
@@ -1,55 +0,0 @@
-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 $(COMMONOPTS)
-OCAMLOPT = $(OCAMLFIND) opt $(COMMONOPTS)
-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
-