[rocq] Support for installation of package metadata. #11945
Conversation
src/dune_rules/coq/coq_lib.ml
Outdated
| let+ theory = create_from_coqpath ~boot_id cp in | ||
| Legacy theory | ||
| let db = assert false in | ||
| let dir = assert false in |
There was a problem hiding this comment.
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.
src/dune_rules/coq/coq_lib.ml
Outdated
| ;; | ||
|
|
||
| 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)) = |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
project: DuneProject.t is the one I was having trouble with.
There was a problem hiding this comment.
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.
|
I made some progress. Now it looks like I broke the finding of plugins: |
I think this test-case is for the deprecated method of installing plugins in 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
force-pushed
the
rocq_package
branch
4 times, most recently
from
c313f84 to
0e8877f
Compare
| (** 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) = |
There was a problem hiding this comment.
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.
|
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 <[email protected]> Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ejgallego
force-pushed
the
rocq_package
branch
from
d907585 to
7e13b3e
Compare
2 participants
We now install a
rocq-packagefile 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:
Note: rebased on top of #12035
Joint work with @Lysxia