| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
As reported by PMP, this was not yet the case. The culprit
was the build of coqdep_boot by a one-liner ocamlopt taking all
the necessary .ml files as arguments (in the right order). This
was nice and short, and correct wrt dependencies, but had the
inconvenient of building some .cmi *after* their corresponding
.cmx, while the rest of the Makefile relies on the reverse order
(see the section about MLWITHOUTMLI). Hence on the next run,
make was thinking that these .cmx weren't up-to-date.
For solving this issue, we now build coqdep_boot (and other tools)
via a list of .cmx and let our infractructure build them (after
their .cmi). The only drawback is the 6 extra lines to hardcode
the dependencies of the *.cm(o|i|x) needed for coqdep_boot.
(since the .ml.d aren't already taken in account by make at that
time).
|
|
|
|
Earlier (as in #4812), a target with some declared dependencies (e.g.
in a .d) but no building rule would lead to a successful build,
even though it is actually incomplete.
Side effect: it is now mandatory to declare phony targets in a
.PHONY statement.
|
|
Restore the .cmxa-->.cmxs rule from the Makefile. Sorry, I was thinking
that all plugins would now be built from .mlpack (hence using only the
.cmx-->.cmxs rule), and I forgot about this coqidetop business.
Now the really intersting question is : why on earth 'make world' was
silently failing to build this file but succeeding nonetheless ?!
|
|
For now, the pack name reuse the previous .cma name of the plugin,
(extraction_plugin, etc).
The earlier .mllib files in plugins are now named .mlpack.
They are also handled by bin/ocamllibdep, just as .mllib.
We've slightly modified ocamllibdep to help setting the -for-pack
options: in *.mlpack.d files, there are some extra variables such as
foo/bar_FORPACK := -for-pack Baz
when foo/bar.ml is mentioned in baz.mlpack.
When a plugin is calling a function from another plugin, the name
need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz).
Btw, we discard the generated files plugins/*/*_mod.ml, they are
obsolete now, replaced by DECLARE PLUGIN.
Nota: there's a potential problem in the micromega directory,
some .ml files are linked both in micromega_plugin and in csdpcert.
And we now compile these files with a -for-pack, even if they are
not packed in the case of csdpcert. In practice, csdpcert seems
to work well, but we should verify with OCaml experts.
|
|
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).
|
|
|
|
|
|
This makes the core free from particular protocol choices.
It should help with the ppx serialization project and shrinks clib.cma a
bit.
|
|
|
|
- the particlar rule for dev/printers.cma is adapted as for %.cma:%.mllib
- some more removal of | .d in rules
|
|
We add a dependency of .cma over .mllib.
This dependency over the .mllib is somewhat artificial, since
ocamlc -a won't use this file, hence the $(filter-out ...) below.
But this ensures that the .cm(x)a is rebuilt when needed,
(especially when removing a module in the .mllib).
We also remove all "order-only" dependencies over *.d in rules,
since the -include mechanism should already ensure that we have
up-to-date dependencies known by make.
|
|
There were a forgotten CAMLP4DEPS macro.
We also avoid otags failure with camlp5 (in this case, it only
builds the tags of regular .ml files, not .ml4).
|
|
We're back to a unique build phase (as before e372b72), but without
relying on the awkward include-deps-failed-lets-retry feature of make.
Since PMP has made grammar/ self-contained, we could now build
grammar.cma in a rather straightforward way, no need for
a specific sub-call to $(MAKE) for that. The dependencies between
files of grammar/ are stated explicitely, since .d files aren't
fully available initially.
Some Makefile simplifications, for instance remove the CAMLP4DEPS
shell horror. Instead, we generalize the use of two different
filename extensions :
- a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
- a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
except coqide_main.ml4 and its specific rule
Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
.ml4 dichotomy)
|
|
Coqdep_boot has almost no dependencies, and hence can be compiled
very early during the build, without relying on .ml.d files.
Some code of system.ml is now in a separate file minisys.ml,
which is also included in system.ml for compatibility.
|
|
This reverts commit c2249c3b4c3387a3c8510e68fc447274d7299695.
|
|
This reverts commit 973b6c69f0861c113f7bd5b94604d2497520a334.
|
|
This reverts commit 5e9b37a815795efaafd64ab8fe19bf8560d70203.
|
|
This reverts commit d28c1d7d908fe9d5fc719d58433a6b87c12390ba.
|
|
This reverts commit 67335c832a55cbd0ca559906bbe1af2485241353.
|
|
This reverts commit 1171590c544492842a848c6765b61c70fca19a01.
|
|
|
|
|
|
beautification of the standard library.
Currently not intrusive but needs two extra phases of compilation.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
|
|
|
|
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
|
|
Conflicts:
lib/cSig.mli
|
|
Linking a module twice is unsafe and warning 31 will be fatal by default in
OCaml 4.03. See PR#5461.
|
|
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
|
|
|
|
"dev/printers.cma" to be loadable within "ocamldebug".
|
|
|
|
characters.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
