feat(doc): Build and publish the documentation on GitHub Pages

.github/workflows/ci.yml

@@ -8,19 +8,23 @@ on:
   workflow_dispatch:
   merge_group:
 
-# cancel in-progress job when a new push is performed (except on main)
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: ${{ !contains(github.ref, 'main')}}
 
 jobs:
   build:
     runs-on: ubuntu-24.04
+    permissions:
+      contents: read
+
+    # Cancels in-progress job when a new push is performed (except on main)
+    concurrency:
+      group: build-${{ github.ref }}
+      cancel-in-progress: ${{ !contains(github.ref, 'main')}}
+
 
     steps:
 
     - name: Checkout
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Install system dependencies (ubuntu)
       run: |
@@ -47,7 +51,7 @@ jobs:
       uses: actions/cache/restore@v4
       with:
         path: ~/.opam
-        key: locked-${{ hashFiles('*.opam.locked') }}
+        key: locked-doc-${{ hashFiles('*.opam.locked') }}
 
     - name: Initialize OPAM
       if: ${{ steps.cache-opam-restore.outputs.cache-hit != 'true' }}
@@ -67,7 +71,7 @@ jobs:
     - name: Install OPAM dependencies
       if: ${{ steps.cache-opam-restore.outputs.cache-hit != 'true' }}
       run: |
-        opam install . --deps-only --locked --with-test --with-dev-setup --confirm-level=unsafe-yes
+        opam install . --deps-only --locked --with-test --with-dev-setup --with-doc --confirm-level=unsafe-yes
 
     - name: Clean OPAM folder for caching
       if: ${{ steps.cache-opam-restore.outputs.cache-hit != 'true' }}
@@ -83,7 +87,7 @@ jobs:
       if: ${{ steps.cache-opam-restore.outputs.cache-hit != 'true' }}
       with:
         path: ~/.opam
-        key: locked-${{ hashFiles('*.opam.locked') }}
+        key: locked-doc-${{ hashFiles('*.opam.locked') }}
 
     - name: Build
       run: |
@@ -106,3 +110,42 @@ jobs:
         eval $(opam env)
         make headers
         git diff --quiet
+
+    - name: Build documentation
+      run: |
+        opam exec -- dune build @doc
+
+    - name: Assemble documentation site
+      run: |
+        ./etc/mk-doc-site.sh _site
+
+    - name: Upload GitHub Pages artifact
+      if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }}
+      uses: actions/upload-pages-artifact@v3
+      with:
+        path: _site
+
+  # Publishes the documentation on https://rems-project.github.io/archsem/
+  deploy-docs:
+    needs: build
+    if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }}
+    runs-on: ubuntu-24.04
+
+    permissions:
+      pages: write
+      id-token: write
+
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+
+    # Never run two Pages deployments at once, and never cancel one halfway
+    concurrency:
+      group: pages
+      cancel-in-progress: false
+
+    steps:
+
+    - name: Deploy to GitHub Pages
+      id: deployment
+      uses: actions/deploy-pages@v4

.gitignore

@@ -11,3 +11,4 @@ _build
 _opam
 .envrc
 .vscode
+_site

Makefile

@@ -1,6 +1,6 @@
 # This Makefile is provided for people that prefer to type
 # "make" instead of "dune build"
-.PHONY : all clean doc archive headers
+.PHONY : all test clean doc doc-site serve-doc-site archive headers
 all:
 	dune build
 
@@ -14,10 +14,21 @@ GIT_ARCHIVE=git archive
 clean:
 	dune clean
 	rm -f $(TARBALL)
+	rm -rf _site
+
 
 doc:
 	dune build @doc
 
+doc-site: doc
+	./etc/mk-doc-site.sh _site
+
+DOC_SITE_PORT ?= 8000
+serve-doc-site: doc-site
+	@echo "Serving documentation on http://localhost:$(DOC_SITE_PORT)/ (Ctrl-C to stop)"
+	@python3 -m http.server $(DOC_SITE_PORT) -b 127.0.0.1 --directory _site
+
+
 DIRS=Common
 DIRS+=ArchSem
 DIRS+=ArchSemArm

README.md

@@ -119,14 +119,12 @@ particular `cdestruct` is in [Common/CDestruct.v](Common/CDestruct.v).
 
 ## Documentation
 
-To build the documentation call `dune build @doc` and then the documentation
-will be generated in:
-
-- `_build/default/Common/ASCommon.html/toc.html`
-- `_build/default/ArchSem/ArchSem.html/toc.html`
-- `_build/default/ArchSemArm/ArchSemArm.html/toc.html`
-- `_build/default/ArchSemRiscV/ArchSemRiscV.html/toc.html`
-- `_build/default/ArchSemX86/ArchSemX86.html/toc.html`
+The documentation of the `main` branch is published at
+<https://rems-project.github.io/archsem/>.
+
+To build it locally, do `dune build @doc`. It will live in various places in 
+`_build`. You can assemble the documentation webside with `make doc-site` and
+serve it locally with `make serve-doc-site`
 
 
 ## Current limitations

etc/doc-index.html

@@ -0,0 +1,186 @@
+<!DOCTYPE html>
+<html lang="en">
+
+<head>
+<meta charset="utf-8"/>
+<meta name="viewport" content="width=device-width, initial-scale=1.0"/>
+<title>ArchSem documentation</title>
+
+<!-- Claude autogenerated CSS (in particular the colors), sorry -->
+<style>
+:root {
+  --bg: #ffffff;
+  --fg: #1c1c1c;
+  --muted: #5d6470;
+  --rule: #e2e5ea;
+  --card: #f7f8fa;
+  --link: #1a4f8a;
+}
+@media (prefers-color-scheme: dark) {
+  :root {
+    --bg: #16181c;
+    --fg: #e6e8ec;
+    --muted: #9aa2af;
+    --rule: #2c3038;
+    --card: #1e2127;
+    --link: #7ab3f0;
+  }
+}
+* { box-sizing: border-box; }
+body {
+  margin: 0;
+  padding: 2.5rem 1.5rem 4rem;
+  background: var(--bg);
+  color: var(--fg);
+  font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto,
+               "Helvetica Neue", Arial, sans-serif;
+  line-height: 1.6;
+}
+main { max-width: 53rem; margin: 0 auto; }
+header { border-bottom: 1px solid var(--rule); padding-bottom: 1.5rem; }
+header img { max-width: 100%; height: auto; display: block; }
+h1 { font-size: 1.9rem; margin: 1.25rem 0 0.5rem; }
+h2 {
+  font-size: 1.15rem;
+  margin: 2.5rem 0 0.25rem;
+  text-transform: uppercase;
+  letter-spacing: 0.06em;
+  color: var(--muted);
+}
+p { margin: 0.5rem 0; }
+a { color: var(--link); }
+.subtitle { color: var(--muted); }
+ul { list-style: none; margin: 1rem 0 0; padding: 0; }
+li {
+  background: var(--card);
+  border: 1px solid var(--rule);
+  border-radius: 6px;
+  padding: 0.85rem 1rem;
+  margin-bottom: 0.6rem;
+}
+li .name { font-weight: 600; font-size: 1.02rem; }
+li .name code {
+  font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace;
+  font-size: 1rem;
+}
+li .desc { color: var(--muted); font-size: 0.92rem; margin: 0.15rem 0 0.4rem; }
+li .links { font-size: 0.9rem; }
+li .links a + a { margin-left: 1rem; }
+footer {
+  margin-top: 3rem;
+  padding-top: 1.25rem;
+  border-top: 1px solid var(--rule);
+  color: var(--muted);
+  font-size: 0.88rem;
+}
+</style>
+
+</head>
+
+
+
+<body>
+<main>
+
+<header>
+  <img src="archsem_logo.png" alt="ArchSem logo" width="420"/>
+  <h1>ArchSem documentation</h1>
+  <p class="subtitle">
+    ArchSem is a Rocq framework to define the semantics of CPU architectures
+    such as Arm-A, RISC-V, and x86, integrating their concurrency models &mdash;
+    written in Rocq &mdash; and instruction-set semantics &mdash; written in Sail.
+  </p>
+  <p class="subtitle">
+    <a href="https://github.com/rems-project/archsem">GitHub repository</a>
+    &middot;
+    <a href="https://www.cl.cam.ac.uk/~pes20/Stuff/2025-archsem-paper.pdf">POPL
+    2026 paper</a>
+  </p>
+</header>
+
+<h2>Rocq theories</h2>
+<p class="subtitle">
+  Generated with coqdoc. The <em>contents</em> link is the table of contents of
+  the theory; <em>index</em> is the alphabetical index of its identifiers.
+</p>
+<ul>
+  <li>
+    <div class="name"><code>ASCommon</code></div>
+    <div class="desc">
+      Common infrastructure and definitions for the ArchSem project, including
+      CDestruct and a free monad library.
+    </div>
+    <div class="links">
+      <a href="rocq/Common/ASCommon.html/toc.html">contents</a>
+      <a href="rocq/Common/ASCommon.html/index.html">index</a>
+    </div>
+  </li>
+  <li>
+    <div class="name"><code>ArchSem</code></div>
+    <div class="desc">
+      The architecture-generic part: the ISA/concurrency interface, candidate
+      executions, and the generic model constructions.
+    </div>
+    <div class="links">
+      <a href="rocq/ArchSem/ArchSem.html/toc.html">contents</a>
+      <a href="rocq/ArchSem/ArchSem.html/index.html">index</a>
+    </div>
+  </li>
+  <li>
+    <div class="name"><code>ArchSemArm</code></div>
+    <div class="desc">The Arm-A instantiation and its concurrency models.</div>
+    <div class="links">
+      <a href="rocq/ArchSemArm/ArchSemArm.html/toc.html">contents</a>
+      <a href="rocq/ArchSemArm/ArchSemArm.html/index.html">index</a>
+    </div>
+  </li>
+  <li>
+    <div class="name"><code>ArchSemRiscV</code></div>
+    <div class="desc">The RISC-V instantiation and its concurrency models.</div>
+    <div class="links">
+      <a href="rocq/ArchSemRiscV/ArchSemRiscV.html/toc.html">contents</a>
+      <a href="rocq/ArchSemRiscV/ArchSemRiscV.html/index.html">index</a>
+    </div>
+  </li>
+  <li>
+    <div class="name"><code>ArchSemX86</code></div>
+    <div class="desc">The x86 instantiation and its concurrency models.</div>
+    <div class="links">
+      <a href="rocq/ArchSemX86/ArchSemX86.html/toc.html">contents</a>
+      <a href="rocq/ArchSemX86/ArchSemX86.html/index.html">index</a>
+    </div>
+  </li>
+</ul>
+
+<h2>OCaml API</h2>
+<p class="subtitle">
+  Generated with odoc. Only the <code>archsem</code> package ships OCaml code:
+  the extracted models and the litmus-test runner behind the
+  <code>archsem</code> command-line tool. The <code>coq-archsem*</code> package
+  pages exist but are empty.
+</p>
+<ul>
+  <li>
+    <div class="name"><code>archsem</code></div>
+    <div class="desc">
+      The extracted models (<code>Archsem</code>) plus the
+      <code>archsem.litmus</code> and <code>archsem.isla</code> libraries.
+    </div>
+    <div class="links">
+      <a href="ocaml/archsem/index.html">contents</a>
+    </div>
+  </li>
+</ul>
+
+<footer>
+  Generated from the <code>main</code> branch by
+  <a href="https://github.com/rems-project/archsem/actions">CI</a>.
+  Build it yourself with <code>make doc-site</code>, or browse it locally with
+  <code>make serve-doc-site</code>. </br>
+  The CSS of this landing page was generated by Claude
+</footer>
+
+</main>
+</body>
+
+</html>