Convert from AsciiDoctor to Material for MkDocs (#80)

.github/workflows/deploy-to-web.yml

@@ -22,23 +22,20 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v3
 
-      - name: Set up Ruby
-        uses: ruby/setup-ruby@v1
+      - name: Set up Python
+        uses: actions/setup-python@v5
         with:
-          ruby-version: '2.7' 
+          python-version: 3.x
 
-      - name: Install AsciiDoctor
-        run: gem install asciidoctor pygments.rb
+      - name: Install Material for MkDocs
+        run: pip install mkdocs-material
 
       - name: Clean the build directory 
-        run: rm -rf build/* 
+        run: make clean
 
       - name: Build the tutorial 
         run: make 
 
-      - name: Move the tutorial file 
-        run: mv build/tutorial.html build/index.html  
-
       - name: Setup Pages
         uses: actions/configure-pages@v5
 
@@ -49,4 +46,4 @@ jobs:
 
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v4
+        uses: actions/deploy-pages@v4

.github/workflows/test-tutorial-build.yml

@@ -0,0 +1,29 @@
+name: Test tutorial build
+
+on:
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: 3.x 
+
+      - name: Install Material for MkDocs
+        run: pip install mkdocs-material
+
+      - name: Clean the build directory 
+        run: make clean
+
+      - name: Check that the tutorial builds
+        run: make

.gitignore

@@ -1,3 +1,6 @@
 build/*
 /.vscode/
-check
+check
+**.swp
+docs/exercises
+docs/solutions

Makefile

@@ -2,34 +2,33 @@
 
 MAKEFILE_DIR:=$(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
-default: build exercises build/tutorial.html build/exercises.zip
+default: tutorial
 all: default
 
 clean:
-	rm -rf build TAGS
-
-build:
-	mkdir -p build
-	mkdir -p build/exercises
-	mkdir -p build/solutions
+	rm -rf docs/exercises docs/solutions docs/exercises.zip build TAGS
 
 ##############################################################################
 # Exercises
 
 SRC_EXAMPLES=$(shell find src/examples -type f)
-SOLUTIONS=$(patsubst src/examples/%, build/solutions/%, $(SRC_EXAMPLES))
-EXERCISES=$(patsubst src/examples/%, build/exercises/%, $(SRC_EXAMPLES))
+SOLUTIONS=$(patsubst src/examples/%, docs/solutions/%, $(SRC_EXAMPLES))
+EXERCISES=$(patsubst src/examples/%, docs/exercises/%, $(SRC_EXAMPLES))
 
 CN=cn verify
 
-exercises: $(EXERCISES) $(SOLUTIONS)
+exercises: docs-exercises-dirs $(EXERCISES) $(SOLUTIONS)
+
+docs-exercises-dirs:
+	mkdir -p docs/exercises
+	mkdir -p docs/solutions
 
-build/exercises/%: src/examples/%
+docs/exercises/%: src/examples/%
 	@echo Rebuild $@
 	@-mkdir -p $(dir $@)
 	@sed -E '\|^.*--BEGIN--.*$$|,\|^.*--END--.*$$|d' $< > $@
 
-build/solutions/%: src/examples/%
+docs/solutions/%: src/examples/%
 	@-mkdir -p $(dir $@)
 	@if [ `which cn` ]; then \
 	  if [[ "$<" = *".c"* ]]; then \
@@ -41,16 +40,15 @@ build/solutions/%: src/examples/%
 	@echo Rebuild $@
 	@cat $< | sed '\|^.*--BEGIN--.*$$|d' | sed '\|^.*--END--.*$$|d' > $@
 
-build/exercises.zip: $(EXERCISES)
-	cd build; zip -r exercises.zip exercises > /dev/null
+docs/exercises.zip: $(EXERCISES)
+	cd docs; zip -r exercises.zip exercises > /dev/null
 
 WORKING=$(wildcard src/examples/list_*.c)
-WORKING_AUX=$(patsubst src/examples/%, build/solutions/%, $(WORKING))
-temp: $(WORKING_AUX) build 
-#     build/tutorial.html 
+WORKING_AUX=$(patsubst src/examples/%, docs/solutions/%, $(WORKING))
+temp: $(WORKING_AUX) docs-exercises-dirs
 
 ##############################################################################
-# Check that the examples all run correctly 
+# Check that the examples all run correctly
 
 CN_PATH?=cn verify
 
@@ -62,23 +60,16 @@ check-tutorial:
 	@echo Check tutorial examples
 	@$(MAKEFILE_DIR)/check.sh "$(CN_PATH)"
 
-check: check-tutorial check-archive 
+check: check-tutorial check-archive
 
 ##############################################################################
 # Tutorial document
 
-build/tutorial.adoc build/style.css build/asciidoctor.css: src/tutorial.adoc
-	@echo Create build/tutorial.adoc
-	@sed -E 's/include_example\((.+)\)/.link:\1[\1]\n[source,c]\n----\ninclude::\1\[\]\n----/g' $< > $@
-	@cp src/style.css build
-	@cp src/asciidoctor.css build
-
-build/images: src/images
-	cp -r $< $@
+tutorial: exercises mkdocs.yml $(shell find docs -type f)
+	mkdocs build --strict
 
-build/tutorial.html: build/tutorial.adoc $(SRC_EXAMPLES) build/images
-	asciidoctor --doctype book $< -o $@
-	@rm build/tutorial.adoc
+serve: exercises mkdocs.yml $(shell find docs -type f)
+	mkdocs serve
 
 ##############################################################################
 # Misc

README.md

@@ -4,16 +4,55 @@ View the tutorial here: https://rems-project.github.io/cn-tutorial/
 
 ## Building
 
+The CN tutorial is built using [Material for
+MkDocs](https://squidfunk.github.io/mkdocs-material/).
+
+Dependencies:
+* python 3.x
+* pip
+
+```bash
+# Install Material for MkDocs
+pip install mkdocs-material
+
+# Build the tutorial
+make
+```
+
+### Hosting locally
+
+You can start a local server that automatically renders changes to the tutorial
+files.  This is useful while editing the tutorial.
+
+```bash
+# Run the docs locally
+make serve
+```
+
+View at: http://localhost:8000/
+
 Install dependencies: [asciidoctor](https://asciidoctor.org/).
 
-Run `make` to produce `build/tutorial.html` and its dependencies: especially, `build/exercises/*.c` and `build/solutions/*c`.
+## Tutorial examples
+
+The tutorial examples live in [src/examples](./src/examples).
+
+As part of building the tutorial, the examples are lightly preprocessed to
+produce solutions and exercises (solutions with the CN specifications removed).
+
+Run `make exercises` to produce the exercises and solutions in the `docs`
+directory.
+
+### Testing the tutorial examples
 
-Run `make check-tutorial` to check that all examples in the tutorial have working solutions (except tests with names `*.broken.c`, which are expected to fail). Note that this step will not work until after you have installed CN, which is the first part of the tutorial.
+Follow these steps `make check-tutorial` to check that all examples in the tutorial have working solutions (except tests with names `*.broken.c`, which are expected to fail).
 
-Run `make check` to checks both the tutorial and archive examples (see below). 
+1. Install CN (follow steps in [the tutorial](https://rems-project.github.io/cn-tutorial/
+))
+2. Run `make check-tutorial`
 
-## CN Example Archive 
+## CN example archive 
 
 The subdirectory `src/example-archive` includes many more examples of CN proofs, both working and broken. See [the README](./src/example-archive/README.md) for a description how these examples are organized. 
 
-Run `make check-archive` to check all examples in the example archive. 
+Install CN and run `make check-archive` to check all examples in the example archive. 

docs/README.md

@@ -0,0 +1,83 @@
+# Welcome to CN
+
+CN is an extension of the C programming language for testing and verifying the
+correctness of C code, especially on low-level systems code. Compared to
+standard C, CN checks not only that expressions and statements follow the
+correct typing discipline for C-types, but also that the C code executes
+_safely_ — does not raise C undefined behaviour — and _correctly_ — satisfying
+to strong, user-defined specifications.
+
+CN provides utilities for verifying specifications at compile time as well as
+automatically generating unit and integration tests to test specifications at
+runtime.
+
+This documentation is a work in progress -- your suggestions are greatly
+appreciated!
+
+<div class="grid cards" markdown>
+
+-   :material-clock-fast:{ .lg .middle } __Set up in 5 minutes__
+
+    ---
+
+    Build and install CN and get up and running in minutes
+
+    [:octicons-arrow-right-24: Installing CN](getting-started/installation.md)
+
+-   :fontawesome-brands-markdown:{ .lg .middle } __Your first spec__
+
+    ---
+
+    Check out the Hello World tutorial to write, test, and verify your first
+    spec
+
+    [:octicons-arrow-right-24: Hello World](getting-started/hello-world.md)
+
+-   :material-format-font:{ .lg .middle } __Tutorials__
+
+    ---
+
+    Find tutorials covering common tasks and introducing CN features
+
+    [:octicons-arrow-right-24: Tutorials](getting-started/tutorials/README.md)
+
+-   :material-scale-balance:{ .lg .middle } __Language reference__
+
+    ---
+
+    Quick reference for CN specification syntax
+
+    [:octicons-arrow-right-24: Language reference](reference/README.md)
+
+</div>
+
+## Origins
+CN was first described in [CN: Verifying Systems C Code with Separation-Logic Refinement Types](https://dl.acm.org/doi/10.1145/3571194) by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami.
+To accurately handle the complex semantics of C, CN builds on the [Cerberus semantics for C](https://github.com/rems-project/cerberus/).
+Some of the examples in this tutorial are adapted from Arthur Charguéraud’s excellent
+[Separation Logic Foundations](https://softwarefoundations.cis.upenn.edu) textbook, and one of the case studies is based on an
+extended exercise due to Bryan Parno.
+
+## Acknowledgment of Support and Disclaimer
+This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google. The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
+
+## Building these docs
+
+These docs are built with [Material for
+MkDocs](https://squidfunk.github.io/mkdocs-material/).  To build and serve them
+locally on http://localhost:8000:
+
+```bash
+# Install Material for MkDocs
+pip install mkdocs-material
+
+# In the cn-tutorial root directory, run
+mkdocs serve
+```
+
+## Docs layout
+
+    mkdocs.yml    # The configuration file.
+    docs/
+        README.md # The documentation homepage.
+        ...       # Other markdown pages, images and other files.