Option to make "dune coq top" more permissive

[rlepigre]

Desired Behavior

Currently, running dune coq top on a Coq file starts by ensuring that all dependencies of that file are built and up-to-date, which in turn require that the file itself is part of a stanza (so, saved to disk) and that it can be parsed by coqdep.

This disturbs some people's workflow when writing Coq, as they often want to edit files more quickly without constantly recompiling deps even if they are not completely consistent, work on dirty files only a prefix of which is syntactically correct, or work on new files that have not been saved yet.

I feel like we could have an opt-in option to dune coq top to support such use-cases. In particular, it would do no building of dependencies and rely on the user having called, e.g., dune build to get the dependencies in a reasonable state. Of course, to achieve this, one needs to figure out what options to pass to coqtop. One possibility (that was suggested by a colleague of mine) would be to compute a "most general configuration" from the workspace, that would put all theories and all plugins in scope.

CC @Alizter @ejgallego

Example

[Alizter]

There is an analogous option for dune exec:

       --no-build
           don't rebuild target before executing

Since we will be doing no building, we could also make sure that it doesn't possess the workspace lock allowing dune build and dune coq top to be run in tandem.

[rlepigre]

@Alizter I think this issue is a real blocker for people fully moving to using dune for Coq project, so perhaps we should try to implement this sooner rather than later?

I'm happy to do some hacking on this, but it would be good to try an come up with some kind of plan first.

[Alizter]

@rlepigre I'll have a look today.

[ejgallego]

I guess this is usually implemented by replacing Dep.path with Dep.goal (which ensures that the file is present, but doesn't depend on their checksums.

I think tho in general this is a misfeature. While I'm happy if you folks want to add this, I'm convinced that having to use this flag is just a way to mask deeper issues in the toolchain.

This disturbs some people's workflow when writing Coq, as they often want to edit files more quickly without constantly recompiling deps even if they are not completely consistent

When a dep of a Coq file changes, there are two cases: the change is relevant for your edit, or it is not. In the first case you would be wasting your time by skipping to build the dependency, in the second, a proper incremental compiler like coq-lsp will be one day would just not block your edit while it rebuilds the dep.

I'm willing to bet that the cognitive overhead of the dev having to think about --no-rebuild is already a greater burden than just having to recompile sometimes.

Tho I agree that editors should allow you to edit while the stuff is compiling.

coq-lsp has the right infra to delay stuff, so for example you can work on your file and not check proofs, I've just realized that this also works for Require.

What do I mean:

From Foo Require Bar.

Lemma too : Type. .... Qed.

As of coq-lsp 0.2.x , coq-lsp will delay the checking of too until Bar is ready. But actually we should indeed handle the Require effect different, which is to actually go ahead and check too, while we launch the build of Bar in the background.

Once Bar is built, we compare with the previous version and we decide if we need to re-run too.

work on dirty files only a prefix of which is syntactically correct

What does this mean? Do you mean that you would like to have a .vo even if the file is not fully compilable?

coq-lsp already generates .vo like this, hopefully coqc too soon.

or work on new files that have not been saved yet.

That's needed yes.

[rlepigre]

I think tho in general this is a misfeature. While I'm happy if you folks want to add this, I'm convinced that having to use this flag is just a way to mask deeper issues in the toolchain.

That's kind of true, but the fact is that today one still needs to maintain a _CoqProject file by hand for standard editors to properly work with dune projects, and that's a real pain. This becomes especially true when you have plugins that are loaded with the findlib method, in which case it even becomes not possible to make it work just with a _CoqProject file since -I options for plugin directories under _build/default are not enough (you can still pull it of by calling dune build @install for the plugins, and exporting an OCAMLPATH with the _build/install/default/lib directory in it, but that's terrible since you need to remember to call dune build @install again whenever you modify plugins, and if you forget you're suddenly using an older version of the plugins).

Being more flexible with dune coq top would give us a not-so-terrible way to completely get rid of _CoqProject files in dune projects (provided support for dune coq top in editors, which we have hacks for), and that's already a big win.

work on dirty files only a prefix of which is syntactically correct

What does this mean? Do you mean that you would like to have a .vo even if the file is not fully compilable?

No, I mean that when you (maybe by accident) saved your working file to disk, and re-run dune coq top, then coqdep on the file will fail due to syntax errors, and you'll never get your toplevel.

[ejgallego]

That's kind of true, but the fact is that today one still needs to maintain a _CoqProject file by hand for standard editors to properly work with dune projects, and that's a real pain. This becomes especially true when you have plugins that are loaded with the findlib method, in which case it even becomes not possible to make it work just with a _CoqProject file since -I options for plugin directories under _build/default are not enough (you can still pull it of by calling dune build @install for the plugins, and exporting an OCAMLPATH with the _build/install/default/lib directory in it, but that's terrible since you need to remember to call dune build @install again whenever you modify plugins, and if you forget you're suddenly using an older version of the plugins).

Umm, once we fix the coqdep bug that should work tho right? Because coqdep will correctly emit the dependency on the plugin in _build/install, or am I missing something?

Being more flexible with dune coq top would give us a not-so-terrible way to completely get rid of _CoqProject files in dune projects (provided support for dune coq top in editors, which we have hacks for), and that's already a big win.

Yes, that's a big win, however the above concern seems unrelated to the --no-build flag, right?

work on dirty files only a prefix of which is syntactically correct

What does this mean? Do you mean that you would like to have a .vo even if the file is not fully compilable?

No, I mean that when you (maybe by accident) saved your working file to disk, and re-run dune coq top, then coqdep on the file will fail due to syntax errors, and you'll never get your toplevel.

Ah, very interesting thanks! Good to know for coq-lsp (where running coqdep is optional)

[Alizter]

I've made a draft implementing a --no-build option. Please test it. I will write some cram tests later.

• dune coq top: add --no-build option to avoid building dependencies #7380

[rlepigre]

Umm, once we fix the coqdep bug that should work tho right? Because coqdep will correctly emit the dependency on the plugin in _build/install, or am I missing something?

The coqdep bug is part of the issue, but I actually circumvent it by using a wrapper script that fixes the paths. The actual issue is that I don't really know what to write in a _CoqProject file to make editors happy. It seems that I need one META file per plugin, while dune generates a single META file for all plugins in the package (not sure if that is the actual problem though). Also, since the META file is in _build/install and the other files are in _build/default, I need to force the generation of the whole "installed" version of plugins under _build/install to make it so that everything is in one place and I can extend OCAMLPATH.