X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2FMakefile;h=9e84bf4e671bae3c96dd05705b5aaf1d7ee690e2;hb=1fb8d0192e1f7ee891c53dc282c9c9f111e63e3c;hp=6a3f718d59a7aed1d75387112a113dc1c7b69d9d;hpb=ed90e027472d0250d45ae7200600c8804dd476f1;p=helm.git

diff --git a/helm/hbugs/tutors/Makefile b/helm/hbugs/tutors/Makefile
index 6a3f718d5..9e84bf4e6 100644
--- a/helm/hbugs/tutors/Makefile
+++ b/helm/hbugs/tutors/Makefile
@@ -1,9 +1,12 @@
 METADIR = ../meta
-REQUIRES = threads hbugs-common helm-cic_proof_checking helm-tactics helm-getter
+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)
+OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS)
+OCAMLOPT = $(OCAMLFIND) opt -thread $(COMMONOPTS)
+OCAMLDEP = $(OCAMLFIND) ocamldep -package "$(REQUIRES)"
 LINK_OPTIONS = -thread -package threads -linkpkg
 TUTORS_TEMPLATE = hbugs_tutor.TPL.ml
 TUTORS_INDEX = INDEX.xml
@@ -16,13 +19,16 @@ BUILD_TUTORS = ./build_tutors.ml
 CTL = ./sabba.sh
 TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS))
 GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS))
-COMMON = hbugs_tutors_common.cmo
+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)
+byte: $(COMMON) $(TUTORS)
+opt: $(COMMON_OPT) $(TUTORS_OPT)
 start:
 	$(CTL) start
 stop:
@@ -30,16 +36,16 @@ stop:
 
 $(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX)
 	$(BUILD_TUTORS)
-%_tutor: $(COMMON) %_tutor.ml
-	$(OCAMLC) $(LINK_OPTIONS) -o $@ $^
-%_tutor.opt: $(COMMON_OPT) %_tutor.ml
-	$(OCAMLOPT) $(LINK_OPTIONS) -o $@ $^
+%_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
 
-hbugs_tutors_common.cmi: hbugs_tutors_common.mli
+%.cmi: %.mli
 	$(OCAMLC) -c $<
-$(COMMON): hbugs_tutors_common.ml hbugs_tutors_common.cmi
+%.cmo: %.ml %.cmi
 	$(OCAMLC) -c $<
-$(COMMON_OPT): hbugs_tutors_common.ml
+%.cmx: %.ml %.cmi
 	$(OCAMLOPT) -c $<
 
 clean:
@@ -47,4 +53,5 @@ clean:
 distclean: clean
 	rm -f run/*
 .PHONY: all world byte opt clean start stop
+.PRECIOUS: %.cmi