Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

We should have a Miri book #4108

Open
RalfJung opened this issue Dec 24, 2024 · 0 comments
Open

We should have a Miri book #4108

RalfJung opened this issue Dec 24, 2024 · 0 comments
Labels
A-docs Area: affects documentation C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement

Comments

@RalfJung
Copy link
Member

The README is getting quite long, and same for the CONTRIBUTING guide. Might be a good idea to split them both into multiple chapters, in a sort of "Miri book".

This needs a bit of infrastructure work: we'd want CI to deploy the book somewhere. Not sure what the best way is to do that. We can probably copy the setup of UCG or the lang team.
@RalfJung RalfJung mentioned this issue Dec 24, 2024
Open
@RalfJung RalfJung added C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement A-docs Area: affects documentation labels Dec 24, 2024
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
A-docs Area: affects documentation C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@RalfJung