Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Generate and publish dashboard into documentation #505

Merged
merged 14 commits into from
Sep 24, 2021

Conversation

adpaco-aws
Copy link
Contributor

@adpaco-aws adpaco-aws commented Sep 22, 2021

Description of changes:

Generates and publishes the dashboard into rmc-docs, where we have included a dedicated section and the dashboard itself.

Resolved issues:

Resolves #484

Call-outs:

If approved, the dashboard step will be restricted to run in the same way as the publication step.

Testing:

  • How is this change tested? See the CI run here.

  • Is this a refactor change? No.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • 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

@tedinski tedinski left a comment

Choose a reason for hiding this comment

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

  1. I believe we discussed running the dashboard generation only on push to release?
  2. Do we have any mechanism to timeout a dashboard run overall? I'm worried if it was flaky about nontermination to start then maybe we'd need to worry about that again? I don't want to end up with github actions running for... presumably some default timeout?

@tedinski
Copy link
Contributor

Well litani didn't work, so I guess we still don't have a sense of how long it'll take in CI

ModuleNotFoundError: No module named 'dataclasses'

@adpaco-aws
Copy link
Contributor Author

In response to your questions:

  1. Yes, but I wanted to test this on the PR first (it was worth it).
  2. Unfortunately not (see Timeouts have no effect during dashboard generation #491). I was thinking maybe try tools like timeout <dashboard-command>?

Well litani didn't work, so I guess we still don't have a sense of how long it'll take in CI

ModuleNotFoundError: No module named 'dataclasses'

We are actually getting three different errors. For macOS we get the one below:

thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Os { code: 35, kind: WouldBlock, message: "Resource temporarily unavailable" }', src/tools/dashboard/src/litani.rs:93:48

I think this is due to the MacOS runner being too slow, basically.

The error on Ubuntu 20.04 is:

FileNotFoundError: [Errno 2] No such file or directory: 'dot'

Because we need to add litani dependencies.

@adpaco-aws
Copy link
Contributor Author

Okay, that worked (50 minutes). Saving the run here.

I am going to apply the final changes now.

@adpaco-aws adpaco-aws marked this pull request as ready for review September 23, 2021 18:17
@adpaco-aws adpaco-aws requested a review from tedinski September 23, 2021 18:19
@@ -0,0 +1,11 @@
# RMC Dashboard

The [RMC Dashboard](./dashboard/index.html) purpose is to show the level of support in RMC for all Rust features.
Copy link
Contributor

Choose a reason for hiding this comment

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

Nit: grammar, either "RMC Dashboard's purpose" or "the purpose of..."

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Please check the new version.

# RMC Dashboard

The [RMC Dashboard](./dashboard/index.html) purpose is to show the level of support in RMC for all Rust features.
To this end, we extract all examples from the following books:
Copy link
Contributor

Choose a reason for hiding this comment

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

Maybe more description, like "all Rust code snippet examples from the following general Rust documentation books"

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 extended it a bit but would like to extend and review this in a follow-up PR, so opened #509

@@ -14,7 +14,9 @@ DEPS=(
g++
gcc
git
gnuplot # Litani (recommended) dependency
Copy link
Contributor

Choose a reason for hiding this comment

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

Could you add a line to the README about running install_deps.sh?

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 followed @zhassan-aws advice to put this into its own script. Do you want to use install_deps.sh in our README like we do in rmc-docs?

@@ -14,7 +14,9 @@ DEPS=(
g++
gcc
git
gnuplot # Litani (recommended) dependency
Copy link
Contributor

Choose a reason for hiding this comment

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

Do we really need to add gnuplot as a dependency to RMC? It brings in a ton of other packages. Since the Installation section of the tutorial refers to install_deps.sh, can we perhaps put gnuplot in a separate install_dashboard_deps.sh that is only run in CI?

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 liked this idea so I added it. The script is only run in the workflow when the dashboard is going to be generated.

@adpaco-aws
Copy link
Contributor Author

Following @avanhatt's advice, I have updated our README to point to rmc-docs so the quickstart section is simplified and we have installation instructions in one location. You can see a preview here, let me know what you think.

@adpaco-aws adpaco-aws merged commit 6a68180 into model-checking:main Sep 24, 2021
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 22, 2022
* Generate and publish dashboard into documentation

* Add Litani deps & restrict workflow to 20.04

* Add setuptools

* Final edits

* Conform with rebase

* Install script for litani deps

* Add more docs for dashboard

* Enable dash run in CI (to be removed)

* Include dashboard deps script

* Dashboard deps permissions

* Uncomment workflow condition

* Update README quickstart section

* minor fix
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 25, 2022
* Generate and publish dashboard into documentation

* Add Litani deps & restrict workflow to 20.04

* Add setuptools

* Final edits

* Conform with rebase

* Install script for litani deps

* Add more docs for dashboard

* Enable dash run in CI (to be removed)

* Include dashboard deps script

* Dashboard deps permissions

* Uncomment workflow condition

* Update README quickstart section

* minor fix
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
* Generate and publish dashboard into documentation

* Add Litani deps & restrict workflow to 20.04

* Add setuptools

* Final edits

* Conform with rebase

* Install script for litani deps

* Add more docs for dashboard

* Enable dash run in CI (to be removed)

* Include dashboard deps script

* Dashboard deps permissions

* Uncomment workflow condition

* Update README quickstart section

* minor fix
tedinski pushed a commit that referenced this pull request Apr 27, 2022
* Generate and publish dashboard into documentation

* Add Litani deps & restrict workflow to 20.04

* Add setuptools

* Final edits

* Conform with rebase

* Install script for litani deps

* Add more docs for dashboard

* Enable dash run in CI (to be removed)

* Include dashboard deps script

* Dashboard deps permissions

* Uncomment workflow condition

* Update README quickstart section

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

Automatically generate dashboard in CI
4 participants