Initial hello world for RMC documentation (rust-lang#456)

* Initial hello world for RMC documentation

* copyright line to our new toml file

* fix nits, add new useful readme for documentation development

Author: tedinski

.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/[email protected]
+        with:
+          branch: gh-pages
+          folder: rmc-docs/book/

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

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 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/`

rmc-docs/book.toml

@@ -0,0 +1,15 @@
+# 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)"
+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}"

rmc-docs/build-docs.sh

@@ -0,0 +1,28 @@
+#!/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 && 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"
+EXPECTED_HASH="2a0953c50d8156e84f193f15a506ef0adbac66f1942b794de5210ca9ca73dd33"
+if [ ! -x mdbook ]; then
+    curl -sSL -o "$FILE" "$URL"
+    echo "$EXPECTED_HASH $FILE" | sha256sum -c -
+    tar zxf $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."

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]()

rmc-docs/src/getting-started.md

@@ -0,0 +1,9 @@
+# Getting started with RMC
+
+Hello, World!
+
+```rust
+fn main() {
+    assert!(1 == 1);
+}
+```