diff options
| author | Pierre Letouzey | 2016-06-07 16:03:50 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-06-08 14:37:36 +0200 |
| commit | 301ec42f1b38623df8f5de2cfb69da6836bd6e01 (patch) | |
| tree | 335352f69ea6624d996ff3ab1d5527378f65651b /Makefile | |
| parent | f2a2bf8322222ecc4a4b384a510ab00c377f6fb7 (diff) | |
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).
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -153,7 +153,7 @@ noconfig: # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles -Makefile Makefile.build Makefile.common config/Makefile : ; +Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### # Cleaning @@ -173,7 +173,7 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(FAKEIDE) + rm -f $(COQTOPBYTE) $(CHICKENBYTE) find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete rm -f */*.pp[iox] plugins/*/*.pp[iox] rm -rf $(SOURCEDOCDIR) @@ -206,8 +206,8 @@ archclean: clean-ide optclean voclean rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT) - rm -f $(TOOLS) $(CSDPCERT) + rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) + rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f clean-ide: |