Update build system and CI

- building examples now places them in docs/exercises and docs/solutions rather
  than build/
- mkdocs is responsible for compiling from docs/ to build/ and depends on the
  examples already being in place (reflected in the Makefile)
- CI now tests building the tutorial in PRs
- CI has been updated to publish the new docs to GitHub Pages

Author: thatplguy

.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,30 @@
+name: Test tutorial build
+
+on:
+  pull_request:
+    types: [opened, reopened, edited]
+
+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

@@ -2,3 +2,5 @@ build/*
 /.vscode/
 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. 

mkdocs.yml

@@ -1,4 +1,5 @@
 site_name: CN Docs
+site_dir: build
 theme:
   name: material
   features:
@@ -75,7 +76,7 @@ markdown_extensions:
   - pymdownx.mark
   - pymdownx.smartsymbols
   - pymdownx.snippets:
-      base_path: ["build"]
+      base_path: ["docs", "build"]
   - pymdownx.striphtml
   - pymdownx.superfences:
       custom_fences: