| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot
for porting this chapter.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
|
|
|
|
The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).
This commit adds the infrastructure but no content.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This completes the work of
b60906cc3ee3f994babf9cceff2971bd03485f2f
|
|
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
|
repository. Also removing FAQ-related build rules.
|
|
|
|
|
|
Since 8995d0857277019b54c24672439d3e19b2fcb5af [make doc] puts css
files in subdirectories of doc/refman/html. These subdirectories cause
a failure when doing [install doc/refman/html/* target].
|
|
linking chain.
|
|
Work done by Assia Mahboubi and Enrico Tassi
|
|
We make it so that, by default, the HTML reference manual looks
like the one published online (same .css) and we provide a target
to serve it locally (requires python).
|
|
|
|
|
|
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
|
Make does not allow for rules that produce multiple outputs (unless they
are pattern rules). As a consequence, the hacha rule could be run several
times concurrently, thus causing doc/refman/html to be deleted under the
feet of some runs.
This commit fixes the issue by turning the rule into a single-output rule
and adding a dummy rule to handle all the other indexes. Note that this is
not a perfect solution since, if the user were to manually delete one of
the auxiliary index, it would not be rebuilt until the main index is.
|
|
|
|
For some reason, with my version of transfig (which seems to be the latest),
the order of arguments of the fig2dev command matters: -L png must come
before -m 2. I suppose that this fix shouldn't break things for others.
|
|
Now, only 'phony' targets could be declared just via dependencies.
For 'real-file' targets such as doc/refman/html/index.html, there
should be a concrete production rule.
|
|
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).
|
|
|
|
|
|
|
|
documentation)
This commit r14895 comes apparently itself from commit r12010 in branch v8.2
|
