From a731ac4a09bf4b49fca7217ba4f72583dcae5451 Mon Sep 17 00:00:00 2001 From: Cole Schlesinger Date: Fri, 25 Oct 2024 09:46:39 -0700 Subject: [PATCH] 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 --- .github/workflows/deploy-to-web.yml | 17 ++++---- .github/workflows/test-tutorial-build.yml | 30 +++++++++++++ .gitignore | 2 + Makefile | 51 ++++++++++------------- README.md | 49 +++++++++++++++++++--- mkdocs.yml | 3 +- 6 files changed, 106 insertions(+), 46 deletions(-) create mode 100644 .github/workflows/test-tutorial-build.yml diff --git a/.github/workflows/deploy-to-web.yml b/.github/workflows/deploy-to-web.yml index 211520a6..c316f874 100644 --- a/.github/workflows/deploy-to-web.yml +++ b/.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 \ No newline at end of file + uses: actions/deploy-pages@v4 diff --git a/.github/workflows/test-tutorial-build.yml b/.github/workflows/test-tutorial-build.yml new file mode 100644 index 00000000..16324b0f --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index 74e64b36..4d1be0ad 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,5 @@ build/* /.vscode/ check **.swp +docs/exercises +docs/solutions diff --git a/Makefile b/Makefile index 07f53e90..e525def8 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index a94df9b7..89765e8a 100644 --- a/README.md +++ b/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. \ No newline at end of file +Install CN and run `make check-archive` to check all examples in the example archive. diff --git a/mkdocs.yml b/mkdocs.yml index e5f2fde6..04c49635 100644 --- a/mkdocs.yml +++ b/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: