Makefile: the clean target

Jacques-Pascal's idea, pushed a bit further

Makefile.in

@@ -82,6 +82,9 @@ EXTLIBS = str unix nums dynlink @ZIPLIB@
 EXTCMA	= $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
 EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
 
+INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
+COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo annot dep output
+
 TARGET_EMACS = share/emacs/why3.elc
 
 ###############
@@ -100,6 +103,10 @@ endif
 .PHONY: byte opt clean depend all install install_local install_no_local
 .PHONY: plugins plugins.byte plugins.opt
 
+CLEANDIRS =
+CLEANLIBS =
+GENERATED =
+
 ##############
 # Why3 library
 ##############
@@ -183,9 +190,6 @@ lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
 	cp lib/ocaml/why3__BigInt_num.ml $@
 endif
 
-clean::
-	rm -f lib/ocaml/why3__BigInt_compat.ml
-
 # Ocamlzip
 
 ifeq (@enable_zip@,yes)
@@ -196,9 +200,6 @@ src/session/compress.ml: config.status src/session/compress_none.ml
 	cp src/session/compress_none.ml $@
 endif
 
-clean::
-	rm -f src/session/compress.ml
-
 # build targets
 
 byte: lib/why3/why3.cma
@@ -228,18 +229,9 @@ endif
 
 depend: $(LIBDEP)
 
-LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
-LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
-	   $(addsuffix /*.annot, $(LIBSDIRS)) \
-	   $(addsuffix /*.output, $(LIBSDIRS)) \
-	   $(addsuffix /*.automaton, $(LIBSDIRS)) \
-	   $(addsuffix /*.dep, $(LIBSDIRS)) \
-	   $(addsuffix /*.o, $(LIBSDIRS)) \
-	   $(addsuffix /*~, $(LIBSDIRS))
-
-clean::
-	rm -f $(LIBCLEAN) $(LIBGENERATED)
-	rm -f lib/why3/why3session.* lib/why3/why3.cm* lib/why3/why3.[ao]
+CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
+CLEANLIBS += lib/why3/why3session lib/why3/why3
+GENERATED += $(LIBGENERATED)
 
 ###############
 # installation
@@ -285,7 +277,7 @@ endif
 
 install_no_local_lib::
 	mkdir -p $(OCAMLINSTALLLIB)/why3
-	cp -f lib/why3/why3.cm* lib/why3/why3.[ao] \
+	cp -f $(addprefix lib/why3/why3., $(INSTALLED_LIB_EXTS)) \
 		lib/why3/META $(OCAMLINSTALLLIB)/why3
 
 ifeq (@enable_local@,yes)
@@ -410,15 +402,6 @@ lib/plugins/tptp.cmo: $(TPTPCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
 
-PLUGSDIRS = plugins $(addprefix plugins/, $(PLUGDIRS))
-PLUGCLEAN = $(addsuffix /*.cm[iox], $(PLUGSDIRS)) \
-	    $(addsuffix /*.annot, $(PLUGSDIRS)) \
-	    $(addsuffix /*.output, $(PLUGSDIRS)) \
-	    $(addsuffix /*.automaton, $(PLUGSDIRS)) \
-	    $(addsuffix /*.dep, $(PLUGSDIRS)) \
-	    $(addsuffix /*.o, $(PLUGSDIRS)) \
-	    $(addsuffix /*~, $(PLUGSDIRS))
-
 # depend and clean targets
 
 ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
@@ -427,9 +410,8 @@ endif
 
 depend: $(PLUGDEP)
 
-clean::
-	rm -f $(PLUGCLEAN) $(PLUGGENERATED)
-	rm -f lib/plugins/*
+CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
+GENERATED += $(PLUGGENERATED)
 
 install_no_local::
 	mkdir -p $(LIBDIR)/why3/plugins
@@ -439,7 +421,11 @@ install_no_local::
 # Why3 commands
 ###############
 
-TOOLS_BIN = why3config why3execute why3extract why3prove why3realize why3replay
+TOOLSGENERATED = src/tools/why3wc.ml
+
+TOOLS_BIN = why3config why3execute why3extract why3prove \
+	    why3realize why3replay why3wc
+
 TOOLS_FILES = main $(TOOLS_BIN)
 
 TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))
@@ -451,6 +437,8 @@ TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))
 $(TOOLSDEP): DEPFLAGS += -I src/tools
 $(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
 
+$(TOOLSDEP): $(TOOLSGENERATED)
+
 byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
 opt:  bin/why3.opt  $(TOOLS_BIN:%=bin/%.opt)
 
@@ -510,6 +498,14 @@ bin/why3replay.byte: lib/why3/why3.cma src/tools/why3replay.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 
+bin/why3wc.opt: src/tools/why3wc.cmx
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
+
+bin/why3wc.byte: src/tools/why3wc.cmo
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
+
 clean_old_install::
 	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
 	rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
@@ -522,6 +518,7 @@ install_no_local::
 	cp -f bin/why3prove.@OCAMLBEST@   $(TOOLDIR)/why3prove$(EXE)
 	cp -f bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE)
 	cp -f bin/why3replay.@OCAMLBEST@  $(TOOLDIR)/why3replay$(EXE)
+	cp -f bin/why3wc.@OCAMLBEST@      $(TOOLDIR)/why3wc$(EXE)
 
 install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
 
@@ -534,17 +531,11 @@ endif
 
 depend: $(TOOLSDEP)
 
+CLEANDIRS += src/tools
+GENERATED += $(TOOLSGENERATED)
+
 clean::
-	rm -f src/tools/main.cm[iox] src/tools/main.annot src/tools/main.o src/tools/main.dep
-	rm -f src/tools/why3config.cm[iox] src/tools/why3config.annot src/tools/why3config.o src/tools/why3config.dep
-	rm -f src/tools/why3execute.cm[iox] src/tools/why3execute.annot src/tools/why3execute.o src/tools/why3execute.dep
-	rm -f src/tools/why3extract.cm[iox] src/tools/why3extract.annot src/tools/why3extract.o src/tools/why3extract.dep
-	rm -f src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep
-	rm -f src/tools/why3realize.cm[iox] src/tools/why3realize.annot src/tools/why3realize.o src/tools/why3realize.dep
-	rm -f src/tools/why3replay.cm[iox] src/tools/why3replay.annot src/tools/why3replay.o src/tools/why3replay.dep
-	rm -f $(addprefix bin/,$(TOOLS_BIN))
-	rm -f $(TOOLS_BIN:%=bin/%.byte) $(TOOLS_BIN:%=bin/%.opt)
-	rm -f bin/why3.byte bin/why3.opt bin/why3
+	rm -f bin/why3*
 
 ##############
 # test targets
@@ -680,11 +671,7 @@ endif
 
 depend: $(IDEDEP)
 
-clean::
-	rm -f src/ide/xml.ml
-	rm -f src/ide/*.cm[iox] src/ide/*.o
-	rm -f src/ide/*.annot src/ide/*.dep src/ide/*~
-	rm -f bin/why3ide.byte bin/why3ide.opt bin/why3ide
+CLEANDIRS += src/ide
 
 clean_old_install::
 	rm -f $(BINDIR)/why3ide$(EXE)
@@ -700,9 +687,9 @@ endif
 # Session
 ###############
 
-SESSION_FILES = why3session_lib why3session_copy why3session_info	\
-		why3session_latex why3session_html why3session_rm	\
-		why3session_output why3session_run why3session_csv	\
+SESSION_FILES = why3session_lib why3session_copy why3session_info \
+		why3session_latex why3session_html why3session_rm \
+		why3session_output why3session_run why3session_csv \
 		why3session_main
 
 SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
@@ -735,10 +722,7 @@ endif
 
 depend: $(SESSIONDEP)
 
-clean::
-	rm -f src/why3session/*.cm[iox] src/why3session/*.o
-	rm -f src/why3session/*.annot src/why3session/*.dep src/why3session/*~
-	rm -f bin/why3session.byte bin/why3session.opt bin/why3session
+CLEANDIRS += src/why3session
 
 clean_old_install::
 	rm -f $(BINDIR)/why3session$(EXE)
@@ -811,13 +795,13 @@ endif
 
 depend: $(COQPDEP)
 
+CLEANDIRS += src/coq-tactic
+CLEANLIBS += lib/coq-tactic/why3tac
+GENERATED += $(COQPGENERATED)
+
 clean::
-	rm -f src/coq-tactic/*.cm[iox] src/coq-tactic/*.o
-	rm -f lib/coq-tactic/*.cma lib/coq-tactic/*.cmxs
 	rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob
-	rm -f src/coq-tactic/*.annot src/coq-tactic/*.dep src/coq-tactic/*~
 	rm -f src/coq-tactic/.why3-vo-*
-	rm -f $(COQPGENERATED)
 
 install_no_local::
 	mkdir -p $(LIBDIR)/why3/coq-tactic
@@ -1211,22 +1195,8 @@ $(OCAMLLIBS_DEP): DEPFLAGS += -I src/util -I lib/ocaml @BIGINTINCLUDE@
 $(OCAMLLIBS_CMO) $(OCAMLLIBS_CMX): INCLUDES += -I src/util -I lib/ocaml @BIGINTINCLUDE@
 $(OCAMLLIBS_CMX): OFLAGS += -for-pack Why3extract
 
-ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(OCAMLLIBS_DEP)
-endif
-
-$(OCAMLLIBS_DEP): lib/ocaml/why3__BigInt_compat.ml
-
-depend: $(OCAMLLIBS_DEP)
-
-clean::
-	rm -f lib/ocaml/*.cm[iox] lib/ocaml/*.o
-	rm -f lib/ocaml/*.annot lib/ocaml/*.dep
-
-opt: $(OCAMLLIBS_CMX)
-
 byte: $(OCAMLLIBS_CMO)
-
+opt:  $(OCAMLLIBS_CMX)
 
 byte: lib/why3/why3extract.cma
 opt:  lib/why3/why3extract.cmxa
@@ -1249,8 +1219,19 @@ lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX)
 
 install_no_local_lib::
 	mkdir -p $(OCAMLINSTALLLIB)/why3
-	cp -f lib/why3/why3extract.cm* lib/why3/why3extract.[ao] \
-		$(OCAMLINSTALLLIB)/why3
+	cp -f $(addprefix lib/why3/why3extract., $(INSTALLED_LIB_EXTS)) \
+	  $(OCAMLINSTALLLIB)/why3
+
+ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
+include $(OCAMLLIBS_DEP)
+endif
+
+$(OCAMLLIBS_DEP): lib/ocaml/why3__BigInt_compat.ml
+
+depend: $(OCAMLLIBS_DEP)
+
+CLEANDIRS += lib/ocaml
+CLEANLIBS += lib/why3/why3extract
 
 ################
 # Jessie3 plugin
@@ -1269,7 +1250,8 @@ jessie.opt: src/jessie/Makefile lib/why3/why3.cmxa
 
 install_no_local::
 	mkdir -p $(FRAMAC_LIBDIR)/plugins/
-	cp -f src/jessie/Jessie3.cm* $(FRAMAC_LIBDIR)/plugins/
+	cp -f $(addprefix src/jessie/Jessie3., $(INSTALLED_LIB_EXTS)) \
+	  $(FRAMAC_LIBDIR)/plugins/
 
 clean::
 	$(MAKE) -C src/jessie clean
@@ -1288,61 +1270,12 @@ lib/why3-cpulimit$(EXE): src/tools/@CPULIMIT@.c
 	$(CC) -Wall -o $@ $^
 
 clean::
-	rm -f lib/why3-cpulimit$(EXE) src/tools/*~
+	rm -f lib/why3-cpulimit$(EXE)
 
 install_no_local::
 	cp -f lib/why3-cpulimit$(EXE) $(LIBDIR)/why3/why3-cpulimit$(EXE)
 	cp -f lib/why3-call-pvs $(LIBDIR)/why3/why3-call-pvs
 
-########
-# why3wc
-########
-
-WHY3WCGENERATED = src/tools/why3wc.ml
-
-WHY3WC_FILES = why3wc
-WHY3WCMODULES = $(addprefix src/tools/, $(WHY3WC_FILES))
-
-WHY3WCDEP = $(addsuffix .dep, $(WHY3WCMODULES))
-WHY3WCCMO = $(addsuffix .cmo, $(WHY3WCMODULES))
-WHY3WCCMX = $(addsuffix .cmx, $(WHY3WCMODULES))
-
-$(WHY3WCDEP): DEPFLAGS += -I src/tools
-$(WHY3WCCMO) $(WHY3WCCMX): INCLUDES += -I src/tools
-
-$(WHY3WCDEP): $(WHY3WCGENERATED)
-
-byte: bin/why3wc.byte
-opt:  bin/why3wc.opt
-
-bin/why3wc.opt: $(WHY3WCCMX)
-	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-
-bin/why3wc.byte: $(WHY3WCCMO)
-	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
-
-ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(WHY3WCDEP)
-endif
-
-depend: $(WHY3WCDEP)
-
-clean::
-	rm -f $(WHY3WCGENERATED)
-	rm -f src/tools/*.cm[iox] src/tools/*.o
-	rm -f src/tools/*.annot src/tools/*.dep src/tools/*~
-	rm -f bin/why3wc.byte bin/why3wc.opt bin/why3wc
-
-clean_old_install::
-	rm -f $(BINDIR)/why3wc$(EXE)
-
-install_no_local::
-	cp -f bin/why3wc.@OCAMLBEST@ $(TOOLDIR)/why3wc$(EXE)
-
-install_local:: bin/why3wc
-
 #########
 # why3doc
 #########
@@ -1383,11 +1316,8 @@ endif
 
 depend: $(WHY3DOCDEP)
 
-clean::
-	rm -f $(WHY3DOCGENERATED)
-	rm -f src/why3doc/*.cm[iox] src/why3doc/*.o
-	rm -f src/why3doc/*.annot src/why3doc/*.dep src/why3doc/*~
-	rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc
+CLEANDIRS += src/why3doc
+GENERATED += $(WHY3DOCGENERATED)
 
 clean_old_install::
 	rm -f $(BINDIR)/why3doc$(EXE)
@@ -1872,7 +1802,6 @@ src/util/config.ml share/Makefile.config: src/config.sh
 	    BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
 
 clean::
-	rm -f src/util/config.ml src/config.ml
 	rm -f share/Makefile.config
 
 doc/version.tex: doc/version.tex.in config.status
@@ -1903,6 +1832,11 @@ depend:
 	rm -f $^
 	$(MAKE) $^
 
+clean::
+	rm -f $(GENERATED)
+	$(foreach d,$(CLEANDIRS),rm -f $(addprefix $(d)/*.,$(COMPILED_LIB_EXTS));)
+	$(foreach p,$(CLEANLIBS),rm -f $(addprefix $(p).,$(COMPILED_LIB_EXTS));)
+
 ##################################################################
 # Building the Why3 platform with ocamlbuild (OCaml 3.10 needed) #
 ##################################################################