Factorize Makefiles

Makefile.rules

+.SECONDARY:
+
+INCLUDE_DIRS=
+DKTACTICS_DIR=$(shell $(DKTACTICS))
+DKCHECK_OPT = -I $(DKTACTICS_DIR)/fol $(INCLUDE_DIRS) -errors-in-snf
+FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-ocaml-code -no-coq-code -stop-before-dk -dedukti-code
+
+%.dko: %.dk
+	$(DKCHECK) $(DKCHECK_OPT) -e -nl $<
+
+%.dko: %.sk
+	$(SKCHECK) $(DKCHECK_OPT) -e -nl $<
+
+%.sk: %.fcl
+	$(FOCALIZEC) $(FOCALIZEC_OPT) $<
+
+%.vo: %.v
+	$(COQC) $<

core/arith/Makefile

 include ../../.config_vars
+include ../../Makefile.rules
 
-.SUFFIXES: .dk .dko .sk .fcl
-.SECONDARY:
-
-all: natmorph.dko
-
+FCL_FILES=$(wildcard *.fcl)
 INCLUDE_DIRS= -I ../logic
 
-DKTACTICS_DIR=$(shell $(DKTACTICS))
-DKCHECK_OPT = -I $(DKTACTICS_DIR)/fol $(INCLUDE_DIRS) -coc
-FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-ocaml-code -no-coq-code -stop-before-dk --experimental
-
-.dk.dko:
-	$(DKCHECK) $(DKCHECK_OPT) -e -nl $<
-
-.sk.dko:
-	$(SKCHECK) $(DKCHECK_OPT) -e -nl $<
-
-.fcl.sk:
-	$(FOCALIZEC) $(FOCALIZEC_OPT) $<
-
-naturals.dko : naturals.sk
-natmorph.dko : natmorph.sk naturals.dko
+all: $(FCL_FILES:.fcl=.dko)
 
-natmorph.sk: naturals.dko
+depend: .depend
+.depend:
+	$(FOCALIZEDEP) $(FCL_FILES) > $@
+-include .depend
 
 clean :
-	rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.*
+	rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.* .depend $(FCL_FILES:.fcl=.sk)

core/logic/Makefile

 include ../../.config_vars
-
-.SUFFIXES: .dk .dko .sk .fcl
-.SECONDARY:
+include ../../Makefile.rules
 
 all: basics.dko zen.dko focal.dko
 
-DKTACTICS_DIR=$(shell $(DKTACTICS))
-DKCHECK_OPT = -I $(DKTACTICS_DIR)/fol -coc
-FOCALIZEC_OPT = -no-ocaml-code -no-coq-code -stop-before-dk --experimental
-
-.dk.dko:
-	$(DKCHECK) $(DKCHECK_OPT) -e -nl $<
-
-.sk.dko:
-	$(SKCHECK) $(DKCHECK_OPT) -e -nl $<
-
-.fcl.sk:
-	$(FOCALIZEC) $(FOCALIZEC_OPT) $<
-
 basics.dko: dk_builtins.dko
 cc.dko:
 dk_bool.dko: