Fix regression that caused dependency paths to point to .v files.
The dependency paths used to point to .bin files (as I remember it). But for
some reason a regression was introduced that caused them to point to installed
.v files and not the source .v files. This is an incompatible change, but a
necessary one.
Better rules for relativization of dependency paths in generated datasets.
We now proceed according to the following algorithm:
Determine the absolute path of the dependency on the machine it was generated
Determine the root as follows:
If the build is being initiated by Opam, and the working directory is inside
of Opams build area, we use Opam's build area as the root. This allows for
generating cross-project datasets.
Otherwise, we take the root to be the current working directory. This usually works
well when building projects manually, but will not allow for proper
cross-project dependencies.
Relativize the absolute paths w.r.t. the root
When the root is not an ancestor of the absolute path, we issue a warning.
This will happen when one build a project outside of Opam that has
dependencies on other projects (including the standard library).
We then include the full absolute path in the dataset. This means it will not be
relocatable but it may still be useful on the machine that generated it and
for quick debugging sessions.
A sanity check that the files in a dependency actually exist in dependencies (this check fails in current datasets).
Three changes (split into three commits):