Allow "dune coq top" to step through unsaved files

[rlepigre]

Desired Behavior

(This is a follow up to #7355, which was not completely addressed.)

If a file file.v that has not yet be written to disk would be part of a coq.theory stanza, then dune coq top file.v should not fail, and allow you to step through the file.

Current behavior

The command currently fails with Error: Cannot find file: file.v.

[rlepigre]

Note that a workaround is to write an empty file to disk, and to immediately deleted after the toplevel has been started. However, that is a bit annoying to do, and I think it would be easy to find the relevant stanza, and extend the list of source files with the one given as argument (or something like that).

[ejgallego]

It is actually a bit tricky to implement this properly, imagine the following dune setup:

(coq.theory
  (name A)
  (modules a))

(coq.theory
  (name B)
  (modules b))

So in this case we won't be able to find a file. If we update B theory to say (modules :standard \ a) for example, then we could indeed inject the file in the :standard substitution, but that may be tricky code-wise, as dune may assume that every file we inject into the virtual file system may need to actually have an associate way to build it.

[rlepigre]

I see, you're right that it is non-trivial, at least in complicated setups. Maybe we should only support this if there is a single coq.theory stanza with (modules :standard)? I think that should take care of 99% of the pain some people have, and we could give an error saying that the stanza for the input file cannot be determined unambiguously otherwise.

[Alizter]

That sounds like a reasonable solution to me.

[ejgallego]

see, you're right that it is non-trivial, at least in complicated setups. Maybe we should only support this if there is a single coq.theory stanza with (modules :standard)? I think that should take care of 99% of the pain some people have, and we could give an error saying that the stanza for the input file cannot be determined unambiguously otherwise.

I'm afraid that the code to do that could be even more complex than just injecting a file in the filesystem, which happens at an earlier phase (VFS build).

There is a little bit of a hack that maybe could work without too much effort: if the file doesn't exist, create it, then just run dune.

You could do that in the code for dune coq top or just as a shell script wrapper to that command, that touches the file before calling dune.

[rlepigre]

There is a little bit of a hack that maybe could work without too much effort: if the file doesn't exist, create it, then just run dune.

That's exactly what some of us have been doing, but I was hoping to move towards not having to hack around problems with a wrapper script. 😄

[Alizter]

Coming back to this, is the suggestion for dune coq top to create the file if it doesn't exist?

[rlepigre]

Coming back to this, is the suggestion for dune coq top to create the file if it doesn't exist?

I think that is one possibility, yes.

[Alizter]

I'm a bit weary of doing something like that in case we have something like dune coq top typo.v where the user may have intended typ.v. On the other hand, a --create-missing argument might be a good compromise.

[rlepigre]

Yeah, I'm actually not entirely sold on the idea either. Maybe this whole use-case does not really matter, and the user can just save their file before running the top-level.

[ejgallego]

Indeed it seems to me that Dune requires the file to be present in the filesystem; I'm not sure it would work fine, but we could do as Ali proposes just having dune coq top create a rule for new_file.v, with empty contents, if the file doesn't exists.

It seems to me that guarding this with a command line option could be a good idea so dune coq top foo.v fails by default if the file is not there.