Add script to build the GitHub Pages locally

This script is also run in the CI job

.github/workflows/ci.yml

@@ -17,6 +17,13 @@ jobs:
         name: pdfs
         path: output_pdfs
 
+  build-github-pages:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v3
+    - name: generate the GitHub Pages locally in order to check for errors
+      run: ./tools/build-github-pages.sh build
+
   markdown-link-check:
     runs-on: ubuntu-latest
     steps:

tools/build-github-pages.sh

@@ -0,0 +1,64 @@
+#!/usr/bin/env bash
+
+# SPDX-FileCopyrightText: Copyright 2023 Arm Limited and/or its affiliates <[email protected]>
+# SPDX-License-Identifier: Apache-2.0
+
+########################### BUILD GITHUB PAGES ################################
+#
+# This script uses Git and Docker to build the GitHub Pages version of the ACLE
+# project locally.
+#
+# It accepts one of two options: build or serve.
+#
+#  build generates the web pages, but does not launch a web server.
+#  serve generates them and also launches a web server.
+#
+# Once web server is launched, one can access the server using any web browser.
+# Its address is printed in the output.
+#
+###############################################################################
+
+
+if [ $# -ne 1 ]; then
+    echo "Please provide one option: 'build' or 'serve'."
+    exit 1
+fi
+
+if [ "$1" != "build" ] && [ "$1" != "serve" ]; then
+    echo "Unsupported option. It must be either 'build' or 'serve'."
+    exit 1
+fi
+
+set -x
+
+ROOTDIR=$(realpath "$(dirname "$(realpath "$0")")/..")
+TEMPDIR=$(mktemp -d)
+cd $TEMPDIR
+git clone https://github.com/github/pages-gem.git
+cd pages-gem
+make image
+cd $ROOTDIR
+echo -e "plugins:\n \
+        - jekyll-coffeescript\n \
+        - jekyll-default-layout\n \
+        - jekyll-gist\n \
+        - jekyll-github-metadata\n \
+        - jekyll-optional-front-matter\n \
+        - jekyll-paginate\n \
+        - jekyll-readme-index\n \
+        - jekyll-titles-from-headings\n \
+        - jekyll-relative-links\n" >> _config.yml
+cd $TEMPDIR/pages-gem
+
+if [ "$1" == "build" ]; then
+    SITE=$ROOTDIR
+    docker run --rm -p 4000:4000 -v `realpath ${SITE}`:/src/site gh-pages jekyll build
+elif [ "$1" == "serve" ]; then
+    SITE=$ROOTDIR make server
+fi
+
+return_code=$?
+cd $ROOTDIR
+git restore _config.yml
+
+exit $return_code

tools/howto-build-github-pages-locally.md

@@ -12,6 +12,11 @@ difficult.
 
 This document describes one process to build the GitHub page locally.
 
+## Script
+
+The script `build-github-pages.sh` contained in this same directory automates
+this process.
+
 ## Prerequisites
 
  - Docker.
@@ -52,4 +57,4 @@ Note: it has only been tested on Linux.
  5. On the terminal output, the IP and port of the web server will be shown.
    Just open it in a browser.
 
-Incremental builds can be done by starting at step 4.
+Incremental builds can be done by starting at step 4.