Skip to content

docs: update and improve rocq documentation#14167

Merged
Alizter merged 1 commit intoocaml:mainfrom
Durbatuluk1701:rocq_docs
Apr 13, 2026
Merged

docs: update and improve rocq documentation#14167
Alizter merged 1 commit intoocaml:mainfrom
Durbatuluk1701:rocq_docs

Conversation

@Durbatuluk1701
Copy link
Copy Markdown
Contributor

This PR updates the Rocq documentation. In particular, the following changes are made:

  • Various rocq{dep, top, etc.} -> rocq {dep, top, etc.} updates (the separate Rocq binaries to Rocq subcommand changes)
  • Changes to the (stdlib {yes,no}) descriptions and clarified the Corelib vs. Stdlib behaviors
  • Other minor spacing/grammatical changes

Signed-off-by: Will Thomas <30wthomas@gmail.com>
Copy link
Copy Markdown
Collaborator

@rlepigre-skylabs-ai rlepigre-skylabs-ai left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The changes look good to me.

@Alizter Alizter merged commit 0a8424e into ocaml:main Apr 13, 2026
30 checks passed
@Durbatuluk1701 Durbatuluk1701 deleted the rocq_docs branch April 13, 2026 14:07
@Durbatuluk1701
Copy link
Copy Markdown
Contributor Author

One thing I'd thought of while doing these updates: is (stdlib ...) poorly named now? I know sometimes I am even confused because it seems like it should be including the Stdlib when in reality it is just Corelib.

Would changing its name to something like (prelude ...) or (corelib ...) make more sense?
cc. @Alizter @rlepigre-skylabs-ai

@Alizter
Copy link
Copy Markdown
Collaborator

Alizter commented Apr 13, 2026

@Durbatuluk1701 Could you create an issue about it? I am not sure how Rocq works with respect to the standard library / core library now. I don't know if such a field is still needed so it would be good to review the overall design.

@rlepigre-skylabs-ai
Copy link
Copy Markdown
Collaborator

This is still needed, but the only use-case is building Corelib itself. That is, when enabling the default dune rules in the Rocq repository as part of a composed build for example (by default Rocq uses custom rules). Perhaps the option should be set via something like (no_corelib) instead of a yes/no flag.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants