From 458d00d948088f2318642953356532b6df06efc0 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Tue, 31 Aug 2021 14:52:21 +0000 Subject: [PATCH 1/5] Initial hello world for RMC documentation --- .github/workflows/rmc.yml | 13 +++++++++++++ .gitignore | 2 ++ rmc-docs/book.toml | 13 +++++++++++++ rmc-docs/build-docs.sh | 26 ++++++++++++++++++++++++++ rmc-docs/src/SUMMARY.md | 12 ++++++++++++ rmc-docs/src/getting-started.md | 9 +++++++++ 6 files changed, 75 insertions(+) create mode 100644 rmc-docs/book.toml create mode 100755 rmc-docs/build-docs.sh create mode 100644 rmc-docs/src/SUMMARY.md create mode 100644 rmc-docs/src/getting-started.md diff --git a/.github/workflows/rmc.yml b/.github/workflows/rmc.yml index 0ab4fa2ca796..1747eb5e5dd0 100644 --- a/.github/workflows/rmc.yml +++ b/.github/workflows/rmc.yml @@ -46,3 +46,16 @@ jobs: - name: Execute RMC regression run: ./scripts/rmc-regression.sh + + # On one OS only, build the documentation, too. + - name: Build Documentation + if: ${{ matrix.os == 'ubuntu-20.04' }} + run: ./rmc-docs/build-docs.sh + + # When we're pushed to main branch, only then actually publish the docs. + - name: Publish Documentation + if: ${{ matrix.os == 'ubuntu-20.04' && github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }} + uses: JamesIves/github-pages-deploy-action@4.1.4 + with: + branch: gh-pages + folder: rmc-docs/book/ diff --git a/.gitignore b/.gitignore index 0f0dfb84b5c8..b2a0099fb5f2 100644 --- a/.gitignore +++ b/.gitignore @@ -82,3 +82,5 @@ src/test/rustdoc-gui/src/**.lock /src/test/dashboard *Cargo.lock src/test/rmc-dependency-test/diamond-dependency/build +/rmc-docs/book +/rmc-docs/mdbook* diff --git a/rmc-docs/book.toml b/rmc-docs/book.toml new file mode 100644 index 000000000000..ad715e0f72b4 --- /dev/null +++ b/rmc-docs/book.toml @@ -0,0 +1,13 @@ +[book] +title = "The Rust Model Checker" +description = "Documentation for the Rust Model Checker (RMC)" +authors = ["RMC Developers"] +src = "src" +language = "en" +multilingual = false + +[output.html] +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}" diff --git a/rmc-docs/build-docs.sh b/rmc-docs/build-docs.sh new file mode 100755 index 000000000000..83d84de50697 --- /dev/null +++ b/rmc-docs/build-docs.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" +cd $SCRIPT_DIR + +# 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" +if [ ! -x mdbook ]; then + wget -O "$FILE" "$URL" + tar zxvf $FILE +fi + +# Build the book into ./book/ +mkdir -p book +./mdbook build +touch book/.nojekyll + +# TODO: Test all the code examples from our documentation +# TODO: Build the dashboard and publish into our documentation + +echo "Finished documentation build successfully." diff --git a/rmc-docs/src/SUMMARY.md b/rmc-docs/src/SUMMARY.md new file mode 100644 index 000000000000..fe81e25e629d --- /dev/null +++ b/rmc-docs/src/SUMMARY.md @@ -0,0 +1,12 @@ +# The Rust Model Checker + +- [Getting started with RMC](./getting-started.md) + - [Installation]() + - [Comparison with other tools]() + - [RMC on a single file]() + - [RMC on a crate]() + - [Debugging failures]() + +- [RMC tutorial]() + +- [RMC developer documentation]() diff --git a/rmc-docs/src/getting-started.md b/rmc-docs/src/getting-started.md new file mode 100644 index 000000000000..08cb68c61a9c --- /dev/null +++ b/rmc-docs/src/getting-started.md @@ -0,0 +1,9 @@ +# Getting started with RMC + +Hello, World! + +``` +fn main() { + assert!(1 == 1); +} +``` From d3e88c7d62791e61fe278da8ca4413f2aafd4611 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Tue, 31 Aug 2021 16:49:24 +0000 Subject: [PATCH 2/5] Ignore toml files in copyright check --- .github/workflows/copyright.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/copyright.yml b/.github/workflows/copyright.yml index a2d69c300021..d8e6375d7b85 100644 --- a/.github/workflows/copyright.yml +++ b/.github/workflows/copyright.yml @@ -15,7 +15,7 @@ jobs: - name: Get paths for files added id: git-diff run: | - ignore='(.diff|.md|.props|expected|ignore|gitignore)$' + ignore='(.toml|.diff|.md|.props|expected|ignore|gitignore)$' files=$(git diff --ignore-submodules=all --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -v -E $ignore | xargs) echo "::set-output name=paths::$files" From 1a2fa2ac39ef85f528e235b6f39bd1d0208b8908 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Tue, 31 Aug 2021 19:03:53 +0000 Subject: [PATCH 3/5] revert adding toml to the ignore list, and just add the copyright line to our new toml file --- .github/workflows/copyright.yml | 2 +- rmc-docs/book.toml | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/copyright.yml b/.github/workflows/copyright.yml index d8e6375d7b85..a2d69c300021 100644 --- a/.github/workflows/copyright.yml +++ b/.github/workflows/copyright.yml @@ -15,7 +15,7 @@ jobs: - name: Get paths for files added id: git-diff run: | - ignore='(.toml|.diff|.md|.props|expected|ignore|gitignore)$' + ignore='(.diff|.md|.props|expected|ignore|gitignore)$' files=$(git diff --ignore-submodules=all --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -v -E $ignore | xargs) echo "::set-output name=paths::$files" diff --git a/rmc-docs/book.toml b/rmc-docs/book.toml index ad715e0f72b4..065ead741e86 100644 --- a/rmc-docs/book.toml +++ b/rmc-docs/book.toml @@ -1,3 +1,5 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT [book] title = "The Rust Model Checker" description = "Documentation for the Rust Model Checker (RMC)" From 9f926584bec452c189eb930129f1b09ad7dc7796 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Tue, 31 Aug 2021 19:05:53 +0000 Subject: [PATCH 4/5] fix nits, add new useful readme for documentation development --- rmc-docs/README.md | 10 ++++++++++ rmc-docs/build-docs.sh | 6 ++++-- rmc-docs/src/getting-started.md | 2 +- 3 files changed, 15 insertions(+), 3 deletions(-) create mode 100644 rmc-docs/README.md diff --git a/rmc-docs/README.md b/rmc-docs/README.md new file mode 100644 index 000000000000..3a8ea0cca0a1 --- /dev/null +++ b/rmc-docs/README.md @@ -0,0 +1,10 @@ +## RMC documentation development + +A good trick when developing RMC on a remote machine is to SSH forward to test documentation changes. + +``` +ssh -t -L 3000:127.0.0.1:3000 rmc-host 'cd rmc/rmc-docs/ && ./mdbook serve' +``` + +This command will connect to `rmc-host` where it assumes RMC is checked out in `rmc/` and the documentation has been build once successfully. +It will automatically detect changes to the docs and rebuild, allowing you to quickly refresh in your browser when you visit: `http://127.0.0.1:3000/` diff --git a/rmc-docs/build-docs.sh b/rmc-docs/build-docs.sh index 83d84de50697..e0b1a3c44713 100755 --- a/rmc-docs/build-docs.sh +++ b/rmc-docs/build-docs.sh @@ -10,9 +10,11 @@ cd $SCRIPT_DIR # 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" +EXPECTED_HASH="2a0953c50d8156e84f193f15a506ef0adbac66f1942b794de5210ca9ca73dd33" if [ ! -x mdbook ]; then - wget -O "$FILE" "$URL" - tar zxvf $FILE + curl -sSL -o "$FILE" "$URL" + echo "$EXPECTED_HASH $FILE" | sha256sum -c - + tar zxf $FILE fi # Build the book into ./book/ diff --git a/rmc-docs/src/getting-started.md b/rmc-docs/src/getting-started.md index 08cb68c61a9c..662c25f86754 100644 --- a/rmc-docs/src/getting-started.md +++ b/rmc-docs/src/getting-started.md @@ -2,7 +2,7 @@ Hello, World! -``` +```rust fn main() { assert!(1 == 1); } From f9402d5f0e5f2face31e909dc2e186d531e42ad2 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Wed, 1 Sep 2021 13:54:51 +0000 Subject: [PATCH 5/5] fix typos --- rmc-docs/README.md | 4 ++-- rmc-docs/build-docs.sh | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/rmc-docs/README.md b/rmc-docs/README.md index 3a8ea0cca0a1..2ba0528e9ffd 100644 --- a/rmc-docs/README.md +++ b/rmc-docs/README.md @@ -6,5 +6,5 @@ A good trick when developing RMC on a remote machine is to SSH forward to test d ssh -t -L 3000:127.0.0.1:3000 rmc-host 'cd rmc/rmc-docs/ && ./mdbook serve' ``` -This command will connect to `rmc-host` where it assumes RMC is checked out in `rmc/` and the documentation has been build once successfully. -It will automatically detect changes to the docs and rebuild, allowing you to quickly refresh in your browser when you visit: `http://127.0.0.1:3000/` +This command will connect to `rmc-host` where it assumes RMC is checked out in `rmc/` and the documentation has been built once successfully. +It will automatically detect changes to the docs and rebuild, allowing you to quickly refresh in your local browser when you visit: `http://127.0.0.1:3000/` diff --git a/rmc-docs/build-docs.sh b/rmc-docs/build-docs.sh index e0b1a3c44713..7a0e4fb2d947 100755 --- a/rmc-docs/build-docs.sh +++ b/rmc-docs/build-docs.sh @@ -4,7 +4,7 @@ set -eu -SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" cd $SCRIPT_DIR # Download mdbook release (vs spending time building it via cargo install)