doc: initialize a user-facing mdbook

Design:

- A flake similar to leanprover/lean4?subdir=docs/...
- Alectryon + Lean-mdBook
- CI + build

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

.github/workflows/build-userdocs.yml

@@ -0,0 +1,14 @@
+name: Build Aeneas user docs and test them
+on: [push, pull_request]
+
+jobs:
+  test:
+    name: Test Aeneas user docs
+    runs-on: [self-hosted, linux, nix]
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+    - name: Build the book
+      run: nix build '.?dir=docs/user'#book
+    # TODO: test the Lean examples code via nix build '.?dir=docs/user'#test or something similar.

.github/workflows/deploy-userdocs.yml

@@ -0,0 +1,32 @@
+name: Deploy Aeneas user docs to GitHub pages
+on:
+  push:
+    branches:
+      - main
+
+jobs:
+  deploy:
+    runs-on: [self-hosted, linux, nix]
+    permissions:
+      contents: write  # To push a branch
+      pull-requests: write  # To create a PR from that branch
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+    - name: Deploy GitHub Pages
+      run: |
+        # This assumes your book is in the root of your repository.
+        # Just add a `cd` here if you need to change to another directory.
+        nix build '.?dir=docs/user'#book -o html
+        git worktree add gh-pages
+        git config user.name "Deploy from CI"
+        git config user.email ""
+        cd gh-pages
+        # Delete the ref to avoid keeping history.
+        git update-ref -d refs/heads/gh-pages
+        rm -rf *
+        cp --dereference -vr ../html/* .
+        git add .
+        git commit -m "Deploy $GITHUB_SHA to gh-pages"
+        git push --force --set-upstream origin gh-pages

docs/user/.envrc

@@ -0,0 +1 @@
+use flake

docs/user/.gitignore

@@ -0,0 +1 @@
+book

docs/user/book.toml

@@ -0,0 +1,6 @@
+[book]
+authors = ["The Aeneas contributors"]
+language = "en"
+multilingual = false
+src = "src"
+title = "Aeneas user documentation"