feature(coq): composition of installed theories #7047

Alizter · 2023-02-11T21:00:21Z

We add support for composition with installed theories to the Coq rules.

This allows people to use Dune even if their project depends on an installed project built using make.

This works by first checking if coq lang is enabled, then scanning user-contrib and directories in COQPATH for potential theories. Then a database is constructed allowing users to write (thories foo.bar) and Dune will look for the Coq_lib_name foo.bar. The database would have an entry for user-contrib/foo/bar say and would in turn be able to describe a Coq theory.

Closes #6982

Any testing would be appreciated.

Tasks:

ejgallego · 2023-02-11T22:37:19Z

Very nice!

I'm unsure if we should introduce a Coq_lib.Legacy.t type tho, I guess there is no need as the abstraction we have works.

A pain in the ass regarding plugins is that Coq by default will add anything under user-contrib to -I, we need to do the same for the sub-tree in question (tho maybe only the top level happens in practice)?

How are the meta files installed for plugins in 8.16?

Some test ideas:

test with installed coq (and requiring the Coq library to be added explicitly)
test with some true opam package
mock tests can be done setting COQLIB, not sure if we need to pass -require Coq.Init.Prelude tho?
we should test with a plugin installed in user-contrib, mock version

src/dune_rules/coq/coq_lib.ml

src/dune_rules/coq/coq_rules.ml

src/dune_rules/lib.mli

This will be important once we have installed_theories in ocaml#7047 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

src/dune_rules/coq/coq_lib.ml

This will be important once we have installed_theories in ocaml#7047 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

This will be important once we have installed_theories in #7047 Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

Alizter · 2023-03-07T20:11:37Z

I've pushed a bunch of commits for the current WIP. There is now support for composition with installed plugins and also -boot is being passed everywhere. There is a lot of clean up we can do now.

There are a few commits in here I will cherry pick and make into their own PRs. I don't plan to keep the testing of equations and mathcomp in the CI, that is just for show.

ejgallego · 2023-03-08T00:07:39Z

Amazing work @Alizter !

Blaisorblade · 2023-04-07T19:14:47Z

(thories something.installed)

But spelling out whether something is installed prevents dune composition, doesn't it?

ejgallego · 2023-04-07T19:27:33Z

But spelling out whether something is installed prevents dune composition, doesn't it?

I guess @Alizter just meant that name as a token, the installed part has no relevance.

With this PR, things work for Coq like in OCaml, theories are looked locally (in scope, so both private and public are visible), then in the workspace, then in the installed_db which is built from COQLIB and COQPATH

Alizter · 2023-04-07T21:53:26Z

(thories something.installed)

But spelling out whether something is installed prevents dune composition, doesn't it?

Yeah it was just a name. I should have said foo.bar instead.

Alizter · 2023-04-17T22:51:16Z

@ejgallego The tests are now passing. We no longer pass -boot if we are < 0.8. Please have a look through and let me know if there is anything left, otherwise we should be ready to merge.

Alizter · 2023-04-17T23:21:07Z

I've also tested this in a docker container with coq 8.17 and the tests all pass.

Signed-off-by: Ali Caglayan <alizter@gmail.com>

This is some preliminary refactoring for the introduction of a legeacy library later on when we introduce library composition. Signed-off-by: Ali Caglayan <alizter@gmail.com>

When we start considering installed libraries we need to have a general path. Signed-off-by: Ali Caglayan <alizter@gmail.com>

Signed-off-by: Ali Caglayan <alizter@gmail.com>

We turn a polymorphic variant into a few regular datatypes, so stages of resolution have a totally separate typing, not sharing constructors anymore. Signed-off-by: Ali Caglayan <alizter@gmail.com>

Added: - Coq_lib.equal (from compare) - Coq_lib.empty (convenience for mapping lib names to dirs) - Coq_lib.stdlib (name of the Coq standrad library) - Coq_lib.to_list (perhaps should be renamed explode) - Coq_lib.append Signed-off-by: Ali Caglayan <alizter@gmail.com>

This commit introduces a new database for "installed" theories present in `user-contrib` and `COQPATH`. The above paths are scanned and the database of theories is populated based on the subdirectories found. In order to keep compatibility, we add to the database all possible theory names (so for example, given a directory `A/B` we will register two Coq theories `A` and `A.B`). Changes in the code are as expected, main new things are: - `Coq_lib.t` now can represent two kind of objects: theories with an associated dune stanza, and theories found in the system and for whom no stanza is available. - A new`Coq_path.t` type, which represents an inferred "stanza" for libraries that are installed in the `user-contrib` / `COQPATH` scheme. The list of such paths is then used to build the database. Starting with `(coq lang 0.8)` Coq will not see any theory, even if globally installed, unless that theory was declared in the corresponding `theories` field in the stanzas. This solves a longstanding problem due to users being not able to compose with a theory that could present either locally or in installed form. Signed-off-by: Ali Caglayan <alizter@gmail.com> Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>

ejgallego

Ready to merge!

Since ocaml#6409 we automatically infer rules for coq-native, and in general this requires at least Coq 8.10 due to the need of command-line option flags added in that version for native. Also, since ocaml#7047 and `(coq lang 0.8)` we detect installed theories, correcting a longstanding problem, we require all users to migrate. The recommended path for most projects is just to upgrade their dune file and Coq version file. Coq 8.10 will likely be the base we support in `(lang coq 1.0)`. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

@rgrinberg

CHANGES: - Correctly set `MANPATH` in `dune exec`. Previously, we would use the `bin/` directory of the context. (ocaml/dune#7655, @rgrinberg) - Allow overriding the `ocaml` binary with findlib configuration (ocaml/dune#7648, @rgrinberg) - Modules that were declared in `(modules_without_implementation)`, `(private_modules)` or `(virtual_modules)` but not declared in `(modules)` will cause Dune to emit a warning which will become an error in 3.9. (ocaml/dune#7608, fixes ocaml/dune#7026, @Alizter) - Dune can now detect Coq theories from outside the workspace. This allows for composition with installed theories (not necessarily installed with Dune). (ocaml/dune#7047, @Alizter, @ejgallego) - Fix regression where Merlin was unable to handle filenames with uppercase letters under Windows. (ocaml/dune#7577, @nojb) - On nix+macos, pass `-f` to the codesign hook to avoid errors when the binary is already signed (ocaml/dune#7183, fixes ocaml/dune#6265, @greedy) - Fix bug where RPC clients built with dune-rpc-lwt would crash when closing their connection to the server (ocaml/dune#7581, @gridbugs) - Introduce mdx stanza 0.4 requiring mdx >= 2.3.0 which updates the default list of files to include `*.mld` files (ocaml/dune#7582, @Leonidas-from-XIV) - Fix RPC server on Windows (used for OCaml-LSP). (ocaml/dune#7666, @nojb) - In `(executable)`, `(public_name -)` is now equivalent to no `(public_name)`. This is consistent with how `(executables)` handles this field. (ocaml/dune#7576 , fixes ocaml/dune#5852, @emillon) - Change directory of odoc assets to `odoc.support` (was `_odoc_support`) so that it works with Github Pages out of the box. (ocaml/dune#7588, fixes ocaml/dune#7364, @emillon)

@rleshchinskiy

CHANGES: - Fix string quoting in the json file written by `--trace-file` (ocaml/dune#7773, @rleshchinskiy) - Read `pkg-config` arguments from the `PKG_CONFIG_ARGN` environment variable (ocaml/dune#1492, ocaml/dune#7734, @anmonteiro) - Correctly set `MANPATH` in `dune exec`. Previously, we would use the `bin/` directory of the context. (ocaml/dune#7655, @rgrinberg) - Allow overriding the `ocaml` binary with findlib configuration (ocaml/dune#7648, @rgrinberg) - merlin: ignore instrumentation settings for preprocessing. (ocaml/dune#7606, fixes ocaml/dune#7465, @Alizter) - When a rule's action is interrupted, delete any leftover directory targets. This is consistent with how we treat file targets. (ocaml/dune#7564, @rgrinberg) - Fix plugin loading with findlib. The functionality was broken in 3.7.0. (ocaml/dune#7556, @anmonteiro) - Introduce a `public_headers` field on libraries. This field is like `install_c_headers`, but it allows to choose the extension and choose the paths for the installed headers. (ocaml/dune#7512, @rgrinberg) - Load the host context `findlib.conf` when cross-compiling (ocaml/dune#7428, fixes ocaml/dune#1701, @rgrinberg, @anmonteiro) - Add a `coqdoc_flags` field to the `coq.theory` stanza allowing the user to pass extra arguments to `coqdoc`. (ocaml/dune#7676, fixes ocaml/dune#7954 @Alizter) - Resolve `ppx_runtime_libraries` in the target context when cross compiling (ocaml/dune#7450, fixes ocaml/dune#2794, @anmonteiro) - Use `$PKG_CONFIG`, when set, to find the `pkg-config` binary (ocaml/dune#7469, fixes ocaml/dune#2572, @anmonteiro) - Modules that were declared in `(modules_without_implementation)`, `(private_modules)` or `(virtual_modules)` but not declared in `(modules)` will cause Dune to emit a warning which will become an error in 3.9. (ocaml/dune#7608, fixes ocaml/dune#7026, @Alizter) - Preliminary support for Coq compiled intefaces (`.vos` files) enabled via `(mode vos)` in `coq.theory` stanzas. This can be used in combination with `dune coq top` to obtain fast re-building of dependencies (with no checking of proofs) prior to stepping into a file. (ocaml/dune#7406, @rlepigre) - Fix dune crashing on MacOS in watch mode whenever `$PATH` contains `$PWD` (ocaml/dune#7441, fixes ocaml/dune#6907, @rgrinberg) - Fix `dune install` when cross compiling (ocaml/dune#7410, fixes ocaml/dune#6191, @anmonteiro, @rizo) - Find `pps` dependencies in the host context when cross-compiling, (ocaml/dune#7410, fixes ocaml/dune#4156, @anmonteiro) - Dune in watch mode no longer builds concurrent rules in serial (ocaml/dune#7395 @rgrinberg, @jchavarri) - Dune can now detect Coq theories from outside the workspace. This allows for composition with installed theories (not necessarily installed with Dune). (ocaml/dune#7047, @Alizter, @ejgallego) - `dune coq top` now correctly respects the project root when called from a subdirectory. However, absolute filenames passed to `dune coq top` are no longer supported (due to being buggy) (ocaml/dune#7357, fixes ocaml/dune#7344, @rlepigre and @Alizter) - Added a `--no-build` option to `dune coq top` for avoiding rebuilds (ocaml/dune#7380, fixes ocaml/dune#7355, @Alizter) - RPC: Ignore SIGPIPE when clients suddenly disconnect (ocaml/dune#7299, ocaml/dune#7319, fixes ocaml/dune#6879, @rgrinberg) - Always clean up the UI on exit. (ocaml/dune#7271, fixes ocaml/dune#7142 @rgrinberg) - Bootstrap: remove reliance on shell. Previously, we'd use the shell to get the number of processors. (ocaml/dune#7274, @rgrinberg) - Bootstrap: correctly detect the number of processors by allowing `nproc` to be looked up in `$PATH` (ocaml/dune#7272, @Alizter) - Speed up file copying on macos by using `clonefile` when available (@rgrinberg, ocaml/dune#7210) - Adds support for loading plugins in toplevels (ocaml/dune#6082, fixes ocaml/dune#6081, @ivg, @richardlford) - Support commands that output 8-bit and 24-bit colors in the terminal (ocaml/dune#7188, @Alizter) - Speed up rule generation for libraries and executables with many modules (ocaml/dune#7187, @jchavarri) - Add `--watch-exclusions` to Dune build options (ocaml/dune#7216, @jonahbeckford) - Do not re-render UI on every frame if the UI doesn't change (ocaml/dune#7186, fix ocaml/dune#7184, @rgrinberg) - Make coq_db creation in scope lazy (@ejgallego, ocaml/dune#7133) - Non-user proccesses such as version control or config checking are now run silently. (ocaml/dune#6994, fixes ocaml/dune#4066, @Alizter) - Add the `--display-separate-messages` flag to separate the error messages produced by commands with a blank line. (ocaml/dune#6823, fixes ocaml/dune#6158, @esope) - Accept the Ordered Set Language for the `modes` field in `library` stanzas (ocaml/dune#6611, @anmonteiro). - dune install now respects --display quiet mode (ocaml/dune#7116, fixes ocaml/dune#4573, fixes ocaml/dune#7106, @Alizter) - Stub shared libraries (dllXXX_stubs.so) in Dune-installed libraries could not be used as dependencies of libraries in the workspace (eg when compiling to bytecode and/or Javascript). This is now fixed. (ocaml/dune#7151, @nojb) - Allow the main module of a library with `(stdlib ...)` to depend on other libraries (ocaml/dune#7154, @anmonteiro). - Bytecode executables built for JSOO are linked with `-noautolink` and no longer depend on the shared stubs of their dependent libraries (ocaml/dune#7156, @nojb) - Added a new user action `(concurrent )` which is like `(progn )` but runs the actions concurrently. (ocaml/dune#6933, @Alizter) - Allow `(stdlib ...)` to be used with `(wrapped false)` in library stanzas (ocaml/dune#7139, @anmonteiro). - Allow parallel execution of inline tests partitions (ocaml/dune#7012, @hhugo) - Support `(link_flags ...)` in `(cinaps ...)` stanza. (ocaml/dune#7423, fixes ocaml/dune#7416, @nojb) - Allow `(package ...)` in any position within `(rule ...)` stanza (ocaml/dune#7445, @Leonidas-from-XIV) - Always include `opam` files in the generated `.install` file. Previously, it would not be included whenever `(generate_opam_files true)` was set and the `.install` file wasn't yet generated. (ocaml/dune#7547, @rgrinberg) - Fix regression where Merlin was unable to handle filenames with uppercase letters under Windows. (ocaml/dune#7577, @nojb) - On nix+macos, pass `-f` to the codesign hook to avoid errors when the binary is already signed (ocaml/dune#7183, fixes ocaml/dune#6265, @greedy) - Fix bug where RPC clients built with dune-rpc-lwt would crash when closing their connection to the server (ocaml/dune#7581, @gridbugs) - Introduce mdx stanza 0.4 requiring mdx >= 2.3.0 which updates the default list of files to include `*.mld` files (ocaml/dune#7582, @Leonidas-from-XIV) - Fix RPC server on Windows (used for OCaml-LSP). (ocaml/dune#7666, @nojb) - Coq language versions less 0.8 are deprecated, and will be removed in an upcoming Dune version. All users are required to migrate to `(coq lang 0.8)` which provides the right semantics for theories that have been globally installed, such as those coming from opam (@ejgallego, @Alizter) - Bump minimum version of the dune language for the melange syntax extension from 3.7 to 3.8 (ocaml/dune#7665, @jchavarri)

Alizter added this to the 3.8.0 milestone Feb 12, 2023