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