Skip to content

Conversation

@tedinski
Copy link
Contributor

@tedinski tedinski commented Sep 9, 2021

Description of changes:

Add the first section of the RMC tutorial.

Resolved issues:

Progress towards #254

Call-outs:

  • Test case generation The source material for CBMC I'm taking inspiration from does "test case generation" but we don't seem to get this output from cbmc viewer, so I've skipped this for now.

Testing:

  • How is this change tested? The new little crate can cargo test and cargo rmc and rmc tests/final-form.rs. This currently isn't in CI. That will be deferred until later.

  • Is this a refactor change? no

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • [n/a] Methods or procedures are documented
  • 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.

Copy link
Contributor

Choose a reason for hiding this comment

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

This function might confuse people. Should we include prelude.rs instead to "hide" some of the confusion?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I sort of, kind of, hide it already, at least in that this code doesn't actually appear in the documentation.

But yes, we need to find a good way to address this. Right now it looked like there's no good way to include the prelude! The tests we have, at any rate, have to directly refer to it by relative path.

Fixing this is probably a major developer experience issue. My thought is: fix that, then revise this sample.

I create #477 to take this as a note.

Copy link
Contributor

Choose a reason for hiding this comment

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

Sounds good.

Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

Looks great!

@tedinski tedinski merged commit dff6138 into model-checking:main Sep 13, 2021
@tedinski tedinski deleted the tutorial-1 branch September 13, 2021 14:21
@tedinski tedinski mentioned this pull request Sep 14, 2021
12 tasks
tedinski added a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
* Introduce the first section of the RMC tutorial

* add license boilerplate, correct typos

* fix formatting
tedinski added a commit that referenced this pull request Apr 27, 2022
* Introduce the first section of the RMC tutorial

* add license boilerplate, correct typos

* fix formatting
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.

2 participants