Adding package management infrastructure

META.rocq-core.template

@@ -0,0 +1,25 @@
+description = "The Rocq Prover's Core library (including 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"
+  description = "The Rocq Prover's Ltac2 standard library."
+  rocqpath = "Ltac2"
+  requires = "rocq-core"
+  requires += "rocq-runtime.plugins.ltac2_ltac1"
+  requires += "rocq-runtime.plugins.ltac2"
+)

boot/usage.ml

@@ -26,6 +26,7 @@ let print_usage_common co command =
 \n  -include dir           (idem)\
 \n  -R dir coqdir          recursively map physical dir to logical coqdir\
 \n  -Q dir coqdir          map physical dir to logical coqdir\
+\n  -package pkg           add the given Rocq (findlib) package to the load path\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
 \n  -topfile f             set the toplevel name as though compiling f\
 \n  -coqlib dir            set the coq standard library directory\

checker/coqchk_main.ml

@@ -103,6 +103,15 @@ let set_include d p =
   let p = dirpath_of_string p in
   push_include (d,p)
 
+(* Used by option -package. *)
+let packages = ref []
+let add_package p = packages := p :: !packages
+
+let resolve_packages () =
+  let ps = Rocq_package.resolve !packages in
+  packages := [];
+  List.iter (fun p -> set_include p.Rocq_package.dir p.Rocq_package.logpath) ps
+
 (* Initializes the LoadPath *)
 let init_load_path rocqenv =
   (* the to_string casting won't be necessary once Boot handles
@@ -390,6 +399,9 @@ let parse_args argv =
     | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem
     | ("-Q"|"-R") :: ([] | [_]) -> usage 1
 
+    | "-package" :: p :: rem -> add_package p; parse rem
+    | "-package" :: [] -> usage 1
+
     | "-d" :: s :: rem ->
       CDebug.set_flags s;
       parse rem
@@ -454,6 +466,7 @@ let init_with_argv argv =
       | Env coqenv -> init_load_path coqenv
     in
     (* additional loadpath, given with -R/-Q options *)
+    resolve_packages ();
     NewProfile.profile "add_load_paths" (fun () ->
         List.iter
           (fun (unix_path, rocq_root) -> add_rec_path ~unix_path ~rocq_root)

doc/changelog/12-infrastructure-and-dependencies/21564-package-Added.rst

@@ -0,0 +1,13 @@
+- **Added:**
+  New notion of Rocq package and installation layout supported by a new
+  command-line option ``-package DEP`` that automatically adds the correct
+  ``-Q`` and ``-I`` options for ``DEP`` and its transitive dependencies.
+  For backwards compatibility, the old installation scheme targeting the
+  ``coq/user-contrib`` directory is kept, but the plan is to remove it
+  after packages have been ported to the new installation scheme.
+  The ``rocq makefile`` command can be made to rely on the new installation
+  scheme by passing the ``--rocq-package PKGNAME`` argument, and optionally
+  the ``--legacy-support`` argument to also install using the legacy
+  installation scheme
+  (`#21564 <https://github.com/rocq-prover/rocq/pull/21564>`_,
+  by Rodolphe Lepigre).

doc/sphinx/practical-tools/coq-commands.rst

@@ -10,6 +10,7 @@ There are several Rocq commands:
   several other IDEs such as Proof General, vsCoq and Coqtail that are not
   included with the Coq installation.
 + ``rocq``: the main entry point for the Rocq prover
++ ``rocq find``: queries installed Rocq packages and prints their load-path information
 + ``rocqchk``: the Rocq checker (validation of compiled libraries) (also available through ``rocq check``)
 
 Many of the parameters to start these tools are shared and are described below.
@@ -73,6 +74,45 @@ See :ref:`rocq_makefile` and :ref:`building_dune`.
       .. rocqdoc::
          -R <PATH> Mod1
 
+.. _rocqfind:
+
+Rocq package lookup (rocq find)
+-------------------------------
+
+The ``rocq find`` command queries Rocq packages installed through
+OCamlfind.  A Rocq package is an OCamlfind package whose ``META`` file
+contains a ``rocqpath`` field; this field gives the Rocq logical path
+provided by the package.  Package names passed to ``rocq find`` are
+OCamlfind package names, not Rocq logical paths.  Its command-line syntax is
+``rocq find [-Q] [-I] [package ...]``.
+
+With no package argument, ``rocq find`` lists all installed Rocq packages.
+With one or more package arguments, it lists those packages and their
+transitive dependencies.  Its default output contains one line per Rocq
+theory package, with the physical theory directory followed by the logical
+path, for example::
+
+   $ rocq find rocq-stdlib
+   /path/to/lib/rocq-stdlib/rocq.d Stdlib
+
+The ``-Q`` and ``-I`` options make ``rocq find`` print command-line
+arguments instead.  ``-Q`` prints the load-path bindings for Rocq theory
+packages, and ``-I`` prints OCaml include path arguments for OCamlfind
+packages needed by the requested packages, such as plugin dependencies.
+They can be combined::
+
+   $ rocq find -Q -I my-package
+   -Q '/path/to/lib/my-package/rocq.d' MyPackage
+   -I '/path/to/lib/my-package'
+
+For direct invocation of Rocq tools, the ``-package`` option is usually
+more convenient; see :ref:`command-line-options`.  ``rocq find`` is useful
+for inspecting an installation and for build systems that need to obtain
+explicit ``-Q`` and ``-I`` arguments.
+
+See :ref:`rocq_package_layout` for the installation layout assumed by
+``rocq find``.
+
 .. _system_config:
 
 System configuration
@@ -309,6 +349,11 @@ and ``rocq repl``, unless stated otherwise:
 :-R *directory dirpath*: Similar to ``-Q`` *directory dirpath*, but allows using
   :cmd:`Require` with a partially qualified name (i.e. without a `From` clause).
 
+:-package *dependency*: automatically adds the necessary ``-Q`` and ``-I``
+  arguments to be able to work with the Rocq package *dependency* (defined in
+  terms of an ``ocamlfind`` package) and its transitive dependencies.  See
+  :ref:`rocqfind` and :ref:`rocq_package_layout`.
+
 :-top *dirpath*: Set the logical module name to :n:`@dirpath` for the
   `rocq repl` interactive session. If no module name is specified,
   `rocq repl` will default to ``Top``. `rocq compile` does not accept this option

doc/sphinx/practical-tools/utilities.rst

@@ -55,25 +55,86 @@ While this is the easiest way to install packages, it is not the only way.
 You will then need to find the :term:`logical name` used to refer to the package
 in :cmd:`Require` commands.  There are a couple ways to do this:
 
+- For packages using the Findlib-backed Rocq package layout, use
+  :n:`rocq find <package-name>` to show the logical path provided by a package,
+  or :n:`rocq find` to list all installed Rocq packages.  See :ref:`rocqfind`.
+
 - If you installed with opam, use :n:`opam show --list-files rocq-bignums | head -n1` -
   the last component of the filename is the logical name (`Bignums`).
 
-- On Linux, :n:`ls $(rocq c -where)/user-contrib` shows the logical names of all
-  installed user-contributed packages.  You should be able to guess which one you
+- On Linux, :n:`ls $(rocq c -where)/user-contrib` shows the logical names of
+  legacy user-contributed packages.  You should be able to guess which one you
   need.
 
 - Use the :cmd:`Print LoadPath` command when running Rocq, which shows the mapping
   from :term:`logical path`\s to directories.  Again, you should be able to guess.
 
-The last two methods work even if you didn't install with opam.  Perhaps in the
-future the package name to logical name mapping will be more readily available.
-
 Once you know the logical name of the package, use it to load compiled
 files from the package with the :cmd:`Require` command.
 
-A :gdef:`package` is a group of files in a top directory and its subdirectories
-that's installed as a unit.  Packages are compiled from *projects*.  These terms
-are virtually interchangeable.
+A :gdef:`package` is an installable unit of Rocq code and metadata.  A
+package is compiled from a source *project*, which may provide one or more
+installed packages.  In the legacy installation scheme, the files of all
+user-contributed packages are installed together under ``user-contrib``.  In the
+Findlib-backed installation layout, a Rocq package is an OCamlfind package with
+Rocq-specific metadata; commands such as ``rocq find`` and the ``-package``
+option use these OCamlfind package names.  An opam package may provide one or
+more such OCamlfind packages.
+
+.. _rocq_package_layout:
+
+Findlib-backed Rocq package layout
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Rocq packages can be installed using OCamlfind metadata.  This layout keeps the
+files of each package under its own Findlib package directory instead of mixing
+all user libraries under ``coq/user-contrib``.  It is the layout used by the
+``-package`` command-line option (see :ref:`command-line-options`) and by
+:ref:`rocqfind`.
+
+A Rocq theory package is an OCamlfind package whose ``META`` file contains a
+``rocqpath`` field.  The package name is the OCamlfind package name used with
+``-package`` and ``rocq find``; the ``rocqpath`` is the Rocq logical path used in
+:cmd:`Require` commands.  These names need not coincide.  For example, a
+package named ``rocq-stdlib`` may provide the logical path ``Stdlib``.
+
+The important fields of a Rocq theory package are:
+
+``rocqpath``
+  The logical path provided by the package, for example ``Foo`` or
+  ``Stdlib``.  Its presence identifies the Findlib package as a Rocq theory
+  package.
+
+``directory``
+  The package directory, as for any OCamlfind package.
+
+``requires``
+  The package dependencies, written as OCamlfind package names.  Dependencies
+  may be other Rocq theory packages or OCaml packages, including Rocq plugins.
+
+Theory source files and compiled artifacts are installed under a ``rocq.d``
+subdirectory of the package directory.  For example, with a Findlib root
+``$LIB``, a package directory ``$LIB/foo``, and this metadata::
+
+   directory = "."
+   rocqpath = "Foo"
+   requires = "bar foo.plugin"
+
+Rocq theory files for the package are installed below
+``$LIB/foo/rocq.d``.  The command-line option ``-package foo`` expands this
+metadata into the corresponding load path for ``Foo`` and into the paths needed
+by the transitive dependencies.  Equivalently, ``rocq find -Q -I foo`` prints
+explicit ``-Q`` and ``-I`` arguments for use by build systems.
+
+Packages containing both theories and plugins usually express the plugin as a
+Findlib subpackage and list it in ``requires``.  The plugin files remain
+ordinary OCamlfind-installed files; they are not installed under ``rocq.d``.
+
+The legacy installation scheme under ``$(rocq c -where)/user-contrib`` is kept
+for compatibility while packages are ported.  New projects should prefer the
+Findlib-backed layout.  Projects built with ``rocq makefile`` can opt into it
+with ``--rocq-package`` and can additionally request a legacy copy with
+``--legacy-support``.
 
 Setup for working on your own projects
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -395,8 +456,10 @@ separated by whitespace:
 * Selected options of `rocq compile`, which are forwarded directly to it. Currently these
   are ``-Q``, ``-I``, ``-R`` and ``-native-compiler``.
 * ``-arg`` options for other options of `rocq compile` that don’t fall in the above set.
-* Options specific to ``rocq makefile``. Currently there are two options:
-  ``-generate-meta-for-package`` (see below for details), and ``-docroot``.
+* Options specific to ``rocq makefile``. Currently these include ``-docroot``,
+  ``-generate-meta-for-package`` (see below for details), ``--rocq-package``,
+  ``--package-version``, ``--description``, ``--legacy-support``, and
+  ``--no-rocq-package-warning``.
 * Directory names, which include all appropriate files in the directory and
   its subdirectories.
 * Comments, started with an unquoted ``#`` and continuing to the end of the
@@ -439,6 +502,19 @@ includes a ``.mlg`` file (to be pre-processed by ``rocq pp-mlg``) that
 declares a plugin, then the given name must match the ``findlib`` plugin
 name, e.g. ``DECLARE PLUGIN "my-package.plugin"``.
 
+Passing ``--rocq-package my-package`` enables the newer Findlib-backed Rocq
+package installation scheme described in :ref:`rocq_package_layout`. In that
+mode, the project must declare exactly one ``-Q`` or exactly one ``-R``
+directive, whose logical path becomes the package ``rocqpath``. Theory files
+are installed under the Findlib package's ``rocq.d`` directory, and
+``-package`` entries declare package dependencies. The ``--package-version``
+and ``--description`` options fill in the corresponding fields of the generated
+``META`` file. The ``--legacy-support`` option also installs a copy of the
+theories under the global ``user-contrib`` directory. Because the legacy
+installation scheme is deprecated, ``rocq makefile`` warns by default when
+``--rocq-package`` is omitted; pass ``--no-rocq-package-warning`` to silence
+that warning.
+
 The ``-native-compiler`` option given in the ``_RocqProject`` file overrides
 the global one passed at configure time.
 
@@ -459,8 +535,9 @@ This command generates the following files:
 RocqMakefile
   is a makefile for ``GNU Make`` with targets to build the project
   (e.g. generate .vo or .html files from .v or compile .ml* files)
-  and install it in the ``user-contrib`` directory where the Rocq
-  library is installed.
+  and install it. Depending on the project options, installation uses either
+  the legacy ``user-contrib`` directory or the Findlib-backed Rocq package
+  layout.
 
 RocqMakefile.conf
   contains make variables assignments that reflect

lib/coqProject_file.ml

@@ -23,6 +23,11 @@ type 'a project = {
   project_file  : string option;
   makefile : string option;
   native_compiler : native_compiler option;
+  rocq_package : string option;
+  package_version : string option;
+  package_description : string option;
+  legacy_support : bool;
+  warn_missing_rocq_package : bool;
   docroot : string option;
 
   files : string sourced list; (* .v, .ml, .mlg, .mli, .mllib, .mlpack files *)
@@ -32,6 +37,7 @@ type 'a project = {
   ml_includes : path sourced list;
   r_includes  : (path * logic_path) sourced list;
   q_includes  : (path * logic_path) sourced list;
+  packages : string list;
   extra_args : string sourced list;
   defs : (string * string) sourced list;
 
@@ -49,6 +55,11 @@ let mk_project project_file makefile native_compiler extra_data = {
   project_file;
   makefile;
   native_compiler;
+  rocq_package = None;
+  package_version = None;
+  package_description = None;
+  legacy_support = false;
+  warn_missing_rocq_package = true;
   docroot = None;
 
   files = [];
@@ -57,6 +68,7 @@ let mk_project project_file makefile native_compiler extra_data = {
   meta_file = Absent;
   r_includes = [];
   q_includes = [];
+  packages = [];
   extra_args = [];
   defs = [];
 
@@ -236,6 +248,9 @@ let process_cmd_line ~warning_fn orig_dir parse_extra proj args =
        updated version of Dune. *)
     aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r
 
+  | "-package" :: p :: r ->
+    aux { proj with packages = p :: proj.packages } r
+
   | "-native-compiler" :: flag :: r ->
     let proj = parse_native ~warning_fn ~error proj flag in
     aux proj r
@@ -273,6 +288,28 @@ let process_cmd_line ~warning_fn orig_dir parse_extra proj args =
       error "Option -generate-meta-for-package cannot be repeated";
     aux { proj with meta_file = Generate m } r
 
+  | "--rocq-package" :: p :: r ->
+    if proj.rocq_package <> None then
+      error "Option --rocq-package given more than once";
+    if String.equal p "" then
+      error "Option --rocq-package requires a non-empty package name";
+    aux { proj with rocq_package = Some p } r
+
+  | "--package-version" :: v :: r ->
+    if proj.package_version <> None then
+      error "Option --package-version given more than once";
+    aux { proj with package_version = Some v } r
+
+  | "--description" :: d :: r ->
+    if proj.package_description <> None then
+      error "Option --description given more than once";
+    aux { proj with package_description = Some d } r
+
+  | "--legacy-support" :: r ->
+    aux { proj with legacy_support = true } r
+
+  | "--no-rocq-package-warning" :: r ->
+    aux { proj with warn_missing_rocq_package = false } r
 
   | v :: "=" :: def :: r ->
     aux { proj with defs = proj.defs @ [sourced (v,def)] } r
@@ -310,8 +347,15 @@ let process_cmd_line ~warning_fn orig_dir parse_extra proj args =
           end else
               raise (Parsing_error ("Unknown option " ^ f)) in
       aux proj r
- in
+  in
   let proj = aux proj args in
+  let proj =
+    let packages_incs =
+      let get Rocq_package.{dir; logpath} = sourced (mk_path dir, logpath) in
+      List.map get (Rocq_package.resolve proj.packages)
+    in
+    {proj with q_includes = proj.q_includes @ packages_incs}
+  in
   (* Short-circuit -native-compiler options passed via -args *)
   let rec filter_extra proj = function
   | [] -> { proj with extra_args = [] }