feat(doc): Versioned documentation pages

This patch overhauls documentation generation to support separate
documentation pages for each Alt-ergo version on the GitHub pages
website.

We generate one version for the `next` and `main` branch, and one
version for each tag of the form `v*.*.*`. The version selector from
Sphinx is used to allow users to change the version (it appears in the
lower-right corner of the page).

We also keep a `latest` version that points to the latest tag that was
built (using a symbolic link). The default page redirects to the
`latest` version.

As part of this overhaul of the documentation workflow, the OCaml
documentation built by `odoc` is now also versioned and added to the
`API` sub-directory of the Sphinx documentation (with a placeholder to
prevent Sphinx from complaining).

Fixes OCamlPro#693

.github/workflows/documentation.yml

@@ -8,10 +8,17 @@ name: Documentation
 # - deploy_docs only run on the next branch when code is pushed. It retrieve
 # the ocaml and sphinx documentation and deploy them on the gh-pages branch
 
-on: [push, pull_request]
+on:
+  push:
+    tags:
+      - "v*.*.*"
+    branches:
+      - next
+      - main
+  pull_request:
 
 env:
-  OCAML_DEFAULT_VERSION: 4.10.0
+  OCAML_DEFAULT_VERSION: 4.14.1
   # Add OPAMYES=true to the environment, this is usefill to replace `-y` option
   # in any opam call
   OPAMYES: true
@@ -44,62 +51,58 @@ jobs:
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }}
-          dune-cache: true
+          # https://github.com/ocaml/dune/issues/7720
+          dune-cache: false
+
+      - name: Retrieve annotated tags for dune
+        run: git fetch --tags --force
+
 
       # Install dependencies if the cache is not retrieved
       # odoc is installed as deps with { with-doc } in opam files
       - name: opam install deps
         run: opam exec -- make deps
-      # if: steps.cache-opam.outputs.cache-hit != 'true'
 
-      # Try to upgrade installed packages and fix dependencies if needed,
-      # when the cache is retrieved
-      # - run: opam upgrade --fixup
-      #  if: steps.cache-opam.outputs.cache-hit == 'true'
+      - name: Perform version substitution
+        run: opam exec -- dune subst
 
       # Make the documentation
       - name: Make OCaml documentation
-        run: opam exec -- make odoc
+        run: opam exec -- dune build @doc
 
       # Create and upload an artifact `ocaml_doc` that contains the ocaml
       # documentation in html format.
-      # This is only done if this workflow is triggered in a PR or on the
-      # following branches : next, main
       - name: Upload ocaml documentation
         uses: actions/upload-artifact@v4
-        if: github.event_name == 'pull_request' || github.ref == 'refs/heads/next' || github.ref == 'refs/heads/main'
         with:
           name: ocaml_doc
           path: _build/default/_doc/_html/
 
-
-  # On PR, or push on next/main, build the sphinx general documentation
-  # If this build fails, the documentation workflow stops
-  # If it succeeds, an artifact is made with the generated documentation
-  # This artifact is used in the deploying job
   sphinx_docs:
     name: Sphinx documentation
-
-    # We only run this if the ocaml documentation build is successful
-    needs: ocaml_docs
-
-    # Sphinx documentation is only builded if a PR is open or when it's
-    # pushed on next or main
-    if: github.event_name == 'pull_request' || github.ref == 'refs/heads/next' || github.ref == 'refs/heads/main'
     runs-on: ubuntu-latest
 
+    outputs:
+      version-name: ${{ steps.version-name.outputs.target }}
+
     steps:
       # Checkout the code of the current branch
       - name: Checkout code
         uses: actions/checkout@v4
 
+      - name: Determine version name
+        id: version-name
+        run: |
+          echo "target=${GITHUB_REF#*/*/}" >> $GITHUB_OUTPUT
+
       # Build the sphinx documentation
       # and automatically print any error or warning
       - name: Build sphinx documentation
         uses: ammaraskar/sphinx-action@master
         with:
           docs-folder: "docs/sphinx_docs/"
-          build-command: "sphinx-build -b html . _build"
+          build-command: |
+            sphinx-build -b html -A current_version=${{ steps.version-name.outputs.target }} . _build
 
       # Create and upload an artifact `sphinx_doc` that contains the sphinx
       # documentation in html format.
@@ -109,45 +112,76 @@ jobs:
           name: sphinx_doc
           path: docs/sphinx_docs/_build
 
-
-  # For every push on main, retrieve ocaml and sphinx documentation
-  # and publish them on gh-pages branch
   deploy_docs:
     name: Deploy documentation
+    permissions:
+      contents: write
 
-    if: github.ref == 'refs/heads/main'
+    if: ${{ github.event_name == 'push' }}
 
     needs:
       - ocaml_docs
       - sphinx_docs
 
     runs-on: ubuntu-latest
     steps:
-      # Retrieve ocaml documentation artifact
-      - name: Download ocaml documentation
-        uses: actions/download-artifact@v4
-        with:
-          name: ocaml_doc
-          path: _build/odoc/dev
-
-      # Retrieve sphinx documentation artifact
       - name: Download sphinx documentation
         uses: actions/download-artifact@v4
         with:
           name: sphinx_doc
-          path: _build
+          path: _build/${{ needs.sphinx_docs.outputs.version-name }}
 
-      - name: Add files to bypass nojekyll
-        run: |
-          touch _build/.nojekyll
-          touch _build/odoc/.nojekyll
-          touch _build/odoc/dev/.nojekyll
+      - name: Download ocaml documentation
+        uses: actions/download-artifact@v4
+        with:
+          name: ocaml_doc
+          path: _build/${{ needs.sphinx_docs.outputs.version-name }}/API
 
-      # Deploy files contain in _build directory on gh-pages branch
       - name: deploy-doc
         uses: JamesIves/[email protected]
         with:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           BRANCH: gh-pages
           FOLDER: _build
           CLEAN: false
+
+  update_versions:
+    name: Update documentation versions
+    permissions:
+      contents: write
+
+    needs: deploy_docs
+    runs-on: ubuntu-latest
+
+    if: ${{ github.event_name == 'push' }}
+
+    steps:
+      - name: Checkout documentation
+        uses: actions/checkout@v4
+        with:
+          ref: gh-pages
+
+      - name: Update latest version
+        if: startsWith(github.ref, 'refs/tags/')
+        run: |
+          ln -nsf ${{ needs.sphinx_docs.outputs.version-name }} latest
+
+      - name: Write versions to JSON file
+        run: |
+          rm -f versions.json
+          echo -n '[' >versions.json
+          PREFIX=''
+          for version in $(ls -d */ | sort -n); do
+            echo -n "$PREFIX" >>versions.json
+            PREFIX=','
+            echo -n '{"url": "/alt-ergo/'$version'", "slug": "'${version%/}'"}' >>versions.json
+          done
+          echo -n ']' >>versions.json
+
+      - name: Push new versions
+        run: |
+          git config user.name github-actions
+          git config user.email [email protected]
+          git add versions.json
+          git commit -m 'Update versions.json' || exit 0
+          git push

alt-ergo-lib.opam.locked

@@ -30,9 +30,9 @@ depends: [
   "dolmen" {= "0.10"}
   "dolmen_loop" {= "0.10"}
   "dolmen_type" {= "0.10"}
-  "dune" {= "3.11.1"}
-  "dune-build-info" {= "3.11.1"}
-  "dune-configurator" {= "3.11.1"}
+  "dune" {= "3.16.0"}
+  "dune-build-info" {= "3.16.0"}
+  "dune-configurator" {= "3.16.0"}
   "fmt" {= "0.9.0"}
   "gen" {= "1.1"}
   "js_of_ocaml" {= "5.4.0"}

docs/sphinx_docs/API/index.md

@@ -1,7 +1,4 @@
-
 # API documentation
 
-Here, you can find the different version of the Alt-Ergo's API documentation :
-
-* [dev](https://ocamlpro.github.io/alt-ergo/odoc/dev/index.html)
-* [2.4.0](https://ocamlpro.github.io/alt-ergo/odoc/2.4.0/index.html)
+This is a placeholder to resolve references. It is replaced with the OCaml
+documentation when publishing the documentation.

docs/sphinx_docs/Usage/index.md

@@ -105,16 +105,17 @@ Look at the `worker_json_example.json` in the ressources `rsc` of the project to
 
 A small example of how to use the Alt-Ergo web worker can be build with the command ```make js-example```. This command also makes the web worker if it has not already been built. It produces a `www` directory with an html page where you can write a small example, run the worker, and see the results. You can also look at the console of your browser to look at the json file sent
 
+## Library
+
+Since version 2.2.0, Alt-Ergo's library is also compiled and installed. See the
+[API documentation] (also available [on ocaml.org](https://ocaml.org/p/alt-ergo-lib/latest/doc/index.html))
+for more information.
 
 [install section]: ../Install/index.md
 [Lwt]: https://ocsigen.org/lwt/
 [js_of_ocaml]: https://ocsigen.org/js_of_ocaml/
-[API documentation]: ../API/index.md
+[API documentation]: ../API/index
 [AB-Why3 README]: ../Plugins/ab_why3.md
 [Alt-ergo native language]: ../Alt_ergo_native/index
 [SMT-LIB language]: ../SMT-LIB_language/index
 [Dune-site plugins]: https://dune.readthedocs.io/en/stable/sites.html#plugins
-
-## Library
-
-Since version 2.2.0, Alt-Ergo's library is also compiled and installed. See the [API documentation] for more information.

docs/sphinx_docs/VERSION

@@ -0,0 +1 @@
+PROUT

docs/sphinx_docs/_static/css/versions.css

@@ -0,0 +1,3 @@
+.rst-versions .rst-other-versions .rtd-current-item {
+  font-weight: 700;
+}

docs/sphinx_docs/_static/js/versions.js

@@ -0,0 +1,33 @@
+function renderVersions(versions) {
+  return `
+  <dl>
+    <dt>Versions</dt>${ versions.active.map((version) => `
+    <dd ${ version.slug == versions.current.slug ? 'class="rtd-current-item"' : '' }>
+      <a href="${ version.url }">${ version.slug }</a>
+    </dd>
+    `).join("\n")}
+  </dl>
+  `;
+}
+
+document.addEventListener('DOMContentLoaded', function () {
+  $.getJSON('/alt-ergo/versions.json', (active) => {
+    const versions = {
+      "active": active,
+      "current": JSON.parse(document.getElementById('CURRENT_VERSION').innerHTML),
+    };
+
+    document.body.insertAdjacentHTML("beforeend", `
+    <div class="rst-versions" data-toggle="rst-versions" role="note" aria-label="Versions">
+      <span class="rst-current-version" data-toggle="rst-current-version">
+        <span class="fa fa-book"> Current version</span>
+        ${ versions.current.slug }
+        <span class="fa fa-caret-down"></span>
+      </span>
+      <div class="rst-other-versions">
+        ${renderVersions(versions)}
+      </div>
+    </div>
+    `);
+  });
+});

docs/sphinx_docs/_templates/versions.html

@@ -0,0 +1 @@
+<script type="application/json" id="CURRENT_VERSION">{"slug": "{{ current_version|default("dev", true) }}"}</script>

docs/sphinx_docs/conf.py

@@ -70,3 +70,8 @@
 # relative to this directory. They are copied after the builtin static files,
 # so a file named "default.css" will overwrite the builtin "default.css".
 html_static_path = ['_static']
+
+# -- Context population (version management and more) ------------------------
+
+html_css_files = ['css/versions.css']
+html_js_files = ['js/versions.js']

docs/sphinx_docs/index.md

@@ -9,14 +9,16 @@ It was developed at [LRI](https://www.lri.fr), and is now improved and maintaine
 You can [try Alt-Ergo](https://alt-ergo.ocamlpro.com/try.html) online.
 You can also learn more about our partners with the [Alt-Ergo Users' Club](https://alt-ergo.ocamlpro.com/#club).
 
+If you are using Alt-Ergo as a library, see the [API documentation](API/index) (also available [on ocaml.org](https://ocaml.org/p/alt-ergo-lib/latest/doc/index.html)).
+
 ## Input file formats
 
 Alt-ergo supports different input languages:
 
 - Alt-ergo supports the SMT-LIB language v2.6. **This is Alt-Ergo's preferred
   and recommended input format.** 
 - The original input language is its native language, based on the language of the Why3 platform.
-- It also (partially) supports the input language of Why3 through the :doc:`AB-Why3 plugin <../Plugins/ab_why3>`.
+- It also (partially) supports the input language of Why3 through the [AB-Why3 plugin](../Plugins/ab_why3).
 
 ```{toctree}
 :caption: Contents