Redirect (or Cd) should have an option/variant that computes paths relative to the directory of the .vo file

[JasonGross]

Version

8.8.1

Operating system

Linux

Description of the problem

Currently Redirect does not work with relative paths. If I do Redirect "foo" Check I. interactively, the file foo.out in the current directory gets written. However, if I put it in a .v file that is not at top-level, and invoke coqc on the .v file, it gets written to the current working directory. This makes Redirect effectively unusable in developments. I would like either an option or a variant of Redirect that takes the file path as relative to the location where the .vo file is being output. Alternatively (perhaps better), I'd like a command which is "cd to the directory where the .vo file is being output", or "cd to this directory relative to where the .vo file is being output".

See also #4953

[JasonGross]

(I am reporting this because I just ran into a case where Redirect "/tmp/foo" is unusable: if multiple users are building the same project on the same machine, it will give a "permission denied" error on trying to write to the file in /tmp.)

[andres-erbsen]

At least it seems to be possible to create per-user paths:

Welcome to Coq 8.8.2 (October 2018)

Coq < Cd "~".
/home/browse

I still think that Redirect does not really make sense of a vernac command (#4953) and I am guessing all use cases are (in the long run) better served by redirecting the output of coqc in Makefile (or improving the interaction protocol, as I think was the case with the original motivation for adding redirect).