Create a new build script, based on the UniMath one

.github/workflows/build-schools.yml

@@ -1,68 +1,84 @@
-# This is a basic workflow to help you get started with Actions
-
 name: CI
 
 # Controls when the action will run.
 on:
-  # Triggers the workflow on push or pull request events but only for the master branch
+  # Run the workflow on push or pull request events but only for the master branch
   push:
     branches: [ master ]
   pull_request:
     branches: [ master ]
 
+  # Run at 05:37 UTC every Thursday to keep the cache from being evicted.
   schedule:
-    # Run this workflow at 02:15 UTC every Tuesday to keep the cache from being
-    # evicted. A typical run with everything cached should take less than 10
-    # minutes.
-    - cron: 15 2 * * TUE
+    - cron: 37 5 * * THU
 
-  # Allows you to run this workflow manually from the Actions tab
+  # Run when activated manually from the Actions tab
   workflow_dispatch:
 
-env:
-  # Set this to the version of Coq that should be used.
-  coq-version: 8.19.0
-  dune-version: 3.8.0
-  DUNE_CACHE_STORAGE_MODE: copy
-
-# A workflow run is made up of one or more jobs that can run sequentially or in parallel
 jobs:
-  # This workflow contains a single job called "build"
   build:
-    name: Build Schools
-    # The type of runner that the job will run on
-    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ ubuntu-latest ]
+        coq-version: [ latest ]
+        ocaml-version: [ default ]
 
-    # Steps represent a sequence of tasks that will be executed as part of the job
+    name: Build Schools on Linux (Coq ${{ matrix.coq-version }})
+    runs-on: ${{ matrix.os }}
     steps:
-      # Checkout UniMath into the working directory
       - name: Checkout UniMath.
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: UniMath/UniMath
           clean: false
           path: .
 
-      # Checkout the current branch into Schools/
       - name: Checkout Schools.
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: Schools
 
-      # Ideally we would use docker-coq. A setup currently takes about 7min
-      # before it starts compiling, with OCaml cached.
-      - name: Install OCaml.
-        uses: ocaml/setup-ocaml@v2
+      # The path variable here matches the DUNE_CACHE_ROOT variable in the "Build Schools" step
+      - name: Load cache
+        uses: actions/cache/restore@v4
+        id: cache
+        with:
+          path: dune-cache
+          key: UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}
+          restore-keys: |
+            UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}
+            UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-
+
+      - name: Build Schools
+        uses: coq-community/docker-coq-action@v1
         with:
-          ocaml-compiler: ocaml-variants.4.14.0+options,ocaml-option-flambda
-          dune-cache: true
-          opam-disable-sandboxing: true
+          coq_version: ${{ matrix.coq-version }}
+          ocaml_version: ${{ matrix.ocaml-version }}
+          custom_script: |
+            startGroup "Workaround permission issue"
+              sudo chown -R coq:coq .
+            endGroup
 
-      - name: Install Dune
-        run: opam pin add dune ${{ env.dune-version }}
-      - name: Install Coq
-        run: opam pin add coq ${{ env.coq-version }}
+            startGroup "Print versions"
+              opam --version
+              opam exec -- dune --version
+              opam exec -- coqc --version
+            endGroup
 
-      # Schools is built using the flags specified in code/dune.
-      - name: Compile Schools.
-        run: opam exec -- dune build Schools --display=short --error-reporting=twice
+            startGroup "Build UniMath"
+              export DUNE_CACHE_ROOT=$(pwd)/dune-cache/
+              opam exec -- dune build Schools -j 2 --display=short --cache=enabled --error-reporting=twice
+            endGroup
+
+      # In a separate step, to make sure it runs, even if the previous step fails
+      - name: Revert permissions
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+
+      - name: Save cache
+        uses: actions/cache/save@v4
+        if: ${{ always() }}
+        with:
+          path: dune-cache
+          key: UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}