WIP: adding package management infrastructure

[rlepigre-skylabs-ai]

This PR is an attempt at the first necessary steps to implement rocq-prover/rfcs#101, whose aim is to add proper package management to Rocq (piggy-backing on findlib). This was discussed in this week's Rocq Call.

Current state

In the current version, the following two changes are done:

• The rocq dep command is extended with a -package <pkg> argument (similar to that of ocamlfind).
• A rocqfind tool is added: given a list of package names, it returns the necessary -Q / -I options to use them.

Both seem to work as I expect them to, at least on the small-ish tests I ran.

More work is obviously needed, for instance adding a similar -package option to other commands, but argument handling is not fully shared between commands (rocqchk, rocq doc, ...) if I understand correctly, so I'd prefer to agree on some kind of plan (maybe involving refactoring) before doing changes in several places.

Testing done

My testing setup was constructed as follows:

dune build
mkdir -p fake-lib-dir/rocq-core/ltac2
cp -r _build/install/default/lib/coq/theories other-fake-lib-dir/rocq-core/rocq.d
cp -r _build/install/default/lib/coq/user-contrib/Ltac2 other-fake-lib-dir/rocq-core/ltac2/rocq.d

And writing the following to file fake-lib-dir/rocq-core/META.

version = "dev"
description = "The Rocq Prover's prelude."
rocqpath = "Corelib"
requires = "rocq-runtime.plugins.ltac"
requires += "rocq-runtime.plugins.tauto"
requires += "rocq-runtime.plugins.cc"
requires += "rocq-runtime.plugins.firstorder"
requires += "rocq-runtime.plugins.number_string_notation"
requires += "rocq-runtime.plugins.btauto"
requires += "rocq-runtime.plugins.rtauto"
requires += "rocq-runtime.plugins.ring"
requires += "rocq-runtime.plugins.nsatz"
requires += "rocq-runtime.plugins.zify"
requires += "rocq-runtime.plugins.micromega"
requires += "rocq-runtime.plugins.funind"
requires += "rocq-runtime.plugins.ssreflect"
requires += "rocq-runtime.plugins.derive"

package "ltac2" (
  directory = "ltac2"
  version = "dev"
  description = "The Rocq Prover's Ltac2 standard library."
  rocqpath = "Ltac2"
  requires = "rocq-core"
  requires += "rocq-runtime.plugins.ltac2_ltac1"
  requires += "rocq-runtime.plugins.ltac2"
)

With this setup, I could then for example run:

$ OCAMLPATH=fake-lib-dir:_build/install/default/lib _build/install/default/bin/rocqfind -I -Q rocq-core.ltac2
-I '_build/install/default/lib/rocq-runtime'
-Q 'fake-lib-dir/rocq-core/rocq.d' Corelib
-Q 'fake-lib-dir/rocq-core/ltac2/rocq.d' Ltac2

I also tested the rocq dep by writing the following to file test.v:

Require Import Corelib.Init.Prelude.
Require Import Ltac2.Ltac2.

And the running the following command.

$ OCAMLPATH=fake-lib-dir:_build/install/default/lib _build/install/default/bin/rocq dep -boot -package rocq-core -package rocq-core.ltac2 some-test/test.v
some-test/test.vo some-test/test.glob some-test/test.v.beautified some-test/test.required_vo: some-test/test.v fake-lib-dir/rocq-core/ltac2/rocq.d/Ltac2.vo fake-lib-dir/rocq-core/rocq.d/Init/Prelude.vo _build/install/default/lib/rocq-runtime/rocqworker

TODO

• Added / updated test-suite.
• Added changelog.
• Added / updated documentation.

[rlepigre-skylabs-ai]

Regarding the adaptation of rocq makefile, I believe that we wouldn't even need the -package options to the various commands, and that rocqfind would be sufficient for compilation (provided that install packages follow the expected installation scheme). All we'd need to do is ask the user to give a list of package dependencies in a variable ROCQ_PACKAGES, and then we could do something like the following in the generated Makefile:

DEPS_ARGS := $(shell rocqfind -Q -I ${ROCQ_PACKAGES} | tr '\n' ' ')

We would then add ${DEPS_ARGS} to all invoked rocq commands, in addition to the -Q / -R / -I that are needed for the local plugins / theories, and things would just work.

Of course, we'd still need to make sure that make install respects the installation scheme.

[SkySkimmer]

• the -I argument and output of rocqfind seems wrong: -I dir as an argument of rocqdep / rocqc means "add dir to OCAMLPATH". Since rocqfind gets its info from OCAMLPATH it has nothing new to add. The output it gives is also wrong since it prints directories which don't lead to META files. Finally when the _CoqProject contains -I dir (because there is a local META in dir) it seems like rocqfind should be informed about it.

• I don't understand the point of rocqfind, shouldn't rocqc/rocqdep understand -package directly? also what is the point of the cmxs output

[rlepigre-skylabs-ai]

• the -I argument and output of rocqfind seems wrong: -I dir as an argument of rocqdep / rocqc means "add dir to OCAMLPATH". Since rocqfind gets its info from OCAMLPATH it has nothing new to add. The output it gives is also wrong since it prints directories which don't lead to META files.

Good point, I now only add -I for the directories containing the META file.

Finally when the _CoqProject contains -I dir (because there is a local META in dir) it seems like rocqfind should be informed about it.

Yeah, maybe. I was thinking of rocqfind as a way of looking up actually installed stuff, not something we'd use for local plugins for example. I also don't know if rocqfind is useful in itself, but I thought it could be useful for rocq makefile-generated Makefiles.

• I don't understand the point of rocqfind, shouldn't rocqc/rocqdep understand -package directly? also what is the point of the cmxs output

Yeah, I think they probably should, yes.

I initially thought of the cmxs output as a way to get external dependencies, for example in Makefile rules, to get sounder builds when they change. However that's probably not necessary, because the .vo has the hash of the .cmxs it directly uses, right?

[rlepigre-skylabs-ai]

Regarding adding a -package option to rocq c, what do you think is the best way to do that? I see there are several places in the code base where argument parsing is done, and I was hoping not to duplicate the code everywhere (rocq doc, rocqchk, ...).

[SkySkimmer]

the .vo has the has of the .cmxs it directly uses, right?

if "has the has" is meant to be "contains the hash" then yes

[rlepigre-skylabs-ai]

if "has the has" is meant to be "contains the hash" then yes

Oups, I edited the comment.

[rlepigre-skylabs-ai]

I've now added the -package option in all places where I could find a -Q option being supported.

[rlepigre-skylabs-ai]

@SkySkimmer what do you think should be the next steps here? Should I make it so that Corelib and Ltac2 get installed as packages (in addition to the current installation scheme)?

It's also not clear to me how to make tests for this PR. Any recommendation on that front?

[SkySkimmer]

I still don't understand what the transition is supposed to look like.
Are we supposed to install copies of packages in user-contrib and in their own lib/ subdir? That sounds like a waste of disk space.

[rlepigre-skylabs-ai]

That seems like the easiest thing to do (potentially using symbolic links instead of actual copies, but that might lead to problems). Do you see another alternative?

[SkySkimmer]

I don't think the argument parsing in coqproject_file and coqargs are the right places to call resolve. Is findlib even initialized when we're in that code?

It's also not clear to me how to make tests for this PR. Any recommendation on that front?

test-suite/coq-makefile and test-suite/misc have tests which are arbitrary scripts

That seems like the easiest thing to do (potentially using symbolic links instead of actual copies, but that might lead to problems). Do you see another alternative?

If we have copies (including symbolic links) won't they get detected as conflicts? eg Require Prelude would say "found prelude.vo in lib/coq/theories/... and lib/rocq-core/..."

[rlepigre-skylabs-ai]

That seems like the easiest thing to do (potentially using symbolic links instead of actual copies, but that might lead to problems). Do you see another alternative?

If we have copies (including symbolic links) won't they get detected as conflicts? eg Require Prelude would say "found prelude.vo in lib/coq/theories/... and lib/rocq-core/..."

I guess that any particular project you should not rely both on packages and on lib/coq/user-contrib and lib/coq/theories. Either the package is ported, and only uses packages (and transitively for its deps), or it uses a legacy mode that does not allow packages.

Do you think something like that could work?

[SkySkimmer]

Do we really want to force the transition order like that?

[rlepigre-skylabs-ai]

I think this would be OK if package that have transitioned can be depended on by packages that have not, which would simply mean double-installing everything.

To me, it seems fine to require that a package can only transition if all its dependencies have.

[SkySkimmer]

also isn't part of the point of this system that we can multiple packages using the same logical paths? but such packages can't be double installed

[rlepigre-skylabs-ai]

Yeah, that's a good point. I guess they can't right now, so at least that's not a regression. We can only get that benefit when the legacy installation method is removed I guess.

[SkySkimmer]

If we installed only once, we could have coqdep/coqc implicitly add -Q for all findlib packages if no -package is used.
Then a project must give either all or none of its dependencies with -package.
Installed conflicting packages would only error (ambiguous require) if attempted to be used without -package.

This may break dune though.

[rlepigre-skylabs-ai]

This needs more testing, but I believe that this PR has everything for the first step, including the installation of Corelib and Ltac2 following the installation scheme.