Coq stanzas cannot be independent of `coq-stdlib`

[LasseBlaauwbroek]

This is a continuation of coq/coq#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 coq/coq#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.

[ejgallego]

Thanks for the summary @LasseBlaauwbroek , I'd be great to support tactician better in Dune, however I'm not sure that just setting the right flags is going to be enough.

To have a particular build setup working on dune it must be a) composable b) incremental .

a) means that we should be able to put tactician, Coq, and the stdlib into scope, and the build should work fine b) means that compilation rules must track every dependency properly, for example building the stdlib must be triggered when a tactician change would have it produce different object files.

Can you share a bit more what the inject setup does?

Something may worth doing is indeed adding a (stdlib no) field, which would add the right flags and could be useful for some more people.

[LasseBlaauwbroek]

Even though it would indeed be great to have composability support with Dune, I don't think that is realistic to achieve at the moment. Tactician has quite a complex setup, and being able to run a composable build and running things with dune exec is quite far away. Outside of the current issue, one problem I'm having is https://discuss.ocaml.org/t/make-a-binary-depend-on-non-code-files-in-dune/8994. And there are probably more.

Tactician is fairly non-standard, because it has to be injected into other pre-existing Coq packages in order to function. Behind-the-scenes, this means that flags must be added to coqc that load the Tactician plugin. For this, Tactician has a command tactician exec ... (modeled after dune exec and opam exec) that will use bwrap to inject these flags. Hence, you can run something like tactician exec make or tactician exec dune build to build a project with Tactician support. In addition there is tactician inject, which modifies the config of your Opam switch to automatically run any package installations within tactician exec. If you wanted to get a fully composable build, you would have to run something crazy like dune exec tactician exec dune build, which I'm quite sure does not currently work for a myriad of reasons...

I think that having (stdlib no) would already be a major improvement (together with Coq's package split). After that, I'd be happy to work towards a more composable build :-)

[LasseBlaauwbroek]

One additional reason why dune exec tactician exec dune build is currently somewhat problematic is because dune-inception is not really well-supported: https://github.com/ocaml/dune/issues/4630

[ejgallego]

Dune support instrumentation for example for the ppx_bisect plugin, so it wouldn't be too far-fetched to think that instrumentation could be used to support tactician. The key point is to see how the dependency DAG looks like.

Runtime deps for binaries have been a long discussion topic, and IMHO a feature worth implementing, but still some design work is needed. (A runtime dep is one that is only pulled for dune exec , not for dune build)

[LasseBlaauwbroek]

Yes, a way to get non-code deps would be great, and it would greatly improve my development experience. Dune's instrumentation feature also looks interesting, although it's currently not obvious to me why something like dune build --instrument-with tactician would be better than tactician exec dune build (which already works today and is universal with any build system, and you can even use it for editors like tactician exec coqide or tactician exec emacs).

In order to gradually improve support for Tactician, I would propose the following actions in order of importance:

• [ ] Support for (stdlib no), so that Tactician can depend on coq-core only.
• [ ] Adding support for non-code deps in exeuctables. This will hopefully allow building and running the tactician executable using dune exec tactician (although it would probably still not be able to do composable builds).
• [ ] Make Tactician composable with coq-core (this already kind of works modulo the previous two points; but I can already drop Tactician in the Coq repo with small modifications and build it's main theory files).
• [ ] Make Tactician composable with other Coq packages that need to be instrumented by making (something similar to) dune exec tactician exec dune build work.
• [ ] Integrate with Dunes instrumentation facilities.

[ejgallego]

Instrumentation in Dune doesn't change the build target, but adds some extra flags and registers maybe some extra targets. The advantage of having dune handle this is that you can let Dune track the dependencies of the metadata and instrumentation setup, so you get incremental builds.

[LasseBlaauwbroek]

Yes, that would indeed be a nice feature to have. Currently you have to be kind of careful to run dune clean when switching between tactician exec dune build and dune build...

Regarding step (1), adding in (stdlib no): Is there already a roadmap for this? How hard do you estimate this to be? I'd be happy to help, but unfortunately I'm not at all familiar with Dune's internals.

[ejgallego]

That'd be quite easy to do, I think; I'll be happy to guide you with it.

You want to modify src/dune_rules/coq_rules and coq_stanza

If the option is set, we basically setup the flags to add -boot, and if the stdlib is in scope, to ignore it as a dep.

(stdlib no) will be hopefully the default in the dune lang 1.1 for Coq.

[ejgallego]

@LasseBlaauwbroek , Ali and I tried to fix the composition bug in #6165 , it was a bit tricky, but indeed, we added the flag to the buildable as we were going along. I think you can rebase your PR on top of that one, and add the tests, the syntax extension, and the documentation, and let us know how it works.