Skip to content

Draft of initial RMC documentation#471

Merged
tedinski merged 2 commits into
model-checking:mainfrom
tedinski:initial-docs
Sep 7, 2021
Merged

Draft of initial RMC documentation#471
tedinski merged 2 commits into
model-checking:mainfrom
tedinski:initial-docs

Conversation

@tedinski

@tedinski tedinski commented Sep 3, 2021

Copy link
Copy Markdown
Contributor

Description of changes:

Some initial documentation for RMC.

Resolved issues:

N/A

Call-outs:

Nothing special.

Testing:

  • How is this change tested? -

  • Is this a refactor change? -

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • n/a Methods or procedures are documented
  • n/a Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Comment thread rmc-docs/src/getting-started.md Outdated
Comment thread rmc-docs/src/getting-started.md Outdated
Comment thread rmc-docs/src/install-guide.md Outdated
Comment thread rmc-docs/src/install-guide.md Outdated
Comment thread rmc-docs/src/install-guide.md Outdated
Comment thread rmc-docs/src/rmc-tutorial.md Outdated

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Remove 'reasonable'. Maybe start with some motivation. Why do you want to invest time learning RMC?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Did the first. I also added more context.

Comment thread rmc-docs/src/tool-comparison.md Outdated
@tedinski tedinski mentioned this pull request Sep 7, 2021
12 tasks
Comment thread rmc-docs/src/getting-started.md Outdated
Comment thread rmc-docs/src/getting-started.md Outdated
Comment thread rmc-docs/src/install-guide.md Outdated

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Maybe add that cargo will handle most of the installation for these dependencies?

Comment thread rmc-docs/src/install-guide.md Outdated
Comment thread rmc-docs/src/install-guide.md Outdated
Comment thread rmc-docs/src/install-guide.md Outdated

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Recommend adding to .bashrc/.bash_profile?

Comment thread rmc-docs/src/tool-comparison.md Outdated
Comment thread rmc-docs/src/tool-comparison.md Outdated
Comment thread rmc-docs/src/tool-comparison.md Outdated
Comment thread rmc-docs/src/tool-comparison.md Outdated
Comment thread rmc-docs/src/getting-started.md Outdated

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

property tests -> property-based tests?

Comment thread rmc-docs/src/install-guide.md Outdated
Comment thread rmc-docs/src/install-guide.md Outdated

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Is this command necessary (I don't recall running it in my initial setup). I just did that, and it's been running for over 30 minutes for me and seems to be cloning a lot of repositories:

Cloning into '/home/zyadh/rmc/firecracker'...
Cloning into '/home/zyadh/rmc/library/backtrace'...
Cloning into '/home/zyadh/rmc/library/stdarch'...
Cloning into '/home/zyadh/rmc/src/doc/book'...
Cloning into '/home/zyadh/rmc/src/doc/edition-guide'...
Cloning into '/home/zyadh/rmc/src/doc/embedded-book'...
Cloning into '/home/zyadh/rmc/src/doc/nomicon'...
Cloning into '/home/zyadh/rmc/src/doc/reference'...
Cloning into '/home/zyadh/rmc/src/doc/rust-by-example'...
Cloning into '/home/zyadh/rmc/src/doc/rustc-dev-guide'...
Cloning into '/home/zyadh/rmc/src/llvm-project'...

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I've assumed it was necessary, since our CI is doing it.

@avanhatt avanhatt left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

LGTM!

@tedinski tedinski merged commit d49f4c9 into model-checking:main Sep 7, 2021
@tedinski tedinski deleted the initial-docs branch September 7, 2021 21:22
tedinski added a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
* Draft of initial RMC documentation

* revisions in response to feedback
tedinski added a commit that referenced this pull request Apr 27, 2022
* Draft of initial RMC documentation

* revisions in response to feedback
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.

4 participants