[coq top] Test case for problems with path / dir computation in dune …

[ejgallego]

…coq top

After some more testing, I have found problems finding the directory /
file for dune coq top:

        let coq_file_build =
          let p = Common.prefix_target common coq_file_arg in
          Path.Build.relative context.build_dir p
        in
        let dir =
          let dir = Filename.dirname coq_file_arg in
          let p = Common.prefix_target common dir in
          Path.Build.relative context.build_dir p
        in

dune coq top will also fail on project that have a theories/a/b.v
layout, such as in Coq for example, when doing:

dune coq top theories/Reals/Real.v

in the above snippet, dir is set to theories/Reals which is
incorrect, as it should be the root of where the stanza is placed.

This makes dune fail with:

Error: No rule found for theories/Reals/Reals/Reals.v.d

as dir is set incorrectly.

We need to think more about this, and fix it because it is currently
only usable on flat layouts.

Let's discuss in this PR cc @rlepigre

[rlepigre]

Damn, I thought I tested something like that...

Not sure what the best fix is: we seem to need the directory quite early on, though I don't completely understand what is the role of all the ~dir arguments that are passed throughout the code. I often wondered whether I was making the right choice when coming up with the code, but I could find no hint as to what the expected directory is. Is it always the case that it is the directory containing the dune file defining the stanza of interest?

If that is the case, maybe we should extend the exploration of the workspace to build a map from directories to "stanza root" directories, if no such thing already exists?

[ejgallego]

@rlepigre indeed that part is tricky, but indeed I think we have all we need in hand, I need to think more about it, but it seems to me that we should:

• Build the dune db, stanza scanning, etc...
• Use the reverse map to locate the stanza
• Use the stanza base dir as dir

This is what code in coq_rules.ml expects today, and I think would actually be cleaner! Note that the fact that coq_rules expects dir to be like that, doesn't mean it has to be that way.

I picked that particular logic as it was natural to me that for example, for a project with theories/dune, we do (cd theories && coqc foo/bar/m.v) instead of (cd theories/foo/bar/m.v && coqc ... but YMMV.

Don't worry too much about it, I can take care of the fix, should be a very small patch (I just read your mail)

[ejgallego]

And yes, we need to document dir and other parameters much better!

The thing is that coq_rules was the first implementation of (include_subdirs qualified) so we didn't know too well what we were doing.

[ejgallego]

Note that dune build foo/bar/foo.v does already properly locate the right path for the target, so I'd be surprised if we can't just follow what dune build does, then just use the reverse map.

[ejgallego]

In particular, Targets.interpret_targets is the function that takes care of understanding the filename argument to dune build

[rgrinberg]

Replaced by @rlepigre's PR