feature(coq): composition of installed theories by Alizter · Pull Request #7047 · ocaml/dune

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 !

ejgallego · 2023-04-07T17:05:45Z

@ejgallego Yes, we need to version to boot flags unfortunately.

We could version that, or keep boot and add then user-contrib + coqpath by default if the lang version is less than 0.8

I guess the second apporach may be easier.

ejgallego · 2023-04-07T17:06:27Z

Let's deprecate up to 0.4 to start with.

ejgallego · 2023-04-07T17:25:20Z

Also coq-stdlib installs Ltac2 in user-contrib so that can be used to make a quick test.

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>

Alizter added this to the 3.8.0 milestone Feb 12, 2023