Add preliminary support for Rocq's packaging support#15400
Open
rlepigre-skylabs-ai wants to merge 1 commit into
Open
Add preliminary support for Rocq's packaging support#15400rlepigre-skylabs-ai wants to merge 1 commit into
rlepigre-skylabs-ai wants to merge 1 commit into
Conversation
Signed-off-by: Rodolphe Lepigre <rodolphe.lepigre@skylabs-ai.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds support for Rocq package support (see this rfc), which is enabled by rocq-prover/rocq#21564.
This introduces a distinction between the public name of a Rocq theory (i.e., an ocamlfind package name) and the Rocq module path under which it lives. Starting with version 0.15 of the rocq language support, Rocq theory dependencies consist of ocamlfind package names, and transitive dependencies are handled in the expected way using ocamlfind (for installed dependencies). Dependencies in the workspace are still resolved by
duneas before, and Rocq packages are installed by dune using the expected installation scheme.The changes to the
rocq.theorystanza are the following:(public_name ...)field, similar to that of(library ...)stanzas is added, and its use enables Rocq package support.(theories ...)field is populated by Rocq package names (not to be confused with module paths), and transitive dependencies are automatically added.(legacy_install)flag, if present, leads to the Rocq package being additionally installed under$LIB/coq/user-contribfor backwards compatibility.This solves #11483, and provides an alternative to #11945 (it is not entirely clear to me how the two approaches compare though).