[meta] [coq] Support for installed theories coordination issue.

[ejgallego]

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: #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: coq/coq#16091 )

[Alizter]

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.

I don't understand how this would work.

[ejgallego]

I don't understand how this would work.

What it is what you don't understand, the idea is:

• if coqc is installed, then we query it and get the location of user-contrib and stdlib, and build installed_libs
• if coqc is not installed, then we do nothing, installed_libs = empty.

[Alizter]

@ejgallego yes but how do we query coqc without the super context?

[ejgallego]

The same way ocamlc is located, we don't query Dune, but search for path I guess.

[Alizter]

@rgrinberg what is a sensible way to call coqc --config without being able to resolve coqc from the super context?

[rgrinberg]

Using Context.which. The super context is only needed if you want to mind env when resolving the binary.