Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install}

 General idea : Makefile.build was far too big to be easy to grasp or
 maintain, with information scattered everywhere. Let's try to tidy that!
 Normally, this commit is transparent for the user. We simply regroup
 some parts of Makefile.build in several new dedicated files:
  - Makefile.ide
  - Makefile.checker
  - Makefile.dev (for printers, revision, extra partial targets, otags)
  - Makefile.install
 These new files are "included" at the start of Makefile.build, to provide
 the same behavior as before, but with a Makefile.build shrinked by 50%
 (to approx 600 lines). Makefile.build now handles in priority the build
 of coqtop, minor tools, theories and plugins.

 Note: this is *not* a separate build system for coqchk nor coqide,
 even if this can be seen as a first step in this direction (won't be easy
 anyway to continue, due to the sharing of various stuff in lib and more).
 In particular Makefile.{coqchk,ide} may rely here and there on some generic
 rules left in Mafefile.build. Conversely, be sure to prefix rules in
 Makefile.{coqchk,ide} by checker/... or ide/... in order to avoid
 interferences with generic rules.

 Makefile.common is still there, but quite simplified. For instance,
 some variables that were used only once (e.g. lists of cmo files to link
 in the various tools) are now defined in Makefile.build, directly
 where they're needed. THEORIESVO and PLUGINSVO are made directly out of
 the theories/*/vo.itarget and plugins/*/vo.itarget files, no long manual
 list of subdirs anymore. Specific sub-targets such as 'reals' still
 exist, but in Makefile.dev, and they aren't mandatory.

 Makefile.doc is augmented by the rules building the documentation of
 the sources via ocamldoc.

 This classification attempt could probably be improved. For instance,
 the install rules for coqide are currently in Makefile.ide, but could
 also go in Makefile.install. Note that I've removed install-library-light
 which was broken anyway (arith isn't self-contained anymore).

1 files changed, 254 insertions, 0 deletions

diff --git a/Makefile.ide b/Makefile.ide
new file mode 100644
index 000000000..8d6b5de36
--- /dev/null
+++ b/Makefile.ide
@@ -0,0 +1,254 @@
+#######################################################################
+#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
+# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
+#   \VV/  #############################################################
+#    //   #      This file is distributed under the terms of the      #
+#         #       GNU Lesser General Public License Version 2.1       #
+#######################################################################
+
+## Makefile rules for building the CoqIDE interface
+
+## NB: For the moment, the build system of CoqIDE is part of
+## the one of Coq. In particular, this Makefile.ide is included in
+## Makefile.build. Please ensure that the rules define here are
+## indeed specific to files of the form ide/*
+
+## Coqide-related variables set by ./configure in config/Makefile
+
+#COQIDEINCLUDES : something like -I +lablgtk2
+#HASCOQIDE : opt / byte / no
+#IDEFLAGS : some extra cma, for instance
+#IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o
+#IDECDEPS
+#IDECDEPSFLAGS
+#IDEINT : X11 / QUARTZ / WIN32
+
+## CoqIDE Executable
+
+COQIDEBYTE:=bin/coqide.byte$(EXE)
+COQIDE:=bin/coqide$(EXE)
+COQIDEAPP:=bin/CoqIDE_$(VERSION).app
+COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
+
+## CoqIDE source directory and files
+
+# Note : for just building bin/coqide, we could only consider
+# config, lib, ide and ide/utils. But the coqidetop plugin (the
+# one that will be loaded by coqtop -ideslave) refers to some
+# core modules of coq, for instance printing/*.
+
+IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
+
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
+
+IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo
+IDECMA:=ide/ide.cma
+IDETOPLOOPCMA=ide/coqidetop.cma
+
+LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
+
+IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
+
+## GTK for Coqide MacOS bundle
+
+GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share
+GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
+GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
+
+
+###########################################################################
+# CoqIde special targets
+###########################################################################
+
+.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
+
+# target to build CoqIde
+coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
+
+coqide-binaries: coqide-$(HASCOQIDE) ide-toploop
+coqide-no:
+coqide-byte: $(COQIDEBYTE) $(COQIDE)
+coqide-opt:  $(COQIDEBYTE) $(COQIDE)
+coqide-files: $(IDEFILES)
+ifeq ($(BEST),opt)
+ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
+else
+ide-toploop: $(IDETOPLOOPCMA)
+endif
+
+ifeq ($(HASCOQIDE),opt)
+$(COQIDE): $(LINKIDEOPT)
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \
+		lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^
+	$(STRIP) $@
+else
+$(COQIDE): $(COQIDEBYTE)
+	cp $< $@
+endif
+
+$(COQIDEBYTE): $(LINKIDE)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
+	        lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+
+ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
+	$(SHOW)'CAMLP4O   $<'
+	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@
+
+
+ide/%.cmi: ide/%.mli
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+
+ide/%.cmo: ide/%.ml
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+
+ide/%.cmx: ide/%.ml
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $<
+
+
+####################
+## Install targets
+####################
+
+.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
+
+ifeq ($(HASCOQIDE),no)
+install-coqide: install-ide-toploop
+else
+install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
+endif
+
+install-ide-bin:
+	$(MKDIR) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
+
+install-ide-toploop:
+	$(MKDIR) $(FULLCOQLIB)/toploop
+	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
+ifeq ($(BEST),opt)
+	$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
+endif
+
+install-ide-devfiles:
+	$(MKDIR) $(FULLCOQLIB)
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
+	  $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
+ifeq ($(BEST),opt)
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)
+endif
+
+install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time
+	$(MKDIR) $(FULLDATADIR)
+	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR)
+	$(MKDIR) $(FULLCONFIGDIR)
+	if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
+
+install-ide-info:
+	$(MKDIR) $(FULLDOCDIR)
+	$(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
+
+###########################################################################
+# CoqIde MacOS special targets
+###########################################################################
+
+.PHONY: $(COQIDEAPP)/Contents
+
+$(COQIDEAPP)/Contents:
+	rm -rdf $@
+	$(MKDIR) $@
+	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist
+	$(MKDIR) "$@/MacOS"
+
+$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
+		unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \
+		threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^
+	$(STRIP) $@
+
+$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
+	$(MKDIR) $@/coq/
+	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/
+	$(MKDIR) $@/gtksourceview-2.0/{language-specs,styles}
+	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
+	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
+	cp -R "$(GTKSHARE)/"locale $@
+	cp -R "$(GTKSHARE)/"icons $@
+	cp -R "$(GTKSHARE)/"themes $@
+
+$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents
+	$(MKDIR) $@
+	$(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@
+
+$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents
+	$(MKDIR) $@
+	$(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@
+
+
+$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
+	$(MKDIR) $@/xdg/coq
+	$(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys
+	$(MKDIR) $@/gtk-2.0
+	{ "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
+	 sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \
+	> $@/gtk-2.0/gdk-pixbuf.loaders
+	{ "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\
+	 sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\
+	 sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \
+	> $@/gtk-2.0/gtk-immodules.loaders
+	$(MKDIR) $@/pango
+	echo "[Pango]" > $@/pango/pangorc
+
+$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP)
+	$(MKDIR) $@
+	$(INSTALLLIB) $(GTKLIBS)/charset.alias $@/
+	$(MKDIR) $@/pango/1.8.0/modules
+	$(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/
+	{ "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\
+	 sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \
+	> $@/pango/1.8.0/modules.cache
+
+	for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
+	    do cp $$i $@/; \
+	    ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \
+	done
+	for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \
+	    do \
+		for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
+		do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
+		ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \
+	    done
+	EXTRAWORK=1; \
+	while [ $${EXTRAWORK} -eq 1 ]; \
+	do EXTRAWORK=0; \
+	    for i in $@/*.dylib; \
+	    do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
+		do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
+	    done; \
+	done
+	ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@
+
+$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share
+	$(INSTALLLIB) ide/MacOS/*.icns $@
+
+$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
+	$(CODESIGN) $@
+
+###########################################################################
+# CoqIde for Windows special targets
+###########################################################################
+
+%.o: %.rc
+	$(SHOW)'WINDRES    $<'
+	$(HIDE)i686-w64-mingw32-windres -i $< -o $@
+
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End: