Fix the "dune coq top" bug identified by #5552

[rlepigre]

See #5552.

[rgrinberg]

side note: maybe you should just reject absolute paths? we don't allow dune build /foo/bar as far as I know. Why allow it here?

[rlepigre]

Yeah, I know that's a bit silly. The reason I did that originally is that emacs/proof-general feeds coqtop with an absolute path. But I'm not sure how important that is that we support that.

[rlepigre]

Should we also remove that @Alizter? I agree this is kind of useless anyway: editors will need to detect the workspace root anyway, so they can cook up a path relative to it.

[rgrinberg]

Could you also add a test of the form:

$ ls
dune-project theory/
theory/dune theory/foo.v
$ cd theory
$ dune coq top --root=.. -- foo.v

All dune commands work when you run them in sub-directories, so this should be no exception.

[rlepigre]

Could you also add a test of the form:

$ ls
dune-project theory/
theory/dune theory/foo.v
$ cd theory
$ dune coq top --root=.. -- foo.v

All dune commands work when you run them in sub-directories, so this should be no exception.

I added a test case, but this currently fails. I'm not sure what is the right way to fix things here. I should certainly reuse stuff from the dune build command, but I've not had much success yet. I tried playing with functions in bin/target.ml but I don't know what is the right thing to do here.

In particular, I'm not sure where the translation of paths should happen. It seem that all operations are expected to work with paths relative to the root, is that right? If yes, how do you typically construct such paths for a relative path to the current working directory?

[rgrinberg]

I tried playing with functions in bin/target.ml but I don't know what is the right thing to do here.

You're on the right track. In particular, see the epxand_path function. Note the Workspace_root.t needed to make the paths relative to the cwd. You only need this part:

  Path.relative Path.root (root.reach_from_root_prefix ^ s)

Where s is your argument to dune coq top.

[rlepigre]

You're on the right track. In particular, see the epxand_path function. Note the Workspace_root.t needed to make the paths relative to the cwd. You only need this part:

  Path.relative Path.root (root.reach_from_root_prefix ^ s)

Where s is your argument to dune coq top.

Thanks @rgrinberg! Unfortunately I don't quite understand how that helps. I think that what I need instead is a way to compute the relative path from the root (which seems to be the current working directory after initialisation, as returned by Path.External,cwd ()) to the initial working directory (given by Path.Externam.initial_cwd).

In the (failing) test, when I run the last command from the theories folder, the value of root is: {dir = ".."; to_cwd = []; reach_from_root_prefix = ""; _}, which I don't think is helpful. Am I missing something?

I could probably hack a fix by extracting the path I want somehow, but that would almost surely not be the correct approach. Could you elaborate a bit on what you think is the right way to fix the problem?

[Alizter]

LGTM @rlepigre I think DCO is complaining because you are not the author of the first commit? Otherwise I don't know why it doesn't like your sign off.

Once that is sorted @rgrinberg this is good to merge.

[Alizter]

I see that the extra test wasn't added, let me try to do that.

[rlepigre]

I see that the extra test wasn't added, let me try to do that.

I added the test, but it currently fails (the message in the test is wrong): see test/blackbox-tests/test-cases/coq/coqtop-root.t/run.t. However, I could not figure out how to solve the problem in a nice way.

[Alizter]

@rlepigre Could you push the broken test so I can take a look at it?

[rlepigre]

If you know a way to fix it @Alizter, feel free to implement it. Otherwise I can have a go if you tell me how to.

[rlepigre]

It is pushed, it is the second commit.

[Alizter]

OK so @rgrinberg thinks that Workspace_root has an incorrect implementation which is why the test doesn't work. I've filed that as an issue: #5899.

@rlepigre could you drop the second test, the fix for that will have to come later.

[rgrinberg]

Why should the fix come later? Resolving the argument with reach_from_root_prefix is still the right way to do it.

[Alizter]

Yes that's right, I will push my change.

[Alizter]

@rlepigre I don't have permission to push to you branch.

[rlepigre]

@rlepigre I don't have permission to push to you branch.

You should have received an invite.

[Alizter]

@rlepigre There is a checkbox in the bottom right hand side of this page which should give permission for pushing to this specific branch. I don't need full access to your repo. :-)

[rlepigre]

It was checked already, I guess you do not qualify as a "maintainer" @Alizter? 😛

[Alizter]

OK no problem :p @rlepigre I've opened a new PR so we can merge it quickly #5901

[rlepigre]

OK no problem :p @rlepigre I've opened a new PR so we can merge it quickly #5901

Great, thanks for taking care of this!