Initial hello world for RMC documentation by tedinski · Pull Request #456 · model-checking/kani

tedinski · 2021-08-31T15:03:19Z

Description of changes:

This introduces:

A candidate CI process for building/publishing RMC documentation.
"Hello world" and nothing more to push there.

Resolved issues:

N/A

Call-outs:

The GitHub Actions documentations is deeply confusing about permissions. This PR will be able to test the building of the documentation, but not the publishing of it. We may well have to merge it to find out if that part works or not! (I have several hypotheses about what's going to happen when we try, none of them confirmed or refuted by any documentation I can find.)
This just tacks the documentation build onto the end of the ubuntu-20.04 build, instead of as its own workflow. This is because we want to (not in this PR, but in a later PR) use RMC to test the code examples in the documentation, as well as build and publish Abdal's dashboard. This means we need RMC built and ready to run, so we might as well piggy back on an existing build. (Later, when we have releases of RMC available to download, we can probably separate documentation publishing into its own workflow, instead of piggybacking like this.)

Testing:

How is this change tested? We'll have to merge it to see! :(
Is this a refactor change? -

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.

celinval

Thanks for doing this!

celinval · 2021-08-31T18:16:51Z

Is there any other way to publish github doc? In my previous team, this branch blew up once people added images to the doc. Another possibility is that we could also add a check here to make sure we are not pushing binary files.

The only binary files are the fonts from the mdbook theme. These should change rarely, if ever, and only with changes the to the version of mdbook we're using.

I think this will be fine, but the custom action does have a single-commit option that ensures the gh-pages branch has history wiped out automatically. I don't plan on turning this on for now, but if this becomes a problem in the future, we could switch to using that.

That's fair. Thanks for checking.

Should we branch protect that branch, so only actions can update it

celinval · 2021-08-31T18:20:57Z

Can we download this in a folder outside of the script directory?

There isn't really anyplace better to put it that I can think of.

You could put it in the current directory, temp or take the directory as a parameter. It's not a blocker but a nice to have. It keeps the repository clean.

…e to our new toml file

danielsn · 2021-09-03T14:39:32Z

Should we branch protect that branch, so only actions can update it

danielsn · 2021-09-03T14:40:27Z

+site-url = "/rmc/"
+git-repository-url = "https://github.com/model-checking/rmc"
+# If we get a stable default branch, we can use this feature, but HEAD doesn't work
+#edit-url-template = "https://github.com/model-checking/rmc/edit/HEAD/rmc-docs/{path}"


uncomment this

danielsn · 2021-09-03T14:41:05Z

+
+# Download mdbook release (vs spending time building it via cargo install)
+FILE="mdbook-v0.4.12-x86_64-unknown-linux-gnu.tar.gz"
+URL="https://github.com/rust-lang/mdBook/releases/download/v0.4.12/$FILE"


is there a good way to keep up to date with new releases

there was a suggestion to use the mdbook action

* Initial hello world for RMC documentation * copyright line to our new toml file * fix nits, add new useful readme for documentation development

tedinski mentioned this pull request Aug 31, 2021

Training material #254

Closed

12 tasks

tedinski force-pushed the new-docs branch from ab10c4b to 6294442 Compare August 31, 2021 16:49

celinval reviewed Aug 31, 2021

View reviewed changes

zhassan-aws reviewed Aug 31, 2021

View reviewed changes

Comment thread rmc-docs/build-docs.sh Outdated

zhassan-aws reviewed Aug 31, 2021

View reviewed changes

Comment thread rmc-docs/README.md Outdated

tedinski added 4 commits September 2, 2021 18:02

Initial hello world for RMC documentation

458d00d

Ignore toml files in copyright check

d3e88c7

revert adding toml to the ignore list, and just add the copyright lin…

1a2fa2a

…e to our new toml file

fix nits, add new useful readme for documentation development

9f92658

tedinski force-pushed the new-docs branch from 545b66c to 61998a6 Compare September 2, 2021 18:03

tedinski changed the base branch from main-154-2021-08-24 to main September 2, 2021 18:03

fix typos

f9402d5

tedinski force-pushed the new-docs branch from 61998a6 to f9402d5 Compare September 2, 2021 18:14

Merge branch 'main' into new-docs

f6a8984

danielsn approved these changes Sep 3, 2021

View reviewed changes

tedinski merged commit d7b4182 into model-checking:main Sep 3, 2021

tedinski deleted the new-docs branch September 3, 2021 18:46

tedinski added a commit that referenced this pull request Apr 27, 2022

Initial hello world for RMC documentation (#456)

2e5e7cb

* Initial hello world for RMC documentation * copyright line to our new toml file * fix nits, add new useful readme for documentation development

Conversation

tedinski commented Aug 31, 2021

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants