I'm opening this issue to summarize discussions with Ali and Rudi about the main missing piece for the 1.0 Coq Theory support (cc: rocq-prover/rocq#1998) which is detection of installed theories.

As of today, Coq uses a very simple install layout where a theory Foo.Bar is installed under $lib/coq/user-contrib/Foo/Bar; this is a model we want to move away from, but for 1.0 we need compatiblity both ways: Coq theories using coq_makefile need to be able to use dune-based theories, and viceversa.

The idea for the first prototype is to generate a theory for each (sub)-directory found in user-contrib, thus, if we have:

user-contrib/mc
user-contrib/mc/alg
user-contrib/mc/ssr

we generate 3 theories, and users can refer to any of the three.

Then, coqc is always called with -boot -R Coq $lib/coq/theories -Q mc.alg $lib/user-contrib/mc/alg for example. -boot is essential.

This scheme has a great advantage, in the sense that it makes -boot the default for Dune rules, and will simplify a lot of code.

I think we should also require users to depend on Coq explicitly, that is to say, the standard library, and deprecate the (stdlib ) theory flag.

We can see two technical challenges:

• scanning $lib/user-contrib may be expensive; but I'd suggest to do a first eager implementation before going to a lazy scan, which I think is possible
• the installed_theories DB needs to call coqc to find out the location of $lib/coq at scope creation time; this is tricky as we can't resolve the binary fully yet. However, I think that is not a problem, because in the case coq itself is in the workspace scope (and thus we can't resolve it), the set of installed_libs should be empty.

Another flag I'd add to this first prototype is implicit_stdlib, which would allow users to select -Q or -R for the Coq namespace, in preparation for making -Q the default upstream (cc: rocq-prover/rocq#20073 )