Introduce GitHub Action.

.github/workflows/docker-action.yml

@@ -0,0 +1,77 @@
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-platform-docs.opam'
+          before_script: |
+            startGroup "Workaround permission issue"
+              sudo chown -R coq:coq .  # <--
+            endGroup
+            startGroup "Install APT dependencies"
+              cat /etc/os-release  # Print the Debian OS version
+              curl -fsSL https://deb.nodesource.com/setup_20.x | sudo bash -
+              sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends \
+                nodejs
+            endGroup
+          script: |
+            startGroup "Build"
+              cd src
+              make node_modules
+              make
+            endGroup
+          uninstall: ""
+      - uses: actions/upload-artifact@v4
+        with:
+          path: |
+            src/node_modules
+            src/*.html
+            src/*.css
+            src/*.js
+            src/*.v
+
+  # Deploy job
+  deploy:
+    if: github.event_name == 'push' && github.ref == 'refs/heads/main'
+
+    # Add a dependency to the build job
+    needs: build
+
+    # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
+    permissions:
+      pages: write      # to deploy to Pages
+      id-token: write   # to verify the deployment originates from an appropriate source
+
+    # Deploy to the github-pages environment
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+
+    # Specify runner + deployment step
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/download-artifact@v4
+      - uses: actions/configure-pages@v5
+      - uses: actions/upload-pages-artifact@v3
+        with:
+          path: artifact/
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

coq-platform-docs.opam

@@ -0,0 +1,36 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "Théo Zimmermann <[email protected]>"
+version: "dev"
+
+homepage: "https://github.com/Zimmi48/platform-docs"
+dev-repo: "git+https://github.com/Zimmi48/platform-docs.git"
+bug-reports: "https://github.com/Zimmi48/platform-docs/issues"
+
+
+synopsis: "A project of short tutorials and how-to guides for Coq features and Coq Platform packages."
+description: """
+This project aims to create an online compilation of short and interactive tutorials and how-to guides for Coq and the Coq Platform.
+
+Each core functionality and plugin of Coq and the Coq Platform should have (short) pedagogical tutorials and/or how-to guides demonstrating how to use the functionality, with practical examples. They should further be available online through an interactive interface, most likely using JSCoq.
+
+Tutorials and how-to guides serve different purposes and are complementary. Tutorials guide a user during learning in discovering specific aspects of a feature like "Notations in Coq", by going through (simple) predetermined examples, and introducing notions gradually. In contrast, how-to guides are use-case-oriented and guides users through real life problems and their inherent complexity, like "How to define functions by well-founded recursion and reason about them".
+"""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" 
+  "coq-equations" 
+]
+
+tags: [
+  "logpath:"
+]
+authors: [
+  "Thomas Lamiaux"
+  "Pierre Rousselin"
+  "Théo Zimmermann"
+]

meta.yml

@@ -0,0 +1,22 @@
+fullname: "Coq Platform Docs"
+shortname: platform-docs
+organization: Zimmi48 # To change later to "coq"
+synopsis: "A project of short tutorials and how-to guides for Coq features and Coq Platform packages."
+description: |
+  This project aims to create an online compilation of short and interactive tutorials and how-to guides for Coq and the Coq Platform.
+
+  Each core functionality and plugin of Coq and the Coq Platform should have (short) pedagogical tutorials and/or how-to guides demonstrating how to use the functionality, with practical examples. They should further be available online through an interactive interface, most likely using JSCoq.
+
+  Tutorials and how-to guides serve different purposes and are complementary. Tutorials guide a user during learning in discovering specific aspects of a feature like "Notations in Coq", by going through (simple) predetermined examples, and introducing notions gradually. In contrast, how-to guides are use-case-oriented and guides users through real life problems and their inherent complexity, like "How to define functions by well-founded recursion and reason about them".
+authors:
+- name: "Thomas Lamiaux"
+- name: "Pierre Rousselin"
+- name: "Théo Zimmermann"
+# TODO: add license
+dependencies:
+- description: Equations
+  opam:
+    name: coq-equations
+opam-file-maintainer: "Théo Zimmermann <[email protected]>"
+tested_coq_opam_versions:
+- version: "8.19"

src/index.html

@@ -0,0 +1,23 @@
+<!DOCTYPE html>
+<html>
+<head>
+    <title>Coq Platform Docs - Demo</title>
+</head>
+<body>
+    <h1>Coq Platform Docs - Demo</h1>
+    <p>
+        This is a demo page for the Coq Platform Docs.
+    </p>
+    <p>
+        List of available tutorials:
+    </p>
+    <ul>
+        <li><a href="RequireImportTutorial.html">Require/Import Tutorial (interactive version)</a></li>
+        <li><a href="RequireImportTutorial.v">Require/Import Tutorial (source code)</a></li>
+        <li><a href="SearchTutorial.html">Search Tutorial (interactive version)</a></li>
+        <li><a href="SearchTutorial.v">Search Tutorial (source code)</a></li>
+        <li><a href="Tutorial_Equations_basics.html">Equations Tutorial : basics (interactive version)</a></li>
+        <li><a href="Tutorial_Equations_basics.v">Equations Tutorial : basics (source code)</a></li>
+    </ul>
+</body>
+</html>