Update installation guide to include rmc lib build#604
Update installation guide to include rmc lib build#604celinval merged 4 commits intomodel-checking:mainfrom
Conversation
|
Do you plan on updating the rest of the documentation (e.g. https://github.com/model-checking/rmc/blob/main/rmc-docs/src/dev-documentation.md and https://github.com/model-checking/rmc/blob/main/rmc-docs/src/tutorial-first-steps.md) in a separate PR? |
I can add this to the dev-documentation.md. And I'll replace |
| } | ||
|
|
||
| fn __nondet() -> u32 { | ||
| fn rmc::nondet() -> u32 { |
There was a problem hiding this comment.
You probably meant to remove this function.
There was a problem hiding this comment.
yep... thanks for catching it.
Forgot to remove one nondet definition.
| ([`--keep-stage` comes with caveats](https://rustc-dev-guide.rust-lang.org/building/suggested.html#incremental-builds-with---keep-stage). Know that it may cause spurious build failures.) | ||
| ```bash | ||
| # Build rmc crate | ||
| ./scripts/setup/rmc_build_lib.sh |
There was a problem hiding this comment.
Can we make this part of x.py in the rmc case?
There was a problem hiding this comment.
I debated about this one. I wanted to start untangling ourselves from the bootstrap script. My goal is to actually enhance this script to also compile an RMC friendly std library.
There was a problem hiding this comment.
I'll merge as is since this is documenting what's been pushed already. If you prefer I can modify the bootstrap script to build the RMC library and I can update this doc again. Just let me know and I can create a follow up PR.
Update documentation after adding rmc crate
3 participants
Description of changes:
On #597 we introduced an RMC crate. This change is to update the document to reflect the steps needed to build this crate.
Resolved issues:
Call-outs:
Testing:
How is this change tested?
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.