This is a continuation of rocq-prover/rocq#16510. Since Coq 8.17, Coq has been split into coq-core and coq-stdlib. It is now possible for Coq developments and plugins to only depend on coq-core. However, Dune does not properly support this yet.

To see this, have a Coq file with only Declare ML Module "coq-core.plugins.ltac". in it. This file does not depend on things in coq-stdlib but it does depend on the Ltac library in coq-core. Then try to compile it with a stanza like this:

(coq.theory
 (name Test)
 (package test)
 (flags -noinit -boot)
)

This errors out with cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used. because coqdep is not passed the -boot flag. Adding (boot) does not help either: Error: No rule found for theories/Init/Prelude.vo.
It seems to me that

1. -boot should be passed to coqdep when it is passed as a flag.
2. When (boot) and -noinit -boot is specified, Dune should not go looking for theories/Init/Prelude.vo.
   Alternatively, like @ejgallego suggested, a special (stdlib no) syntax could be introduced.

A concrete package that demonstrates this can be found here: https://github.com/coq-tactician/coq-tactician/tree/coqdev This development currently only compiles when full Coq is installed but errors out when only coq-core is installed.

To answer some questions of @ejgallego in rocq-prover/rocq#16510:

How does tactician work before the stdlib? Does the stdlib still needs to be compiled after it?

Tactician first compiles its own code that only depends on coq-core. Then, it can be injected into Opam's package installation process with tactician inject (which performs some clever tricks with bwrap). At that point coq-stdlib can be installed with support for Tactician using opam install coq-stdlib. Before the split, there was a special package coq-tactician-stdlib that would recompile and overwrite the stdlib because there was a chicken-and-the-egg problem between installing Tactician and Coq.