From 9e9f214235f9e95208d0eb81d5031bd58e3f4343 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Mon, 11 Nov 2024 00:50:47 +0100 Subject: [PATCH 1/2] Rocq Package Metadata: Piggybacking on Findlib. --- text/000-rocq-findlib.md | 267 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 267 insertions(+) create mode 100644 text/000-rocq-findlib.md diff --git a/text/000-rocq-findlib.md b/text/000-rocq-findlib.md new file mode 100644 index 00000000..fbab1434 --- /dev/null +++ b/text/000-rocq-findlib.md @@ -0,0 +1,267 @@ +- Title: Rocq Package Metadata: Piggybacking on Findlib + +- Drivers: Rodolphe Lepigre + +---- + +# Summary + +The current installation scheme for Rocq theories, which consists in mingling +files from various packages under a single `user-contrib` folder, poses many +modularity problems. To solve them, we propose to piggyback on existing OCaml +Findlib infrastructure, which would support a much better installation scheme, +targeting different directories for different packages (as is typically done +in other languages, for example OCaml). This proposal is in part motivated by +the desire to improve the Rocq support in the `dune` build system. + +# Motivation + +Rocq packages, typically in the form of Opam packages, currently adhere to the +following installation scheme (focusing on plugins and theories only). If +there are plugins, they are simply installed as standard OCaml libraries. This +builds on existing OCaml infrastructure, and works very well in practice since +the move to the `findlib` method for loading plugins. Rocq theories, however, +are all installed under `$PREFIX/lib/rocq/user-contrib/`, independently of the +package they originate from. + +The `user-contrib` setup poses several modularity issues: +1. The connection between theories and the packages they originate from is + lost. In particular, this makes it non-trivial to uninstall a package, and + extra metadata needs to be kept in a package-specific way. For example, the + `dune` build system relies on its `dune-package` files to remember exactly + what files belong to a package. +2. Two packages can overlap in the directory paths they define, but the setup + prevents them from defining theories with the same name (they would end up + at exactly the same file path). For instance, this forbids one to provide + alternative packages defining theories with the same interface, which can + be useful for configuration options, or alternative implementations when + there are various trade-offs to choose from. +3. It is not possible to infer the transitive dependencies of a given package + from its installed theories. As a consequence, build systems are left with + two alternatives: + - Always give access to the whole of user-contrib, which is what happens + with typical `rocq_makefile` setups. + - Only give access to user-selected theories (as with the `dune` setup), + but require users to make all transitive dependencies explicit, which + clearly does not scale. +4. It is not possible to know what plugins a given package might want to + load, which again poses problems for build systems like `dune`. + +# Detailed design + +The main idea is to piggyback on the OCaml Findlib infrastructure. It is used +for plugins already, and that should remain unchanged. In particular, plugins +should continue to be installed in the same way. + +The proposal is to install Rocq theories similarly to OCaml packages. Here, +the notion of package is that of Findlib, not that of Opam, even though they +are related (an Opam package generally consists in a collection of Findlib +packages). Findlib packages are declared in `META` files, which typically +look like the following. +``` +version = "dev" +description = "..." +requires = "str unix yojson" +... + +package "subpackage1" ( + directory = "subpackage1" + version = "dev" + description = "..." + requires = "str unix yojson" + ... +) + +package "subpackage2" ( + directory = "package2" + + package "subsubpackage1" ( + directory = "subsubpackage1" + version = "dev" + description = "..." + requires = "str unix" + ... + ) + + package "subsubpackage2" ( + ... + ) +) +``` +Assuming that the above `META` file is placed in a folder `example`, then +it declares four packages named `example`, `example.subpackage1`, +`example.subpackage2.subsubpackage1`, and +`example.subpackage2.subsubpackage2`. +Each package has associated metadata, including a list of the other packages +it depends on (`requires` field), and a directory (`directory` field). The +directory for package `example` is the `example/` directory holding the `META` +file. The directory for `example.subpackage1` is `example/subpackage1/`. In +effect, the nesting of packages reflects a nesting of directories, and it is +expected for packages to place their files (which, or OCaml would be `.cma`, +`.cmxa`, and `.cmxs` files, for example) in their respective directories. + +For Rocq theories, the same structure can be preserved: the package name can +be used to require the corresponding theory in build systems, and the package +directory can be used to store the theory's files (`.v`, `.vo`, `.glob`). The +`requires` field can also be used to specify dependencies on both plugins, and +other theories uniformly. The only missing piece is the expected directory +path for the theory. For that, we can simply rely on a new `rocqpath` field, +whose presence also indicates what findlib package is a Rocq theory. + +## Package structure + +A Rocq theory Findlib package contains the following information: +- The package name built in the usual Findlib way. Note that the package name + may (and often will) differ from the directory path of the theory. Indeed, + the contrary would be way too constraining (and would also prevent fixing + modularity issue 2). For example, the findlib package for the Rocq stdlib + would likely be named `rocq-stdlib`, while its directory path is `Stdlib`. +- Field `rocqpath` specifying the directory path associated to the package's + theory. The presence of this field also distinguishes Rocq theory packages + from standard OCaml package (including Rocq plugins). +- Standard field `directory`, indicating the directory under which the files + for the package are expected to be found. Unlike OCaml packages, theories do + not generally have a flat directory structure. To guard against collosions + between package names and Rocq path members, theory files should be stored + under an additional `rocq.d` directory. Note that since `rocq.d` contains a + dot, it does not constitute a valid package name, which should prevent name + clashes in practice. (Generally, (sub-)package names coincide with their + directory field, but that is not a requirement of the META format. If that + convention was to be adopted, clashes would become impossible.) +- Standard field `requires`, giving a list of dependencies, in the form of + package names. These include both plugins and other theories, as they can + be handled uniformly. Note that a package can always be identified as a + theory by looking for the `rocqpath` field. +- Other standard metadata fields like `version` or `description`. + +## Requiring a package + +When a package `my_package` is required via a build system, the metadata can +be used to compute a set of transitive dependencies for it. Using `ocamlfind`, +this can be done as follows. +``` +ocamlfind query p -r -format "%p" +``` + +The obtained packages can then be sorted into two lists: one containing OCaml +libraries (including Rocq plugins), and one containing Rocq theories. One may +run the following command to determine whether a package is a theory or not. +``` +ocamlfind query some_dep -format "%(rocqpath)" +``` +The result is empty if `some_dep` is a standard OCaml package (possibly a Rocq +plugin), and it gives a directory path for Rocq theories. + +The mapping for each theory package `some_theory` can then be computed using +the following command. +``` +ocamlfind query some_theory -format "-Q %d/rocq.d %(rocqpath)" +``` + +## Example: stdpp + +The packages for [stdpp](https://gitlab.mpi-sws.org/iris/stdpp) could end up +being installed under `/lib/rocq-stdpp/`, which would contains the +following `META` file. +``` +version = "dev" +description = "An extended \"Standard Library\" for Rocq." +rocqpath = "stdpp" +requires = "rocq-stdlib" + +package "bitvector" ( + directory = "bitvector" + version = "dev" + description = "A library for bitvectors based on std++." + rocqpath = "stdpp.bitvector" + requires = "rocq-stdpp" +) + +package "unstable" ( + directory = "unstable" + version = "dev" + description = "Unfinished std++ libraries." + rocqpath = "stdpp.unstable" + requires = "rocq-stdpp" +) +``` + +Differences with the current `stdpp` setup: +- Rocq-ified package names. +- Use of sub-packages form `stdpp.bitvector` and `stdpp.unstable`, instead of + different Opam packages. + +## Example: coq-elpi + +``` +rocqpath = "elpi" +requires = "rocq-stdlib coq-elpi.plugin" +... + +package "plugin" ( + directory = "plugin" + requires = "rocq-core.plugins.ltac rocq-core.vernac elpi" + ... +) + +package "apps" ( + directory "apps" + + package "derive" ( + directory "derive" + rocqpath = "elpi.apps.derive" + requires = "rocq-elpi rocq-elpi.apps.derive.elpi" + ... + + package "elpi" ( + directory "elpi" + rocqpath = "elpi.apps.derive.elpi" + requires = "rocq-elpi" + ... + ) + ) + + package "tc" ( + directory "tc" + rocqpath = "elpi.apps.tc" + requires = "rocq-elpi rocq-elpi.apps.tc.elpi rocq-elpi.apps.tc.plugin" + ... + + package "plugin" ( + directory = "plugin" + requires = "rocq-core.plugins.ltac rocq-core.vernac rocq-elpi.plugin" + ... + ) + + package "elpi" ( + directory "elpi" + rocqpath = "elpi.apps.tc.elpi" + requires = "rocq-elpi" + ... + ) + ) + + ... +) +``` + +# Drawbacks + +None, except the eventual need to port all projects to use a build system that +respects the new installation scheme. However, as a first step, it is possible +to keep using the current installation scheme at the same time. + +# Alternatives + +All reasonable systems have a modular installation scheme. An alternatives +implementation would be to start from scratch and not reuse the Findlib file +format, but given the close integration of Rocq in the OCaml ecosystem that +probably would not make sense. + +# Unresolved questions + +Can we adapt `rocq_makefile` so that it expects dependencies to be installed +following the considered installation scheme, and itself installs libraries +appropriately? + +We need to confirm that this is good enough for good `dune` support. From 37f7a335f8612cdb9f49fc3ade8841c8c39d608a Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Mon, 11 Nov 2024 09:13:27 +0100 Subject: [PATCH 2/2] Apply suggestions from code review Co-authored-by: Jim Fehrle --- text/000-rocq-findlib.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/000-rocq-findlib.md b/text/000-rocq-findlib.md index fbab1434..daa028e2 100644 --- a/text/000-rocq-findlib.md +++ b/text/000-rocq-findlib.md @@ -121,7 +121,7 @@ A Rocq theory Findlib package contains the following information: from standard OCaml package (including Rocq plugins). - Standard field `directory`, indicating the directory under which the files for the package are expected to be found. Unlike OCaml packages, theories do - not generally have a flat directory structure. To guard against collosions + not generally have a flat directory structure. To guard against collisions between package names and Rocq path members, theory files should be stored under an additional `rocq.d` directory. Note that since `rocq.d` contains a dot, it does not constitute a valid package name, which should prevent name @@ -253,7 +253,7 @@ to keep using the current installation scheme at the same time. # Alternatives -All reasonable systems have a modular installation scheme. An alternatives +All reasonable systems have a modular installation scheme. An alternative implementation would be to start from scratch and not reuse the Findlib file format, but given the close integration of Rocq in the OCaml ecosystem that probably would not make sense.