[rocq] Support for installation of package metadata. by ejgallego · Pull Request #11945 · ocaml/dune

ejgallego · 2025-06-27T12:13:51Z

We now install a rocq-package file for each Rocq theory. This way, when Rocq developments build with Dune are globally installed, we can find out additional metadata, such as the list of their dependencies.

Fixes #11012 fixes #11483

TODO:

update changelog
update documentation

Note: rebased on top of #12035

Joint work with @Lysxia

Lysxia · 2025-06-27T16:52:43Z

src/dune_rules/coq/coq_lib.ml

-        let+ theory = create_from_coqpath ~boot_id cp in
-        Legacy theory
+        let db = assert false in
+        let dir = assert false in


@ejgallego What should those be?

dir and db are useful in the memo table as to distinguish stanzas that may appear (and be private) in different composed builds.

I think we can have a case where two identical stanzas live in two separate directories, if these are private. I'm not sure why dir is not enough here tho, I'd dare to say that stanzas are uniquely identified by the pair (dir, stanza)

We can ask Rudy once we get the patch more advanced, I guess for now we can pass db = installed_db and dir the directory we found the rocq-package file.

Lysxia · 2025-06-27T17:49:00Z

src/dune_rules/coq/coq_lib.ml

    ;;

-    let create_from_stanza_impl (coq_db, db, dir, (s : Coq_stanza.Theory.t)) =
+    let create_from_coq_package_impl (coq_db, db, dir, (s : Coq_package.meta)) =


Our initial idea was to convert a Coq_package into a Coq_stanza but some fields don't seem easy to populate, so I am trying the other way around. However this memo table relies on physical equality of Coq_stanza so I'm not sure this still works as expected.

Which fields are not easy to populate? I think we should record enough info in the Coq_package as to be able to do so.

Indeed the equality here is tricky; I'll have a look later on.

project: DuneProject.t is the one I was having trouble with.

I see! This is indeed not needed for the db, I'd suggest to make it an option for now, there are already some codepaths where we use get_exn for it.

Lysxia · 2025-06-30T21:39:57Z

I made some progress. Now it looks like I broke the finding of plugins:

File "test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/run.t", line 1, characters 0-0:
...
+  File "$TESTCASE_ROOT/lib/coq/user-contrib/Bar/rocq-package", line 3, characters 9-22:
+  3 | (plugins global.plugin)
+               ^^^^^^^^^^^^^
+  Error: Library "global.plugin" not found.
+  -> required by theory Bar in
+     $TESTCASE_ROOT/lib/coq/user-contrib/Bar/rocq-package:2
+  -> required by _build/default/.Foo.theory.d
+  -> required by alias all

ejgallego · 2025-07-01T10:01:42Z

I made some progress. Now it looks like I broke the finding of plugins:

File "test/blackbox-tests/test-cases/coq/compose-installed-plugin.t/run.t", line 1, characters 0-0:
...
+  File "$TESTCASE_ROOT/lib/coq/user-contrib/Bar/rocq-package", line 3, characters 9-22:
+  3 | (plugins global.plugin)
+               ^^^^^^^^^^^^^
+  Error: Library "global.plugin" not found.
+  -> required by theory Bar in
+     $TESTCASE_ROOT/lib/coq/user-contrib/Bar/rocq-package:2
+  -> required by _build/default/.Foo.theory.d
+  -> required by alias all

I think this test-case is for the deprecated method of installing plugins in user-contrib, so IMHO it is fine if it broken.

You could fix it by scanning the cmxs files, but given that Rocq 9 doesn't support this anymore, IMHO not worth it.

ejgallego · 2025-07-01T10:02:30Z

You could fix it by scanning the cmxs files, but given that Rocq 9 doesn't support this anymore, IMHO not worth it.

I'm sorry I'll be away for the rest of the week, but as soon as I'm back I'll rebase this on top of `(lang rocq ...) which should avoid this problem.

ejgallego · 2025-07-18T16:13:01Z

src/dune_rules/rocq/rocq_lib.ml

    (** Our final final resolve is used externally, and should return the
        library data found from the previous iterations. *)
-    let resolve rocq_db (loc, name) =
+    let resolve ~db rocq_db (loc, name) =


I think the db parameter here may not be right, note what we do for the case in Found_stanza, but I'm not a 100% sure.

In principle, it indeed seems wrong for us to resolve the OCaml plugin information with the library DB that belongs to a stanza, in this case for example, private ML libraries would be present. So I guess we should have the code to capture the right DB here.

However, this requires a bit more thinking.

Lysxia · 2025-11-17T10:50:34Z

Just rebased on main along with #12035, still wip.

We now install a `rocq-package` file for each Rocq theory. This way, when Rocq developments build with Dune are globally installed, we can find out additional metadata, such as the list of their dependencies. Fixes ocaml#11012 fixes ocaml#11483 TODO: - update changelog - update documentation Co-authored-by: Li-yao Xia <lysxia@gmail.com> Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

Lysxia · 2026-01-20T22:39:09Z

@rgrinberg Why was this closed? I thought this is supposed to fix #11483

rgrinberg · 2026-01-20T22:46:39Z

Because it seemed like the PR was abandoned. I assume you replied because you're still working on it, so I'll re-open. Anything that you're stuck on?

Lysxia · 2026-01-21T08:58:18Z

Sorry about it. I've been busy elsewhere, but I'm still interested in fixing this!

ejgallego added the coq label Jun 27, 2025

Lysxia reviewed Jun 27, 2025

View reviewed changes

Lysxia force-pushed the rocq_package branch from 91865e8 to 67863a7 Compare June 30, 2025 21:36

ejgallego added rocq and removed coq labels Jul 17, 2025

ejgallego force-pushed the rocq_package branch 4 times, most recently from c313f84 to 0e8877f Compare July 18, 2025 16:10

ejgallego commented Jul 18, 2025

View reviewed changes

ejgallego mentioned this pull request Aug 1, 2025

Empty Coq/Rocq theory leads to package error #12109

Open

Lysxia force-pushed the rocq_package branch from 0e8877f to d907585 Compare November 17, 2025 10:47

ejgallego mentioned this pull request Nov 20, 2025

[rocq] Initial support for the Rocq Prover build language #12035

Merged

8 tasks

ejgallego force-pushed the rocq_package branch from d907585 to 7e13b3e Compare November 25, 2025 21:26

ejgallego force-pushed the rocq_package branch from de1a78d to d149c5a Compare December 1, 2025 21:05

rgrinberg closed this Jan 20, 2026

rgrinberg reopened this Jan 20, 2026

Conversation

ejgallego commented Jun 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Lysxia Jun 27, 2025

Choose a reason for hiding this comment

Uh oh!

ejgallego Jun 30, 2025

Choose a reason for hiding this comment

Uh oh!

Lysxia Jun 27, 2025

Choose a reason for hiding this comment

Uh oh!

ejgallego Jun 30, 2025

Choose a reason for hiding this comment

Uh oh!

Lysxia Jun 30, 2025

Choose a reason for hiding this comment

Uh oh!

ejgallego Jul 1, 2025

Choose a reason for hiding this comment

Uh oh!

Lysxia commented Jun 30, 2025

Uh oh!

ejgallego commented Jul 1, 2025

Uh oh!

ejgallego commented Jul 1, 2025

Uh oh!

ejgallego Jul 18, 2025

Choose a reason for hiding this comment

Uh oh!

Lysxia commented Nov 17, 2025

Uh oh!

Lysxia commented Jan 20, 2026

Uh oh!

rgrinberg commented Jan 20, 2026

Uh oh!

Lysxia commented Jan 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ejgallego commented Jun 27, 2025 •

edited

Loading