Share flags config by generating _CoqProject

[rlepigre-skylabs-ai]

This centralizes the configuration of flags to a file theories/rocq-flags.conf, used by dune and by a generation script for theories/_CoqProject. I'm thinking of later using the same script for adapting the generation of theories/_CoqProject to the new package management support when the Rocq version supports it.

[rlepigre-skylabs-ai]

This enables the flag for all profiles instead of just the dev profile, but I guess that's fine right?

[proux01]

Couldn't we rather generate the dune thing out of _CoqProject? (it's just a matter of extracting the -arg ... lines) We have to keep it anyway for editor support.

[rlepigre-skylabs-ai]

My thinking is that we will need to generate the _CoqProject file anyway if we want to support versions of Rocq that have the new -package support and versions that don't have it.

Basically, the _CoqProjects would need to be modified as follows for package support.

diff --git a/theories/_CoqProject b/theories/_CoqProject
index b34d8dd88a..cc961853c7 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -1,3 +1,7 @@
+--rocq-package rocq-stdlib
+-package rocq-core
+--legacy-support
+--description "Rocq standard library"
 -R . Stdlib
 # When editing below lines, keep the theories/dune file in sync
 # to handle when requiring Rocq >= 9.2

(Possibly also adding -boot.)

[proux01]

Let's just wait (about six months) until we require Rocq >= 9.3. This kind of configuration finicking is a real pain. Maybe things can be done better in the dune config but let's not pile hacks in the rocq makefile one just to save a few months.

[rlepigre-skylabs-ai]

Let's just wait (about six months) until we require Rocq >= 9.3. This kind of configuration finicking is a real pain. Maybe things can be done better in the dune config but let's not pile hacks in the rocq makefile one just to save a few months.

OK, up to you.

Note however that this basically means that the development of the new packaging system will be stuck for packages depending on rocq-stdlib (so, basically all packages), as in principle all transitive deps of a package need to be ported before the package can itself be ported. (Doing otherwise is possible, by also giving access to user-contrib, but this defies the point of the better packaging mechanism.) My personal opinion is that the Rocq ecosystem cannot afford to wait that long, since there might well be issues to be discovered during the transition process.

Another way to address this would be to add hacks to the install target so that it also installs following the new installation layout, but I don't know that you'd like that any more than the current PR. 😄

[rlepigre-skylabs-ai]

As a reference, not that rocq-stdpp and rocq-iris already use a similar setup as the one proposed in this PR. Another reason why such a setup is useful is for editor support when building with dune, since a different _CoqProject / _RocqProject is required. I believe that we currently rely on editors first trying _RocqProject before _CoqProject, which seems fragile.

[proux01]

Yes, hacking the Makefile.coq target of the Makefile with something like

rocq makefile <new_option> || rocq makefile  # remove second branch and put option in _CoqProjet when requiring Rocq >= 9.3

would probably be fine but please just don't hack the _CoqProject itself.

[rlepigre-skylabs-ai]

Closing in favour of #286.

[proux01]

BTW, I do agree on the fact that the duplication of config flags between the _CoqProject and dune files is bad. I guess dune should have a way to either read _CoqProject or at least generate it.

[rlepigre-skylabs-ai]

BTW, I do agree on the fact that the duplication of config flags between the _CoqProject and dune files is bad. I guess dune should have a way to either read _CoqProject or at least generate it.

Dune does generate _RocqProject files for editors when (generate_project_file) is used, which is the case in rocq-stdlib if I'm not mistaken, but the contents of this file depends on what packages are in the workspace. In particular, several Rocq packages depending on each-other are in the same dune workspace, the _RocqProject files contain -Q flags for all the transitive dependencies found in the workspace.

[proux01]

damn, one more feature that will take a while before it becomes usable :(

[rlepigre-skylabs-ai]

damn, one more feature that will take a while before it becomes usable :(

What do you mean? We've been using that feature for a while now, and it seems to work pretty well. It's a good alternative to dune rocq top since most editors never added support for it.

[proux01]

I mean until we can safely drop _CoqProject and use _RocqProjecgt (not sure what's the status of the various editors there)

[SkySkimmer]

The generated rocqproject is for editors not for rocq makefile so IDK how useful it is for deduplication

[rlepigre-skylabs-ai]

I mean until we can safely drop _CoqProject and use _RocqProjecgt (not sure what's the status of the various editors there)

Pretty much all editors support _RocqProject these days I believe.