diff --git a/META.rocq-core.template b/META.rocq-core.template new file mode 100644 index 000000000000..5108a8d40e8d --- /dev/null +++ b/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" +) diff --git a/boot/usage.ml b/boot/usage.ml index ba1a2bbc43c8..777c09b33da8 100644 --- a/boot/usage.ml +++ b/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\ diff --git a/checker/coqchk_main.ml b/checker/coqchk_main.ml index bc3b5b68a4ca..18924bbb7848 100644 --- a/checker/coqchk_main.ml +++ b/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) diff --git a/doc/changelog/12-infrastructure-and-dependencies/21564-package-Added.rst b/doc/changelog/12-infrastructure-and-dependencies/21564-package-Added.rst new file mode 100644 index 000000000000..34e75eb4dbd0 --- /dev/null +++ b/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 `_, + by Rodolphe Lepigre). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index cb787ec90d6f..e6972a5e8173 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/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 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 diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 8cb2669b583f..75e6796672d3 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/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 ` 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 diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index 05e9b2475d4e..fa2757be5d81 100644 --- a/lib/coqProject_file.ml +++ b/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 = [] } diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 81d2f6935b3d..a01186722864 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -20,6 +20,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; (* the installation path for installing project documentation (relative to * the user-contrib folder) *) docroot : string option; @@ -30,7 +35,9 @@ type 'a project = { ml_includes : path sourced list; r_includes : (path * logic_path) sourced list; + (* Field [q_includes] includes -Q infered from -package arguments. *) q_includes : (path * logic_path) sourced list; + packages : string list; extra_args : string sourced list; defs : (string * string) sourced list; diff --git a/lib/dune b/lib/dune index bdd1529df401..98a5e2a96ca9 100644 --- a/lib/dune +++ b/lib/dune @@ -5,7 +5,7 @@ (wrapped false) (modules_without_implementation xml_datatype) (libraries - rocq-runtime.boot rocq-runtime.clib rocq-runtime.config + rocq-runtime.boot rocq-runtime.clib rocq-runtime.config findlib (select instr.ml from (!coqperf -> instr.noperf.ml) (coqperf -> instr.perf.ml)))) diff --git a/lib/rocq_package.ml b/lib/rocq_package.ml new file mode 100644 index 000000000000..0f40cb268b4f --- /dev/null +++ b/lib/rocq_package.ml @@ -0,0 +1,40 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* t list = fun ps -> + match ps with [] -> [] | _ -> + let ps = + try Findlib.package_deep_ancestors [] ps with + | Findlib.No_such_package (p, _) -> + CErrors.user_err Pp.(str "Failed to locate package " ++ str p) + | Findlib.Package_loop p -> + CErrors.user_err Pp.(str "Dependency loop on package: " ++ str p) + in + let query p = + let p = + let open Fl_package_base in + try Fl_package_base.query p with + | No_such_package (p, info) -> + CErrors.user_err Pp.(str "Failed to query package: " ++ str p) + in + try + let logpath = Fl_metascanner.lookup "rocqpath" [] p.package_defs in + let dir = Filename.concat (p.Fl_package_base.package_dir) "rocq.d" in + let name = p.Fl_package_base.package_name in + Some {name; dir; logpath} + with Not_found -> None + in + List.filter_map query ps diff --git a/lib/rocq_package.mli b/lib/rocq_package.mli new file mode 100644 index 000000000000..bb7f59d2048e --- /dev/null +++ b/lib/rocq_package.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* t list diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index cfdbe0cf6161..cc8c7373b310 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -85,6 +85,7 @@ type coqargs_pre = { ml_includes : string list; vo_includes : vo_path list; + packages : string list; load_vernacular_list : string list; injections : injection_command list; @@ -140,6 +141,7 @@ let default_pre = { load_rcfile = true; ml_includes = []; vo_includes = []; + packages = []; load_vernacular_list = []; injections = []; } @@ -167,6 +169,19 @@ let add_vo_include opts unix_path rocq_path implicit = let v = { unix_path; rocq_path; implicit; } in { opts with pre = { opts.pre with vo_includes = v :: opts.pre.vo_includes }} +let add_package opts p = + { opts with pre = { opts.pre with packages = p :: opts.pre.packages }} + +let resolve_packages args = + let packages = Rocq_package.resolve args.pre.packages in + let add p vo_includes = + let unix_path = p.Rocq_package.dir in + let rocq_path = p.Rocq_package.logpath in + { unix_path; rocq_path; implicit = false } :: vo_includes + in + let vo_includes = List.fold_right add packages args.pre.vo_includes in + { args with pre = { args.pre with vo_includes } } + let add_vo_require opts d ?(allow_failure=false) p export = { opts with pre = { opts.pre with injections = RequireInjection {lib=d; prefix=p; export; allow_failure} :: opts.pre.injections }} @@ -258,7 +273,7 @@ let parse_args ~init arglist : t * string list = let extras = ref [] in let rec parse oval = match !args with | [] -> - (oval, List.rev !extras) + (resolve_packages oval, List.rev !extras) | opt :: rem -> args := rem; let next () = match !args with @@ -282,6 +297,9 @@ let parse_args ~init arglist : t * string list = option. The above line should be removed once we require an updated version of Dune. *) add_vo_include oval d p true + | "-package" -> + let p = next () in + add_package oval p (* Options with one arg *) |"-coqlib" -> diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index 2c5436f04c2f..fc14db70196f 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -80,6 +80,7 @@ type coqargs_pre = { ml_includes : CUnix.physical_path list; vo_includes : vo_path list; + packages : string list; load_vernacular_list : string list; injections : injection_command list; diff --git a/sysinit/dune b/sysinit/dune index 1cb33e730902..16954aea3731 100644 --- a/sysinit/dune +++ b/sysinit/dune @@ -5,7 +5,7 @@ (modules coqargs) (wrapped false) ; don't depend on rocq-runtime.lib -> impossible to imperatively set random flags - (libraries rocq-runtime.config rocq-runtime.boot rocq-runtime.clib)) + (libraries rocq-runtime.config rocq-runtime.boot rocq-runtime.clib rocq-runtime.lib)) (library (name sysinit) diff --git a/test-suite/coq-makefile/package-install/run.sh b/test-suite/coq-makefile/package-install/run.sh new file mode 100755 index 000000000000..a43cebe3fc8d --- /dev/null +++ b/test-suite/coq-makefile/package-install/run.sh @@ -0,0 +1,119 @@ +#!/usr/bin/env bash + +. ../template/path-init.sh + +rm -rf _test +mkdir -p _test/foo/theories _test/use _test/tmp + +cd _test/foo || exit 1 +cat > theories/A.v <<'EOT' +Definition x := 0. +EOT +cat > _CoqProject <<'EOT' +--rocq-package foo +--package-version 1.2.3 +--description "Test package" +--legacy-support +-R theories Foo +theories/A.v +EOT +cat > _CoqProject.bad <<'EOT' +--rocq-package bad +-Q theories Foo +-R theories Foo +theories/A.v +EOT +cat > _CoqProject.legacy <<'EOT' +-R theories Foo +theories/A.v +EOT +cat > _CoqProject.silent <<'EOT' +--no-rocq-package-warning +-R theories Foo +theories/A.v +EOT +rocq makefile -f _CoqProject.legacy -o Makefile.legacy 2> legacy.err +grep -q 'Omitting --rocq-package is deprecated' legacy.err +rocq makefile -f _CoqProject.silent -o Makefile.silent 2> silent.err +if grep -q 'Omitting --rocq-package is deprecated' silent.err; then + echo '--no-rocq-package-warning did not suppress the warning' + exit 1 +fi +if rocq makefile -f _CoqProject.bad -o Makefile.bad; then + echo '--rocq-package accepted both -Q and -R' + exit 1 +fi + +rocq makefile -f _CoqProject -o Makefile +grep -q 'rocqpath = "Foo"' META.foo +grep -q 'directory = "."' META.foo +grep -q 'version = "1.2.3"' META.foo +grep -q 'description = "Test package"' META.foo +make +make install DSTROOT="$PWD/../tmp" + +pkgdir="$(find ../tmp -type d -name foo | head -n 1)" +test -n "$pkgdir" +test -f "$pkgdir/META" +test -f "$pkgdir/rocq.d/A.vo" +grep -q 'rocqpath = "Foo"' "$pkgdir/META" +grep -q 'directory = "."' "$pkgdir/META" +test -f "$(find ../tmp -path '*/user-contrib/Foo/A.vo' | head -n 1)" + +cd .. || exit 1 +mkdir -p plug/theories plug/src +cat > plug/theories/Loader.v <<'EOT' +Declare ML Module "plug.plugin". +EOT +cat > plug/src/plug.mlpack <<'EOT' +Dummy +EOT +cat > plug/src/dummy.ml <<'EOT' +let () = () +EOT +cat > plug/_CoqProject <<'EOT' +--rocq-package plug +-Q theories Plug +-I src +theories/Loader.v +src/dummy.ml +src/plug.mlpack +EOT +(cd plug && rocq makefile -f _CoqProject -o Makefile) +grep -q 'rocqpath = "Plug"' plug/src/META.plug +grep -q 'directory = "."' plug/src/META.plug +grep -q 'requires = "plug.plugin"' plug/src/META.plug +grep -q 'package "plugin"' plug/src/META.plug + +libdir="$(dirname "$pkgdir")" +cd use || exit 1 +cat > B.v <<'EOT' +From Foo Require A. +Definition y := A.x. +EOT +cat > _CoqProject <<'EOT' +--rocq-package bar +-package foo +-Q . Bar +B.v +EOT + +if which cygpath 2>/dev/null; then + export OCAMLPATH="$OCAMLPATH;$(cygpath -m "$libdir")" +else + export OCAMLPATH="$OCAMLPATH:$libdir" +fi + +rocq makefile -f _CoqProject -o Makefile +grep -q 'COQMF_PACKAGES = foo' Makefile.conf +if grep -q 'rocq\.d' Makefile.conf; then + echo 'package dependency was baked into Makefile.conf' + exit 1 +fi +make + +cd ../foo || exit 1 +make uninstall DSTROOT="$PWD/../tmp" +test ! -e "$pkgdir/META" +test ! -d "$pkgdir/rocq.d" +test -z "$(find ../tmp -path '*/user-contrib/Foo/A.vo' | head -n 1)" diff --git a/test-suite/misc/rocq-find.sh b/test-suite/misc/rocq-find.sh new file mode 100755 index 000000000000..b2c6d6bcac8a --- /dev/null +++ b/test-suite/misc/rocq-find.sh @@ -0,0 +1,82 @@ +#!/usr/bin/env bash + +set -euo pipefail +export LC_ALL=C + +ROCQ="${BIN}rocq" +TMP="$(mktemp -d)" +trap 'rm -rf "$TMP"' EXIT + +LIB="$TMP/lib" +mkdir -p "$LIB/foo" "$LIB/bar" "$LIB/rocq-runtime" + +cat > "$LIB/foo/META" <<'EOT' +directory = "." +rocqpath = "Foo" +requires = "bar foo.plugin" + +package "plugin" ( + directory = "plugin" +) +EOT + +cat > "$LIB/bar/META" <<'EOT' +directory = "." +rocqpath = "Bar" +EOT + +# rocq find filters out static toplevel libraries, so provide the package +# queried by the implementation while keeping the test findlib root isolated. +cat > "$LIB/rocq-runtime/META" <<'EOT' +directory = "." + +package "toplevel" ( + directory = "." +) +EOT + +if command -v cygpath >/dev/null 2>&1; then + FINDLIB_LIB="$(cygpath -m "$LIB")" +else + FINDLIB_LIB="$LIB" +fi + +cat > "$TMP/findlib.conf" < "$TMP/find.out" +cat > "$TMP/find.expected" < "$TMP/find-foo.out" +cat > "$TMP/find-foo.expected" < "$TMP/find-foo-flags.out" +cat > "$TMP/find-foo-flags.expected" < + output_string project_file_channel project_file_contents; + flush project_file_channel; + let project = read_project_file ~warning_fn project_file_path in + assert_equal false project.warn_missing_rocq_package + ) () +let _ = add_test "disable missing --rocq-package warning" t + let _ = run_tests __FILE__ (open_log_out_ch __FILE__) (List.rev !tests) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 44ac85b49f4b..200c09a5d1c3 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -27,6 +27,10 @@ MLGFILES := $(COQMF_MLGFILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) METAFILE := $(COQMF_METAFILE) +ROCQPACKAGE := $(COQMF_ROCQPACKAGE) +LEGACYSUPPORT := $(COQMF_LEGACY_SUPPORT) +HASROCQPATH := $(COQMF_HAS_ROCQPATH) +ROCQPATH := $(COQMF_ROCQPATH) CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES) INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT) OTHERFLAGS := $(COQMF_OTHERFLAGS) @@ -44,6 +48,11 @@ CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) OCAMLWARN := $(COQMF_WARN) +PACKAGE_FLAGS := $(foreach pkg,$(COQMF_PACKAGES),-package $(pkg)) +COQLIBS += $(PACKAGE_FLAGS) +COQLIBS_NOML += $(PACKAGE_FLAGS) +CMDLINE_COQLIBS += $(PACKAGE_FLAGS) + @CONF_FILE@: @PROJECT_FILE@ @COQ_MAKEFILE_INVOCATION@ @@ -129,7 +138,7 @@ COQDEBUG ?= # Extra packages to be linked in (as in findlib -package) CAMLPKGS ?= -FINDLIBPKGS = -package rocq-runtime.plugins.ltac $(CAMLPKGS) +FINDLIBPKGS = -package rocq-runtime.plugins.ltac $(PACKAGE_FLAGS) $(CAMLPKGS) # Option for making timing files TIMING?= @@ -172,6 +181,8 @@ COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused vari # findlib files installation FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" +FINDLIBPACKAGEINSTALL = $(COQPLUGININSTALL)/$(FINDLIBPACKAGE) +FINDLIBROCQINSTALL = $(FINDLIBPACKAGEINSTALL)/rocq.d # we need to move out of sight $(METAFILE) otherwise findlib thinks the # package is already installed @@ -186,6 +197,7 @@ findlib_install = \ fi findlib_remove = \ $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ + if [ "$(ROCQPACKAGE)" ]; then rm -rf "$(FINDLIBROCQINSTALL)"; fi; \ "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ fi @@ -382,7 +394,7 @@ ALLNATIVEFILES = \ $(OBJFILES:.o=.cmi) \ $(OBJFILES:.o=.cmx) \ $(OBJFILES:.o=.cmxs) -FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) +FINDLIBPACKAGE=$(if $(ROCQPACKAGE),$(ROCQPACKAGE),$(patsubst .%,%,$(suffix $(METAFILE)))) # trick: wildcard filters out non-existing files, so that `install` doesn't show # warnings and `clean` doesn't pass to rm a list of files that is too long for @@ -581,18 +593,51 @@ install: META $(HIDE)code=0; for f in $$(cat .filestoinstall); do\ if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ done; exit $$code - $(HIDE)for f in $$(cat .filestoinstall); do\ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ "$$?" != "0" -o -z "$$df" ]; then\ - echo SKIP "$$f" since it has no logical path;\ - else\ - install -d "$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ - fi;\ - done $(call findlib_remove) $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) + $(HIDE)if [ "$(ROCQPACKAGE)" ]; then \ + if [ "$(HASROCQPATH)" != "true" ]; then echo "Error: $(METAFILE) has no top-level rocqpath field"; exit 1; fi; \ + root="$(subst .,/,$(ROCQPATH))"; \ + for f in $$(cat .filestoinstall); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`"; rc="$$?";\ + if [ "$$rc" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + if [ "$$df" = "''" ]; then df=""; fi; \ + rel="$$df"; \ + if [ -n "$$root" ]; then \ + case "$$df" in \ + "$$root") rel="" ;; \ + "$$root"/*) rel="$${df#$$root/}" ;; \ + *) echo SKIP "$$f" since it is outside rocqpath "$(ROCQPATH)"; continue ;; \ + esac; \ + else \ + case "$$rel" in /*) rel="$${rel#/}" ;; esac; \ + fi; \ + dest="$(FINDLIBROCQINSTALL)"; \ + if [ -n "$$rel" ]; then dest="$$dest/$$rel"; fi; \ + install -d "$$dest" &&\ + install -m 0644 "$$f" "$$dest" &&\ + echo INSTALL "$$f" "$$dest";\ + if [ "$(LEGACYSUPPORT)" = "true" ]; then \ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi; \ + fi;\ + done; \ + else \ + for f in $$(cat .filestoinstall); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ + done; \ + fi $(HIDE)$(MAKE) install-extra -f "$(SELF)" @rm -f .filestoinstall install-extra:: @@ -601,7 +646,11 @@ install-extra:: META: $(METAFILE) $(HIDE)if [ "$(METAFILE)" ]; then \ - cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ + if [ "$(ROCQPACKAGE)" ]; then \ + cp "$(METAFILE)" META; \ + else \ + cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ + fi; \ fi install-byte: @@ -628,17 +677,21 @@ uninstall:: @# Extension point @$(MKFILESTOINSTALL) $(call findlib_remove) - $(HIDE)for f in $$(cat .filestoinstall); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ - rm -f "$$instf" &&\ - echo RM "$$instf" ;\ - done - $(HIDE)for f in $$(cat .filestoinstall); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ - (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ - done + $(HIDE)if [ -z "$(ROCQPACKAGE)" ] || [ "$(LEGACYSUPPORT)" = "true" ]; then \ + for f in $$(cat .filestoinstall); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + if [ "$$df" = "''" ]; then df=""; fi; \ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" ;\ + done; \ + for f in $$(cat .filestoinstall); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + if [ "$$df" = "''" ]; then df=""; fi; \ + echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ + (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ + done; \ + fi @rm -f .filestoinstall .PHONY: uninstall @@ -865,15 +918,15 @@ $(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) $(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PACKAGE_FLAGS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PACKAGE_FLAGS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PACKAGE_FLAGS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib $(SHOW)'OCAMLLIBDEP $<' diff --git a/tools/coqdep/lib/args.ml b/tools/coqdep/lib/args.ml index f671ee663680..31ebca9875cd 100644 --- a/tools/coqdep/lib/args.ml +++ b/tools/coqdep/lib/args.ml @@ -16,6 +16,7 @@ type t = ; noglob : bool ; ml_path : string list ; vo_path : (bool * string * string) list + ; packages : string list ; dyndep : string ; worker : string option ; files : string list @@ -29,6 +30,7 @@ let make () = ; noglob = false ; ml_path = [] ; vo_path = [] + ; packages = [] ; dyndep = "both" ; worker = None ; files = [] @@ -51,6 +53,7 @@ let usage () = eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir logname : add and import dir recursively to rocq load path under logical name logname\n"; eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to rocq load path under logical name logname\n"; + eprintf " -package pkg : add the given Rocq (findlib) package to the load path\n"; eprintf " -vos : also output dependencies about .vos files\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the rocq core library directory\n"; @@ -101,6 +104,8 @@ let parse st args = | "-R" :: r :: ln :: ll -> parse (add_vo_path st (true, r, ln)) ll | "-Q" :: r :: ln :: ll -> parse (add_vo_path st (false, r, ln)) ll | ("-Q"|"-R") :: ([] | [_]) -> usage () + | "-package" :: p :: ll -> parse { st with packages = p :: st.packages } ll + | "-package" :: [] -> usage () | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse st ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> parse { st with coqlib = Some r } ll @@ -122,5 +127,6 @@ let parse st args = { st with ml_path = List.rev st.ml_path ; vo_path = List.rev st.vo_path + ; packages = List.rev st.packages ; files = List.rev st.files } diff --git a/tools/coqdep/lib/args.mli b/tools/coqdep/lib/args.mli index f4327907b5f0..3d1a307c3eb0 100644 --- a/tools/coqdep/lib/args.mli +++ b/tools/coqdep/lib/args.mli @@ -16,6 +16,7 @@ type t = ; noglob : bool ; ml_path : string list ; vo_path : (bool * string * string) list + ; packages : string list ; dyndep : string ; worker : string option ; files : string list diff --git a/tools/coqdep/lib/common.ml b/tools/coqdep/lib/common.ml index fd15ba00dc2c..dcbab8d983a2 100644 --- a/tools/coqdep/lib/common.ml +++ b/tools/coqdep/lib/common.ml @@ -386,6 +386,12 @@ let add_include st (rc, r, ln) = else Loadpath.add_q_include st r ln +let add_packages st ps = + let add_package p = + Loadpath.add_q_include st p.Rocq_package.dir p.Rocq_package.logpath + in + List.iter add_package (Rocq_package.resolve ps) + let findlib_init dirs = let env_ocamlpath = try [Sys.getenv "OCAMLPATH"] @@ -412,6 +418,7 @@ let init ~make_separator_hack args = ml_path @ Boot.Env.Path.[to_string @@ relative (Boot.Env.runtimelib env) ".."] in findlib_init ml_path; + add_packages loadpath args.Args.packages; List.iter (add_include loadpath) args.Args.vo_path; Makefile.set_dyndep args.Args.dyndep; rocqenv, { State.vAccu = empty_vAccu; loadpath; separator_hack = make_separator_hack } diff --git a/tools/coqdoc/cmdArgs.ml b/tools/coqdoc/cmdArgs.ml index 3a2b531e40e6..6858948d241f 100644 --- a/tools/coqdoc/cmdArgs.ml +++ b/tools/coqdoc/cmdArgs.ml @@ -196,6 +196,8 @@ let args_options = Arg.align [ "   Map physical dir to Rocq dir"; "-Q", arg_path (fun p l -> { p with paths = l :: !prefs.paths }), "   Map physical dir to Rocq dir"; + "-package", arg_string (fun p s -> { p with packages = s :: !prefs.packages }), + "  Add mapping for the given package and its dependencies"; "--latin1", arg_set (fun p -> {p with encoding = { charset = "iso-8859-1"; inputenc = "latin1"; latin1 = true; @@ -253,8 +255,14 @@ let parse_args ~prog args = let new_argv = Array.of_list (prog::new_argv) in argv := new_argv; current := 0; - try - Arg.parse_argv new_argv args_options add_input_files usage_msg - with - | Arg.Bad s -> Printf.eprintf "%s" s - | Arg.Help s -> Printf.printf "%s" s + let _ = + try + Arg.parse_argv new_argv args_options add_input_files usage_msg + with + | Arg.Bad s -> Printf.eprintf "%s" s + | Arg.Help s -> Printf.printf "%s" s + in + List.iter (fun p -> + let path = (normalize_path p.Rocq_package.dir, p.Rocq_package.logpath) in + prefs := { !prefs with paths = path :: !prefs.paths } + ) (Rocq_package.resolve !prefs.packages) diff --git a/tools/coqdoc/common.ml b/tools/coqdoc/common.ml index 8dec42646ec4..e415c09bb5e0 100644 --- a/tools/coqdoc/common.ml +++ b/tools/coqdoc/common.ml @@ -48,6 +48,7 @@ type t = { externals : bool; corelib_url: string; paths : (string * string) list; + packages : string list; encoding : encoding_t; interpolate : bool; raw_comments : bool; @@ -83,6 +84,7 @@ let default : t = { externals = true; corelib_url = Coq_config.wwwcorelib; paths = []; + packages = []; encoding = { charset = "iso-8859-1"; inputenc = ""; diff --git a/tools/coqdoc/common.mli b/tools/coqdoc/common.mli index 2ddb86274c36..3c81c39935a9 100644 --- a/tools/coqdoc/common.mli +++ b/tools/coqdoc/common.mli @@ -53,6 +53,7 @@ type t = { externals : bool; corelib_url : string; paths : (string * string) list; + packages : string list; encoding : encoding_t; interpolate : bool; raw_comments : bool; diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune index 623dee03634d..05988de3af8a 100644 --- a/tools/coqdoc/dune +++ b/tools/coqdoc/dune @@ -15,7 +15,7 @@ (library (name coqdoclib) (modules :standard \ coqdoc) - (libraries str rocq-runtime.boot rocq-runtime.config rocq-runtime.clib)) + (libraries str rocq-runtime.boot rocq-runtime.config rocq-runtime.clib rocq-runtime.lib)) (executable (name coqdoc) diff --git a/tools/dune b/tools/dune index 329fbcefd76a..a636c7052b55 100644 --- a/tools/dune +++ b/tools/dune @@ -60,3 +60,8 @@ (package coq-core) (modules coq_tex) (libraries rocqtex)) + +(library + (name rocqfind) + (modules rocqfind) + (libraries findlib)) diff --git a/tools/dune_rule_gen/coq_rules.ml b/tools/dune_rule_gen/coq_rules.ml index 6576b5d151ba..a70dd383f5b3 100644 --- a/tools/dune_rule_gen/coq_rules.ml +++ b/tools/dune_rule_gen/coq_rules.ml @@ -288,3 +288,18 @@ let install_rule ~(cctx : Context.t) coq_module = Dune_file.Install.{ section = "lib_root"; package = "rocq-core"; files } let install_rules ~dir_info ~cctx = gen_rules ~dir_info ~cctx ~f:install_rule + +let package_install_rule ~(cctx : Context.t) coq_module = + let tname, rule = cctx.theory.dirname, cctx.rule in + let dst_base = match tname with + | ["Corelib"] -> "rocq.d" + | ["Ltac2"] -> Filename.concat "ltac2" "rocq.d" + | _ -> invalid_arg "Unsupported theory name (not Corelib or Ltac2)." + in + let files = + Coq_module.install_files ~tname ~rule coq_module + |> List.map (fun (src,dst) -> src, Filename.concat dst_base dst) in + (* May need to woraround invalid empty `(install )` stanza if that happens *) + Dune_file.Install.{ section = "lib"; package = "rocq-core"; files } + +let package_install_rules ~dir_info ~cctx = gen_rules ~dir_info ~cctx ~f:package_install_rule diff --git a/tools/dune_rule_gen/coq_rules.mli b/tools/dune_rule_gen/coq_rules.mli index d601a05c6d29..f8cf4609daec 100644 --- a/tools/dune_rule_gen/coq_rules.mli +++ b/tools/dune_rule_gen/coq_rules.mli @@ -76,3 +76,8 @@ val install_rules : dir_info :Coq_module.t Dir_info.t -> cctx:Context.t -> Dune_file.Install.t list Dune_file.Subdir.t list + +val package_install_rules : + dir_info :Coq_module.t Dir_info.t + -> cctx:Context.t + -> Dune_file.Install.t list Dune_file.Subdir.t list diff --git a/tools/dune_rule_gen/gen_rules.ml b/tools/dune_rule_gen/gen_rules.ml index 9d1678c45758..069caa5b51f4 100644 --- a/tools/dune_rule_gen/gen_rules.ml +++ b/tools/dune_rule_gen/gen_rules.ml @@ -101,12 +101,14 @@ let main () = let cctx = Coq_rules.Context.make ~root_lvl ~theory ~user_flags ~rule ~boot ~dir_info ~async ~split in let vo_rules = Coq_rules.vo_rules ~dir_info ~cctx in let install_rules = Coq_rules.install_rules ~dir_info ~cctx in + let package_install_rules = Coq_rules.package_install_rules ~dir_info ~cctx in (* Rule printing *) let fmt = Format.std_formatter in List.iter (Dune_file.Subdir.pp ppr fmt) vo_rules; List.iter (Dune_file.Subdir.pp ppi fmt) install_rules; + List.iter (Dune_file.Subdir.pp ppi fmt) package_install_rules; (* Rules for coqnative (not always setup for now, need to think about this) *) begin diff --git a/tools/rocqfind.ml b/tools/rocqfind.ml new file mode 100644 index 000000000000..6ad8681afb92 --- /dev/null +++ b/tools/rocqfind.ml @@ -0,0 +1,112 @@ +let panic fmt = + Format.kfprintf (fun _ -> exit 1) Format.err_formatter (fmt ^^ "\n%!") + +let usage ~prog () = + Format.printf "Usage: %s [-I] [-Q] [-h|--help] PKG ...\n" prog + +type config = { + flag_I : bool; + flag_Q : bool; + pkgs : string list; +} + +let parse_args ~prog args = + let cfg = {flag_I = false; flag_Q = false; pkgs = []} in + let handle_arg cfg arg = + let is_flag arg = String.length arg > 0 && arg.[0] = '-' in + match arg with + | "-I" -> {cfg with flag_I = true} + | "-Q" -> {cfg with flag_Q = true} + | "-h" | "--help" -> usage ~prog (); exit 0 + | _ when is_flag arg -> panic "Error: unrecognized flag %S." arg + | _ -> {cfg with pkgs = arg :: cfg.pkgs} + in + List.fold_left handle_arg cfg args + +let rocqpath pkg = + try Some(Fl_metascanner.lookup "rocqpath" [] pkg.Fl_package_base.package_defs) + with Not_found -> None + +let rec strip_trailing_current_dir dir = + let parent = Filename.dirname dir in + if Filename.basename dir = Filename.current_dir_name && parent <> dir then + strip_trailing_current_dir parent + else + dir + +let rocq_theory_dir pkg = + let dir = strip_trailing_current_dir pkg.Fl_package_base.package_dir in + Filename.concat dir "rocq.d" + +let query_packages pkgs = + Findlib.init (); + let rocq_package_names () = + let pkgs = Fl_package_base.list_packages () in + let get_name pkg_name = + let pkg = Fl_package_base.query pkg_name in + match rocqpath pkg with + | None -> None + | Some _ -> Some(pkg_name) + in + List.filter_map get_name pkgs + in + let pkgs = if pkgs = [] then rocq_package_names () else pkgs in + let pkgs = Fl_package_base.requires_deeply ~preds:[] pkgs in + let static_libs = + let preds = ["native"] in + Fl_package_base.requires_deeply ~preds ["rocq-runtime.toplevel"] + in + let pkgs = List.filter (fun p -> not (List.mem p static_libs)) pkgs in + let query pkg = + let pkg = Fl_package_base.query pkg in + (rocqpath pkg, pkg) + in + List.map query pkgs + +let split_packages pkgs = + let rocq_pkgs = + let filter (rocqpath, pkg) = + match rocqpath with + | None -> None + | Some(p) -> Some(p, pkg) + in + List.filter_map filter pkgs + in + let plugins = + let filter (rocqpath, pkg) = + match rocqpath with + | None -> Some(pkg) + | Some(_) -> None + in + List.filter_map filter pkgs + in + rocq_pkgs, plugins + +module S = Set.Make(String) + +let output_I done_dirs pkg = + (* For sub-packages, the dir with the META is not the package dir. *) + let dir = Filename.dirname pkg.Fl_package_base.package_meta in + if not (S.mem dir !done_dirs) then begin + done_dirs := S.add dir !done_dirs; + Format.printf "-I %s\n%!" (Filename.quote dir) + end + +let output_Q (rocqpath, pkg) = + let dir = rocq_theory_dir pkg in + let dir = Filename.quote dir in + Format.printf "-Q %s %s\n%!" dir rocqpath + +let main ~prog args = + let {flag_I; flag_Q; pkgs} = parse_args ~prog args in + let (rocq_pkgs, plugins) = split_packages (query_packages pkgs) in + match flag_I, flag_Q with + | false, false -> + let output_theory (mp, pkg) = + Format.printf "%s %s\n%!" (rocq_theory_dir pkg) mp + in + List.iter output_theory rocq_pkgs + | _ , _ -> + let done_dirs = ref S.empty in + if flag_Q then List.iter output_Q rocq_pkgs; + if flag_I then List.iter (output_I done_dirs) plugins; diff --git a/tools/rocqfind.mli b/tools/rocqfind.mli new file mode 100644 index 000000000000..0469d6de380a --- /dev/null +++ b/tools/rocqfind.mli @@ -0,0 +1 @@ +val main : prog:string -> string list -> unit diff --git a/tools/rocqmakefile.ml b/tools/rocqmakefile.ml index cc6edf489099..3acda768d96d 100644 --- a/tools/rocqmakefile.ml +++ b/tools/rocqmakefile.ml @@ -21,8 +21,11 @@ let usage_coq_makefile ~ok = \n\ \nrocq makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]\ \n ... [-I dir] ... [-R physicalpath logicalpath]\ -\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ -\n ... [-arg opt] ... [-docroot path] [-f file] [-o file]\ +\n ... [-Q physicalpath logicalpath] ... [-package package]\ +\n ... [VARIABLE = value] ... [-arg opt] ... [-docroot path]\ +\n ... [-f file] [-o file] [--rocq-package package]\ +\n ... [--package-version version] [--description text]\ +\n ... [--legacy-support] [--no-rocq-package-warning]\ \n ... [-generate-meta-for-package project-name]\ \n [-h] [--help] [-v] [--version]\ \n"; @@ -40,6 +43,8 @@ let usage_coq_makefile ~ok = \n[-Q physicalpath logicalpath]: look for Rocq dependencies starting from\ \n \"physicalpath\". The logical path associated to the physical path\ \n is \"logicalpath\".\ +\n[-package package]: add the given Rocq (findlib) package and its\ +\n dependencies to the load path.\ \n[-coqlib dir]: set the Rocq Corelib directory\ \n[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"\ \n[-arg opt]: send option \"opt\" to rocq compile\ @@ -48,6 +53,14 @@ let usage_coq_makefile ~ok = \n[-f file]: take the contents of file as arguments\ \n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ +\n[--rocq-package package]: enable the Findlib-backed Rocq package\ +\n installation scheme for the package named \"package\". This option\ +\n requires exactly one -Q or one -R directive.\ +\n[--package-version version]: set the generated META version field.\ +\n[--description text]: set the generated META description field.\ +\n[--legacy-support]: with --rocq-package, also install theories under\ +\n the global user-contrib directory.\ +\n[--no-rocq-package-warning]: do not warn when --rocq-package is omitted.\ \n[-generate-meta-for-package project-name]: generate META.project-name.\ \n[-h]: print this usage summary\ \n[--help]: equivalent to [-h]\ @@ -93,6 +106,32 @@ let read_whole_file s = close_in ic; Buffer.contents b +let read_meta_top_field field f = + let field_re = Str.regexp ("[ \t]*" ^ field ^ "[ \t]*=[ \t]*\"\\([^\"]*\\)\"") in + let package_re = Str.regexp "[ \t]*package[ \t]+\"[^\"]+\"[ \t]*(" in + let close_re = Str.regexp "[ \t]*)" in + let lines = String.split_on_char '\n' (read_whole_file f) in + let rec aux depth = function + | [] -> None + | line :: lines -> + let depth = + if Str.string_match close_re line 0 then max 0 (depth - 1) + else depth + in + if Int.equal depth 0 && Str.string_match field_re line 0 then + Some (Str.matched_group 1 line) + else + let depth = + if Str.string_match package_re line 0 then depth + 1 + else depth + in + aux depth lines + in + aux 0 lines + +let read_meta_rocqpath = read_meta_top_field "rocqpath" +let read_meta_directory = read_meta_top_field "directory" + (* Use this for quoting contents of variables which never appears as target or * pattern. *) let makefile_quote s = @@ -137,22 +176,62 @@ let generate_makefile oc env conf_file local_file local_late_file dep_file args ] in output_string oc s -let generate_meta_file p = - try - match p.meta_file with - | Absent -> p - | Generate proj -> - let cmname = List.map (fun { thing } -> thing) - (files_by_suffix p.files [".mllib"; ".mlpack"]) in - let dir, cmname = - match cmname with - | [] -> Printf.eprintf "In order to generate a META file one needs an .mlpack or .mllib file\n"; exit 1 - | [x] -> Filename.dirname x, Filename.(basename @@ chop_extension x) - | _ -> Printf.eprintf "Automatic META generation only works for one .mlpack or .mllib file, since you have more you need to write the META file by hand\n"; exit 1 in - let f = dir ^ "/META." ^ proj in - let oc = open_out f in - let meta : _ format = {| -package "plugin" ( +let meta_quote s = + let b = Buffer.create (String.length s) in + String.iter (function + | '\\' -> Buffer.add_string b "\\\\" + | '"' -> Buffer.add_string b "\\\"" + | c -> Buffer.add_char b c) + s; + Buffer.contents b + +let meta_field name = function + | None -> "" + | Some v -> sprintf "%s = \"%s\"\n" name (meta_quote v) + +let meta_requires_field = function + | [] -> "" + | reqs -> sprintf "requires = \"%s\"\n" (String.concat " " reqs) + +let generated_meta_file_name dir pkg = + let file = "META." ^ pkg in + if String.equal dir Filename.current_dir_name then file else Filename.concat dir file + +let archive = function + | [] -> None + | [x] -> Some (Filename.dirname x, Filename.(basename @@ chop_extension x)) + | _ -> + Printf.eprintf "Automatic META generation only works for one .mlpack or .mllib file, since you have more you need to write the META file by hand\n"; + exit 1 + +let archive p = + List.map (fun { thing } -> thing) (files_by_suffix p.files [".mllib"; ".mlpack"]) + |> archive + +let copy_meta_in f = + let ext = Filename.extension f in + if ext = ".in" then + let meta_file = Filename.chop_extension f in + let oc = open_out meta_file in + (* META generation is just a renaming for now, we lack some metadata *) + output_string oc (read_whole_file f); + close_out oc; + Present meta_file + else + Present f (* already a META.package file *) + +let generate_legacy_meta_file p proj = + match archive p with + | None -> Printf.eprintf "In order to generate a META file one needs an .mlpack or .mllib file\n"; exit 1 + | Some (dir, cmname) -> + let f = generated_meta_file_name dir proj in + let oc = open_out f in + let metadata = + meta_field "version" p.package_version ^ + meta_field "description" p.package_description + in + let meta : _ format = {| +%spackage "plugin" ( directory = "." requires = "rocq-runtime.plugins.ltac" archive(byte) = "%s.cma" @@ -162,26 +241,108 @@ package "plugin" ( ) directory = "." |} - in - let meta = Printf.sprintf meta cmname cmname cmname cmname in - output_string oc meta; - close_out oc; - { p with meta_file = Present f } - | Present f -> - let ext = Filename.extension f in - if ext = ".in" then - let meta_file = Filename.chop_extension f in - let oc = open_out meta_file in - (* META generation is just a renaming for now, we lack some metadata *) - output_string oc (read_whole_file f); - close_out oc; - { p with meta_file = Present meta_file } - else - p (* already a META.package file *) + in + let meta = Printf.sprintf meta metadata cmname cmname cmname cmname in + output_string oc meta; + close_out oc; + { p with meta_file = Present f } + +let single_package_rocqpath p = match p.q_includes, p.r_includes with + | [{ thing = (_, logic); _ }], [] + | [], [{ thing = (_, logic); _ }] -> logic + | [], [] -> + Printf.eprintf "Option --rocq-package requires exactly one -Q or one -R directive, but none was provided\n"; + exit 1 + | q, r -> + Printf.eprintf "Option --rocq-package requires exactly one -Q or one -R directive, but found %d -Q and %d -R directives\n" + (List.length q) (List.length r); + exit 1 + +let generate_rocq_package_meta_file p pkg = + let rocqpath = single_package_rocqpath p in + let plugin = archive p in + let dir = match plugin with Some (dir, _) -> dir | None -> Filename.current_dir_name in + let f = generated_meta_file_name dir pkg in + let oc = open_out f in + let root_requires = p.packages @ if plugin = None then [] else [pkg ^ ".plugin"] in + let plugin_meta = match plugin with + | None -> "" + | Some (_, cmname) -> + let requires = meta_requires_field ("rocq-runtime.plugins.ltac" :: p.packages) in + sprintf {| +package "plugin" ( + directory = "." + %s archive(byte) = "%s.cma" + archive(native) = "%s.cmxa" + plugin(byte) = "%s.cma" + plugin(native) = "%s.cmxs" +) +|} requires cmname cmname cmname cmname + in + let version = Some (Option.default "dev" p.package_version) in + let meta = sprintf {|%s%sdirectory = "." +rocqpath = "%s" +%s%s|} + (meta_field "version" version) + (meta_field "description" p.package_description) + (meta_quote rocqpath) (meta_requires_field root_requires) plugin_meta in + output_string oc meta; + close_out oc; + { p with meta_file = Present f } + +let check_rocq_package_meta_file p = match p.rocq_package, p.meta_file with + | Some _, Present f -> + begin match read_meta_rocqpath f with + | Some rocqpath when String.equal rocqpath (single_package_rocqpath p) -> () + | Some rocqpath -> + Printf.eprintf "The top-level rocqpath field in %s is %S, but --rocq-package expects the -Q/-R logical path %S\n" + f rocqpath (single_package_rocqpath p); + exit 1 + | None -> + Printf.eprintf "Option --rocq-package requires %s to contain a top-level rocqpath field\n" f; + exit 1 + end; + begin match read_meta_directory f with + | None | Some "." -> p + | Some dir -> + Printf.eprintf "The top-level directory field in %s is %S, but --rocq-package requires \".\"\n" f dir; + exit 1 + end + | _ -> p + +let generate_meta_file p = + try + let p = match p.rocq_package, p.meta_file with + | Some pkg, (Absent | Generate _) -> generate_rocq_package_meta_file p pkg + | Some _, Present f -> { p with meta_file = copy_meta_in f } + | None, Absent -> p + | None, Generate proj -> generate_legacy_meta_file p proj + | None, Present f -> { p with meta_file = copy_meta_in f } + in + check_rocq_package_meta_file p with Sys_error e -> Printf.eprintf "Error: %s\n" e; exit 1 +let remove_package_includes p = + let packages = + List.map (fun (Rocq_package.{ dir; logpath; _ }) -> + CUnix.canonical_path_name dir, logpath) + (Rocq_package.resolve p.packages) + in + let is_package_include { thing = ({ canonical_path; _ }, logic); _ } = + List.exists (fun (dir, logpath) -> + String.equal canonical_path dir && String.equal logic logpath) packages + in + { p with q_includes = List.filter (fun inc -> not (is_package_include inc)) p.q_includes } + +let setup_rocq_package project = match project.rocq_package with + | None -> project + | Some _ -> + let project = remove_package_includes project in + ignore (single_package_rocqpath project); + project + let section oc s = let pad = String.make (76 - String.length s) ' ' in let sharps = String.make 79 '#' in @@ -193,7 +354,7 @@ let section oc s = fprintf oc "%s\n\n" sharps ;; -let generate_conf_includes oc { ml_includes; r_includes; q_includes } = +let generate_conf_includes oc { ml_includes; r_includes; q_includes; packages; rocq_package; _ } = section oc "Path directives (-I, -R, -Q)."; let module S = String in let map = map_sourced_list in @@ -214,6 +375,8 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes)) (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes)) (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "R" path l) r_includes)); + fprintf oc "COQMF_PACKAGES = %s\n" + (match rocq_package with None -> "" | Some _ -> S.concat " " packages); ;; let windrive s = @@ -231,7 +394,8 @@ let generate_conf_coq_config oc env = ;; let check_metafile p = - if files_by_suffix p.files [".mlpack"; ".mllib"] <> [] && p.meta_file = Absent then begin + if p.rocq_package = None && + files_by_suffix p.files [".mlpack"; ".mllib"] <> [] && p.meta_file = Absent then begin eprintf "Warning: it is recommended you provide a META.package-name file\n"; eprintf "Warning: since you build plugins. See also -generate-meta-for-package.\n"; end @@ -264,7 +428,15 @@ let generate_conf_files oc p = fout "MLGFILES" ".mlg"; fout "MLPACKFILES" ".mlpack"; fout "MLLIBFILES" ".mllib"; - fprintf oc "COQMF_METAFILE = %s\n" (match p.meta_file with Present x -> x | _ -> "") + fprintf oc "COQMF_METAFILE = %s\n" (match p.meta_file with Present x -> x | _ -> ""); + fprintf oc "COQMF_ROCQPACKAGE = %s\n" (Option.default "" p.rocq_package); + fprintf oc "COQMF_LEGACY_SUPPORT = %s\n" (if p.legacy_support then "true" else "false"); + let rocqpath = match p.rocq_package, p.meta_file with + | Some _, Present x -> read_meta_rocqpath x + | _ -> None + in + fprintf oc "COQMF_HAS_ROCQPATH = %s\n" (if Option.has_some rocqpath then "true" else "false"); + fprintf oc "COQMF_ROCQPATH = %s\n" (Option.default "" rocqpath) let rec all_start_with prefix = function | [] -> true @@ -430,8 +602,13 @@ let destination_of { ml_includes; q_includes; r_includes; } file = let normal_mode ~coqlib project prog args = if project.makefile = None then eprintf "Warning: Omitting -o is deprecated\n\n"; - (* We want to know the name of the Makefile (say m) in order to - * generate m.conf and include m.local *) + if project.rocq_package = None && project.warn_missing_rocq_package then begin + eprintf "Warning: Omitting --rocq-package is deprecated.\n"; + eprintf "Warning: Use --rocq-package to enable the Findlib-backed Rocq package installation scheme.\n"; + eprintf "Warning: Pass --no-rocq-package-warning to silence this warning.\n\n"; + end; + (* We want to know the name of the Makefile (say m) in order to + * generate m.conf and include m.local *) let conf_file = Option.default "CoqMakefile" project.makefile ^ ".conf" in let local_file = Option.default "CoqMakefile" project.makefile ^ ".local" in @@ -440,6 +617,8 @@ let normal_mode ~coqlib project prog args = let project = ensure_root_dir project in + let project = setup_rocq_package project in + check_overlapping_include project; check_native_compiler project.native_compiler; diff --git a/topbin/dune b/topbin/dune index 04e73b63b885..b4d6949d0116 100644 --- a/topbin/dune +++ b/topbin/dune @@ -12,7 +12,7 @@ (modules rocq) (modes exe byte) ; we statically link the "small" subcommands instead of having separate binaries - (libraries rocqshim coqdeplib coqpp coqdoclib rocqwc rocqworkmgr rocqtex rocqmakefile)) + (libraries rocqshim coqdeplib coqpp coqdoclib rocqwc rocqworkmgr rocqtex rocqmakefile rocqfind)) (install (section bin) diff --git a/topbin/rocq.ml b/topbin/rocq.ml index 2f8ea49e1469..45b389c8dde3 100644 --- a/topbin/rocq.ml +++ b/topbin/rocq.ml @@ -35,6 +35,7 @@ type subcommand = | Votour | PpMlg | Dep + | Find | Doc | Wc | Workmgr @@ -55,6 +56,7 @@ let subcommands = [ ("preprocess-mlg", "Preprocess Rocq grammar files (.mlg) to produce OCaml sources", PpMlg); ("pp-mlg", "Alias for preprocess-mlg", PpMlg); ("dep", "Print dependencies for compiling Rocq files", Dep); + ("find", "Print load-path information for Rocq findlib packages", Find); ("doc", "Generate documentation from a Rocq source file", Doc); ("wc", "Count lines of code in a Rocq source file", Wc); ("workmgr", "Control the number of parallel workers used by Rocq", Workmgr); @@ -94,6 +96,7 @@ let run_subcommand opts args = function | Votour -> with_sibling_exe opts "votour" args | PpMlg -> Coqpp_main.main args | Dep -> Coqdeplib.Rocqdep_main.main args + | Find -> Rocqfind.main ~prog:(Sys.argv.(0) ^ " find") args | Doc -> Coqdoclib.Rocqdoc_main.main ~prog:(Sys.argv.(0) ^ " doc") args | Wc -> Rocqwc.main args | Workmgr -> Rocqworkmgr.main ~prog:(Sys.argv.(0) ^ " workmgr") args diff --git a/topbin/rocqnative.ml b/topbin/rocqnative.ml index 7ec16574ae02..b3e2d52734fa 100644 --- a/topbin/rocqnative.ml +++ b/topbin/rocqnative.ml @@ -309,6 +309,7 @@ let print_usage_channel co command = output_string co " -Q dir coqdir map physical dir to logical coqdir\ \n -R dir coqdir synonymous for -Q\ +\n -package pkg add mapping for the given package and its dependencies\ \n\ \n\ \n -boot boot mode\ @@ -338,6 +339,7 @@ type opts = { coqlib : string option; vo_path : (string * DirPath.t) list; ml_path : string list; + packages : string list; } let rec parse_args (args : string list) accu = @@ -356,6 +358,9 @@ let rec parse_args (args : string list) accu = let p = Loadpath.dirpath_of_string p in let accu = { accu with vo_path = (d, p) :: accu.vo_path } in parse_args rem accu + | "-package" :: p :: rem -> + let accu = { accu with packages = p :: accu.packages } in + parse_args rem accu | "-I" :: _d :: rem -> (* Ignore *) parse_args rem accu @@ -373,11 +378,18 @@ let rec parse_args (args : string list) accu = let args_msg = String.concat " " args in CErrors.user_err Pp.(str "parse args error, too many arguments: " ++ str args_msg) +let resolve_packages opts = + List.fold_left (fun opts p -> + let logpath = Loadpath.dirpath_of_string p.Rocq_package.logpath in + { opts with vo_path = (p.Rocq_package.dir, logpath) :: opts.vo_path } + ) opts (Rocq_package.resolve opts.packages) + let () = let _ = Feedback.add_feeder fb_handler in try - let opts = { boot = false; coqlib = None; vo_path = []; ml_path = [] } in + let opts = { boot = false; coqlib = None; vo_path = []; ml_path = []; packages = [] } in let opts, in_file = parse_args (List.tl @@ Array.to_list Sys.argv) opts in + let opts = resolve_packages opts in let () = init_load_path ~boot:opts.boot ~coqlib:opts.coqlib ~vo_path:(List.rev opts.vo_path)