From 9515c12d1605c84a775e015c0e18e027d5bed85e Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 28 Aug 2023 15:17:27 +0200
Subject: [PATCH 01/20] [ ci ] Move external libs outside of Idris2 job

Seems like this is an independent check, which should be processed as
such.
(Hopefully I got the CI incantations right...)
---
 .github/workflows/ci-extern-libs.yaml | 269 ++++++++++++++++++++++++++
 .github/workflows/ci-idris2.yml       | 179 -----------------
 2 files changed, 269 insertions(+), 179 deletions(-)
 create mode 100644 .github/workflows/ci-extern-libs.yaml

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
new file mode 100644
index 0000000000..46ddd54056
--- /dev/null
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -0,0 +1,269 @@
+name: Build External Libraries
+
+######################################################################
+# Ubuntu testing some libraries.
+# We are particularly interested in libraries that are heavily using
+# dependent types, that are prone to find bugs and regressions in the
+# compiler.
+######################################################################
+
+on:
+  # Copied from the ci-idris2.yml file
+  push:
+    branches:
+      - '*'
+    tags:
+      - '*'
+    paths-ignore:
+      - 'docs/**'
+      - 'icons/**'
+      - 'Release/**'
+      - '**.md'
+      - 'CONTRIBUTORS'
+      - 'LICENSE'
+      - 'CHANGELOG.md'
+      - '.github/workflows/ci-bootstrap.yml'
+      - '.github/workflows/ci-lint.yml'
+      - '.github/workflows/ci-sphinx.yml'
+      - '.github/workflows/ci-super-linter.yml'
+  pull_request:
+    branches:
+      - main
+    paths-ignore:
+      - 'docs/**'
+      - 'icons/**'
+      - 'Release/**'
+      - '**.md'
+      - 'CONTRIBUTORS'
+      - 'LICENSE'
+      - '.github/workflows/ci-bootstrap.yml'
+      - '.github/workflows/ci-lint.yml'
+      - '.github/workflows/ci-sphinx.yml'
+      - '.github/workflows/ci-super-linter.yml'
+
+concurrency:
+  group: ${{ github.ref }}
+  cancel-in-progress: true
+
+env:
+  IDRIS2_MINIMUM_COMPAT_VERSION: 0.6.0
+
+jobs:
+
+  initialise:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Project
+        uses: actions/checkout@v3
+        with:
+          # for pull_request so we can do HEAD^2
+          fetch-depth: 2
+
+      - name: Get commit message
+        id: get_commit_message
+        run: |
+          if   [[ '${{ github.event_name }}' == 'push' ]]; then
+            echo "commit_message=$(git log --format=%B -n 1 HEAD | tr '\n' ' ')" >> "$GITHUB_OUTPUT"
+          elif [[ '${{ github.event_name }}' == 'pull_request' ]]; then
+            echo "commit_message=$(git log --format=%B -n 1 HEAD^2 | tr '\n' ' ')" >> "$GITHUB_OUTPUT"
+          fi
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: ubuntu-installed-idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Build self-hosted from previous version
+        run: make all IDRIS2_BOOT="idris2 -Werror" && make install
+
+
+  ########################################################################
+  # Test that we can build Collie
+  ########################################################################
+
+  ubuntu-test-collie:
+    needs: [initialise]
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'ohad/collie'
+      - name: Build Collie
+        run: |
+          make
+
+  ########################################################################
+  # Test that we can build Frex
+  ########################################################################
+
+  ubuntu-test-frex:
+    needs: [initialise]
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'frex-project/idris-frex'
+      - name: Build Frex
+        run: |
+          make
+          make test
+
+  ######################################################################
+  # Test that we can build Stefan Höck's elab-util
+  ######################################################################
+
+  ubuntu-test-elab:
+    needs: [initialise]
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'stefan-hoeck/idris2-elab-util'
+      - name: Build idris2-elab-util
+        run: |
+          make all
+
+  ######################################################################
+  # Ubuntu using katla to build html doc of the libs
+  ######################################################################
+
+  ubuntu-katla:
+    needs: [initialise, ubuntu-test-collie]
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: html]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+
+      - name: Initialise DEPLOY variable
+        run: |
+          if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then
+             echo "IDRIS2_DEPLOY=true" >> "$GITHUB_ENV"
+          fi
+
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme markdown
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout idris2
+        uses: actions/checkout@v3
+      - name: Build API
+        run: make install-api
+        shell: bash
+      - name: Checkout collie
+        uses: actions/checkout@v3
+        with:
+          repository: 'ohad/collie'
+      - name: Build and install Collie
+        run: |
+          make install
+      - name: Checkout idrall
+        uses: actions/checkout@v3
+        with:
+          repository: 'alexhumphreys/idrall'
+      - name: Build and install idrall
+        run: |
+          make install
+      - name: Checkout katla
+        uses: actions/checkout@v3
+        with:
+          repository: 'idris-community/katla'
+      - name: Build and install katla
+        run: |
+          make
+          mkdir -p "${HOME}"/.local/bin/
+          cp -r build/exec/* "${HOME}"/.local/bin/
+          echo "${HOME}/.local/bin" >> "$GITHUB_PATH"
+      - name: Checkout idris2
+        uses: actions/checkout@v3
+      - name: Build html doc & landing page
+        run: |
+          make -C libs/prelude/ install docs IDRIS2=idris2
+          make -C libs/base/ install docs IDRIS2=idris2
+          make -C libs/contrib/ install docs IDRIS2=idris2
+          make -C libs/network/ install docs IDRIS2=idris2
+          make -C libs/linear/ install docs IDRIS2=idris2
+          make -C libs/test/ install docs IDRIS2=idris2
+          make -C libs/papers/ install docs IDRIS2=idris2
+
+          cd .github/scripts
+          ./katla.sh
+          cd -
+          cd www/
+          ./katla.sh
+          cd -
+          cp -r www/html/* .github/scripts/html/
+      - name: Deploy HTML
+        uses: JamesIves/github-pages-deploy-action@4.1.3
+        if: ${{ success() && env.IDRIS2_DEPLOY }}
+
+        with:
+          branch: gh-pages
+          folder: .github/scripts/html/
+          git-config-name: Github Actions
+
diff --git a/.github/workflows/ci-idris2.yml b/.github/workflows/ci-idris2.yml
index 08fccaeaae..736491fd69 100644
--- a/.github/workflows/ci-idris2.yml
+++ b/.github/workflows/ci-idris2.yml
@@ -486,182 +486,3 @@ jobs:
         run: cd tests/idris2/api001 && ./run idris2
         shell: bash
 
-  ######################################################################
-  # Ubuntu testing some libraries.
-  # We are particularly interested in libraries that are heavily using
-  # dependent types, that are prone to find bugs and regressions in the
-  # compiler.
-  ######################################################################
-
-  ubuntu-test-collie:
-    needs: [initialise, ubuntu-self-host-previous-version]
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'ohad/collie'
-      - name: Build Collie
-        run: |
-          make
-
-  ubuntu-test-frex:
-    needs: [initialise, ubuntu-self-host-previous-version]
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'frex-project/idris-frex'
-      - name: Build Frex
-        run: |
-          make
-          make test
-
-  ubuntu-test-elab:
-    needs: [initialise, ubuntu-self-host-previous-version]
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'stefan-hoeck/idris2-elab-util'
-      - name: Build idris2-elab-util
-        run: |
-          make all
-
-  ######################################################################
-  # Ubuntu using katla to build html doc of the libs
-  ######################################################################
-
-  ubuntu-katla:
-    needs: [initialise, ubuntu-test-collie]
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: html]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-
-      - name: Initialise DEPLOY variable
-        run: |
-          if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then
-             echo "IDRIS2_DEPLOY=true" >> "$GITHUB_ENV"
-          fi
-
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme markdown
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout idris2
-        uses: actions/checkout@v3
-      - name: Build API
-        run: make install-api
-        shell: bash
-      - name: Checkout collie
-        uses: actions/checkout@v3
-        with:
-          repository: 'ohad/collie'
-      - name: Build and install Collie
-        run: |
-          make install
-      - name: Checkout idrall
-        uses: actions/checkout@v3
-        with:
-          repository: 'alexhumphreys/idrall'
-      - name: Build and install idrall
-        run: |
-          make install
-      - name: Checkout katla
-        uses: actions/checkout@v3
-        with:
-          repository: 'idris-community/katla'
-      - name: Build and install katla
-        run: |
-          make
-          mkdir -p "${HOME}"/.local/bin/
-          cp -r build/exec/* "${HOME}"/.local/bin/
-          echo "${HOME}/.local/bin" >> "$GITHUB_PATH"
-      - name: Checkout idris2
-        uses: actions/checkout@v3
-      - name: Build html doc & landing page
-        run: |
-          make -C libs/prelude/ install docs IDRIS2=idris2
-          make -C libs/base/ install docs IDRIS2=idris2
-          make -C libs/contrib/ install docs IDRIS2=idris2
-          make -C libs/network/ install docs IDRIS2=idris2
-          make -C libs/linear/ install docs IDRIS2=idris2
-          make -C libs/test/ install docs IDRIS2=idris2
-          make -C libs/papers/ install docs IDRIS2=idris2
-
-          cd .github/scripts
-          ./katla.sh
-          cd -
-          cd www/
-          ./katla.sh
-          cd -
-          cp -r www/html/* .github/scripts/html/
-      - name: Deploy HTML
-        uses: JamesIves/github-pages-deploy-action@4.1.3
-        if: ${{ success() && env.IDRIS2_DEPLOY }}
-
-        with:
-          branch: gh-pages
-          folder: .github/scripts/html/
-          git-config-name: Github Actions

From f9873b77d49bbea0a2681e637091b4bdc5f56b79 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 28 Aug 2023 15:29:12 +0200
Subject: [PATCH 02/20] [ ci ] Run extern-libs after Idris2

Hopefully this solves the artifact issue?
---
 .github/workflows/ci-extern-libs.yaml | 38 ++++-----------------------
 1 file changed, 5 insertions(+), 33 deletions(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 46ddd54056..f5aeb90f14 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -8,38 +8,11 @@ name: Build External Libraries
 ######################################################################
 
 on:
-  # Copied from the ci-idris2.yml file
-  push:
-    branches:
-      - '*'
-    tags:
-      - '*'
-    paths-ignore:
-      - 'docs/**'
-      - 'icons/**'
-      - 'Release/**'
-      - '**.md'
-      - 'CONTRIBUTORS'
-      - 'LICENSE'
-      - 'CHANGELOG.md'
-      - '.github/workflows/ci-bootstrap.yml'
-      - '.github/workflows/ci-lint.yml'
-      - '.github/workflows/ci-sphinx.yml'
-      - '.github/workflows/ci-super-linter.yml'
-  pull_request:
-    branches:
-      - main
-    paths-ignore:
-      - 'docs/**'
-      - 'icons/**'
-      - 'Release/**'
-      - '**.md'
-      - 'CONTRIBUTORS'
-      - 'LICENSE'
-      - '.github/workflows/ci-bootstrap.yml'
-      - '.github/workflows/ci-lint.yml'
-      - '.github/workflows/ci-sphinx.yml'
-      - '.github/workflows/ci-super-linter.yml'
+  # Only run this workflow when the Idris2 workflow has completed
+  workflow_run:
+    workflows: ["Idris2"]
+    types:
+      - completed
 
 concurrency:
   group: ${{ github.ref }}
@@ -266,4 +239,3 @@ jobs:
           branch: gh-pages
           folder: .github/scripts/html/
           git-config-name: Github Actions
-

From cde9fe5ec6020cb92dc628fbf3e127b175bb7533 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 28 Aug 2023 16:16:54 +0200
Subject: [PATCH 03/20] [ ci ] Copy setup-jobs from ci-idris2 to extern-libs

DRY. But sometimes, it really is the easiest way to get things done (and
it should be fine(TM)...)
---
 .github/workflows/ci-extern-libs.yaml | 83 +++++++++++++++++++++++++--
 1 file changed, 79 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index f5aeb90f14..07392e4da7 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -23,6 +23,8 @@ env:
 
 jobs:
 
+  # First 3 jobs blatantly stolen from ci-idris2
+
   initialise:
     runs-on: ubuntu-latest
     steps:
@@ -40,6 +42,72 @@ jobs:
           elif [[ '${{ github.event_name }}' == 'pull_request' ]]; then
             echo "commit_message=$(git log --format=%B -n 1 HEAD^2 | tr '\n' ' ')" >> "$GITHUB_OUTPUT"
           fi
+
+    outputs:
+      commit_message:
+        echo "${{ steps.get_commit_message.outputs.commit_message }}"
+
+  quick-check:
+    needs: initialise
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci: skip]')
+    env:
+      IDRIS2_CG: chez
+      SCHEME: scheme
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+
+      # Get our hands on the released version either by using the cache
+      # or by rebuilding it if necessary.
+      - name: Cache Chez Previous Version
+        id: previous-version-cache
+        uses: actions/cache@v3
+        with:
+          path: Idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}
+          key: ${{ runner.os }}-idris2-bootstrapped-chez-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}
+      - name : Build previous version
+        if: steps.previous-version-cache.outputs.cache-hit != 'true'
+        run: |
+          wget "https://www.idris-lang.org/idris2-src/idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz"
+          tar zxvf "idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz"
+          cd "Idris2-$IDRIS2_MINIMUM_COMPAT_VERSION"
+          make bootstrap
+          cd ..
+      - name: Install previous version
+        run: |
+          cd "Idris2-$IDRIS2_MINIMUM_COMPAT_VERSION"
+          make install
+          cd ..
+
+      # Build the current version and save the installation.
+      - name: Build current version
+        run: |
+          make && make install
+      - name: Artifact Idris2 from previous version
+        uses: actions/upload-artifact@v3
+        with:
+          name: ubuntu-installed-idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}-chez
+          path: ~/.idris2/
+
+  ubuntu-self-host-previous-version:
+    needs: [initialise, quick-check]
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: ubuntu]')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
       - name: Download Idris2 Artifact
         uses: actions/download-artifact@v3
         with:
@@ -53,6 +121,13 @@ jobs:
           chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
       - name: Build self-hosted from previous version
         run: make all IDRIS2_BOOT="idris2 -Werror" && make install
+      - name: Test self-hosted from previous version
+        run: make ci-ubuntu-test INTERACTIVE=''
+      - name: Artifact Idris2
+        uses: actions/upload-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
 
 
   ########################################################################
@@ -60,7 +135,7 @@ jobs:
   ########################################################################
 
   ubuntu-test-collie:
-    needs: [initialise]
+    needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')
@@ -92,7 +167,7 @@ jobs:
   ########################################################################
 
   ubuntu-test-frex:
-    needs: [initialise]
+    needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')
@@ -125,7 +200,7 @@ jobs:
   ######################################################################
 
   ubuntu-test-elab:
-    needs: [initialise]
+    needs: [initialise, quick-check]
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')
@@ -157,7 +232,7 @@ jobs:
   ######################################################################
 
   ubuntu-katla:
-    needs: [initialise, ubuntu-test-collie]
+    needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')

From 8ec3d401287f87c11d0672a94d73b744af7c5ba5 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 28 Aug 2023 16:19:16 +0200
Subject: [PATCH 04/20] [ ci ] rm the ci-idris2 dependency from extern-libs

Now that the setup-jobs have been copied over, this dependency should be
unnecessary.
---
 .github/workflows/ci-extern-libs.yaml | 36 +++++++++++++++++++++++----
 1 file changed, 31 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 07392e4da7..a1dc542fd7 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -8,11 +8,37 @@ name: Build External Libraries
 ######################################################################
 
 on:
-  # Only run this workflow when the Idris2 workflow has completed
-  workflow_run:
-    workflows: ["Idris2"]
-    types:
-      - completed
+  push:
+    branches:
+      - '*'
+    tags:
+      - '*'
+    paths-ignore:
+      - 'docs/**'
+      - 'icons/**'
+      - 'Release/**'
+      - '**.md'
+      - 'CONTRIBUTORS'
+      - 'LICENSE'
+      - 'CHANGELOG.md'
+      - '.github/workflows/ci-bootstrap.yml'
+      - '.github/workflows/ci-lint.yml'
+      - '.github/workflows/ci-sphinx.yml'
+      - '.github/workflows/ci-super-linter.yml'
+  pull_request:
+    branches:
+      - main
+    paths-ignore:
+      - 'docs/**'
+      - 'icons/**'
+      - 'Release/**'
+      - '**.md'
+      - 'CONTRIBUTORS'
+      - 'LICENSE'
+      - '.github/workflows/ci-bootstrap.yml'
+      - '.github/workflows/ci-lint.yml'
+      - '.github/workflows/ci-sphinx.yml'
+      - '.github/workflows/ci-super-linter.yml'
 
 concurrency:
   group: ${{ github.ref }}

From 63ab414abfdb1840470698e6e063cfe557cdae71 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 28 Aug 2023 16:22:35 +0200
Subject: [PATCH 05/20] [ ci ] All extern libs depend on self-host

---
 .github/workflows/ci-extern-libs.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index a1dc542fd7..6919df57a7 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -226,7 +226,7 @@ jobs:
   ######################################################################
 
   ubuntu-test-elab:
-    needs: [initialise, quick-check]
+    needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')

From 6f54787b1a040a2df0ba063bea6d2d3a1fb5b4c0 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Tue, 29 Aug 2023 15:49:43 +0200
Subject: [PATCH 06/20] [ ci ] Add extern libs concurrency group

Should hopefully avoid interference with the Idris2 CI.
---
 .github/workflows/ci-extern-libs.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 6919df57a7..13d2d2adcb 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -41,7 +41,7 @@ on:
       - '.github/workflows/ci-super-linter.yml'
 
 concurrency:
-  group: ${{ github.ref }}
+  group: extlibs-${{ github.ref }}
   cancel-in-progress: true
 
 env:

From 4c27d3cd08ab9cf7966d119422756230c804bf58 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Tue, 29 Aug 2023 16:34:01 +0200
Subject: [PATCH 07/20] [ ci ] Build pack and the LSP as part of ext-libs

These are relied upon by many developers, so it seems only sensible to
test that nothing in the current PR breaks these. If nothing else as a
foreshadowing for the maintainers of them.
---
 .github/workflows/ci-extern-libs.yaml | 77 ++++++++++++++++++++++++++-
 1 file changed, 75 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 13d2d2adcb..8c03cd0e77 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -222,9 +222,11 @@ jobs:
           make test
 
   ######################################################################
-  # Test that we can build Stefan Höck's elab-util
+  # Test that we can build Stefan Höck's elab-util and pack
   ######################################################################
 
+  # ELAB
+
   ubuntu-test-elab:
     needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
@@ -253,8 +255,79 @@ jobs:
         run: |
           make all
 
+  # PACK
+
+  ubuntu-test-pack:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+      PACK_DIR: /root/.pack
+    strategy:
+      fail-fast: false
+    # instead of bootstrapping pack, load the dockerimage where it is already
+    # we'll then use pack to build pack with this job's idris2 sources
+    container: ghcr.io/stefan-hoeck/idris2-pack:latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'stefan-hoeck/idris2-pack'
+      # by default, pack uses the main idris2 head, not the current job's one
+      - name: Toml setup
+        run: |
+          echo "[idris2]" > pack.toml
+          echo "url = \"https://github.com/idris-lang/Idris2\"" >> pack.toml
+          echo "commit = \"$GITHUB_REF\"" >> pack.toml
+          echo "bootstrap  = true" >> pack.toml
+      - name: Build idris2-pack
+        run: |
+          pack install pack
+
+  ######################################################################
+  # Test that we can build the LSP
+  ######################################################################
+
+  ubuntu-test-lsp:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install chezscheme
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'idris-community/idris2-lsp'
+      - name: Install libs and API
+        run: |
+          git submodule update --init Idris2
+          cd Idris2
+          make all
+          make install-with-src-libs
+          make install-with-src-api
+      - name: Build idris2-lsp
+        run: |
+          make all
+
   ######################################################################
-  # Ubuntu using katla to build html doc of the libs
+  # Test that we can use Katla to build html doc of the libs
   ######################################################################
 
   ubuntu-katla:

From 814ecb42f4fea5bb89052c4e98f5578df16dc7cd Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Wed, 30 Aug 2023 10:31:03 +0200
Subject: [PATCH 08/20] [ ci ] Fix pack URL? RM lsp test for now

We need pack to check out the PR's ref somehow. Using
`GITHUB_REPOSITORY` as the URL might work?
---
 .github/workflows/ci-extern-libs.yaml | 79 ++++++++++++++-------------
 1 file changed, 40 insertions(+), 39 deletions(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 8c03cd0e77..02cf7ac6fd 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -280,51 +280,52 @@ jobs:
       - name: Toml setup
         run: |
           echo "[idris2]" > pack.toml
-          echo "url = \"https://github.com/idris-lang/Idris2\"" >> pack.toml
+          echo "url = \"https://github.com/$GITHUB_REPOSITORY\"" >> pack.toml
           echo "commit = \"$GITHUB_REF\"" >> pack.toml
           echo "bootstrap  = true" >> pack.toml
       - name: Build idris2-pack
         run: |
           pack install pack
 
-  ######################################################################
-  # Test that we can build the LSP
-  ######################################################################
-
-  ubuntu-test-lsp:
-    needs: ubuntu-self-host-previous-version
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install chezscheme
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'idris-community/idris2-lsp'
-      - name: Install libs and API
-        run: |
-          git submodule update --init Idris2
-          cd Idris2
-          make all
-          make install-with-src-libs
-          make install-with-src-api
-      - name: Build idris2-lsp
-        run: |
-          make all
+# FIXME: use pack instead, once it's working; otherwise the Idris version is wrong
+#  ######################################################################
+#  # Test that we can build the LSP
+#  ######################################################################
+#
+#  ubuntu-test-lsp:
+#    needs: ubuntu-self-host-previous-version
+#    runs-on: ubuntu-latest
+#    if: |
+#      !contains(needs.initialise.outputs.commit_message, '[ci:')
+#      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+#    env:
+#      IDRIS2_CG: chez
+#    steps:
+#      - name: Download Idris2 Artifact
+#        uses: actions/download-artifact@v3
+#        with:
+#          name: idris2-nightly-chez
+#          path: ~/.idris2/
+#      - name: Install chezscheme
+#        run: |
+#          sudo apt-get update
+#          sudo apt-get install -y chezscheme
+#          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+#          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+#      - name: Checkout
+#        uses: actions/checkout@v3
+#        with:
+#          repository: 'idris-community/idris2-lsp'
+#      - name: Install libs and API
+#        run: |
+#          git submodule update --init Idris2
+#          cd Idris2
+#          make all
+#          make install-with-src-libs
+#          make install-with-src-api
+#      - name: Build idris2-lsp
+#        run: |
+#          make all
 
   ######################################################################
   # Test that we can use Katla to build html doc of the libs

From cd6226cbabf20d1a6c9580d6ef6300cdf4f6396f Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Wed, 30 Aug 2023 13:44:01 +0200
Subject: [PATCH 09/20] [ ci ] Add GH_REF_NAME to pack idris2.commit

This might be the way? (I really don't want to have to fork pack...)
---
 .github/workflows/ci-extern-libs.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 02cf7ac6fd..300ca885f6 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -281,7 +281,7 @@ jobs:
         run: |
           echo "[idris2]" > pack.toml
           echo "url = \"https://github.com/$GITHUB_REPOSITORY\"" >> pack.toml
-          echo "commit = \"$GITHUB_REF\"" >> pack.toml
+          echo "commit = \"${GITHUB_REF}:${GITHUB_REF_NAME}\"" >> pack.toml
           echo "bootstrap  = true" >> pack.toml
       - name: Build idris2-pack
         run: |

From 6909becb88313e1b555463b71b9a3acffbde1e66 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Wed, 30 Aug 2023 14:31:11 +0200
Subject: [PATCH 10/20] [ ci ] Fetch the PR before attempting pack install

That might help...
---
 .github/workflows/ci-extern-libs.yaml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 300ca885f6..2cbb8a2b77 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -281,10 +281,11 @@ jobs:
         run: |
           echo "[idris2]" > pack.toml
           echo "url = \"https://github.com/$GITHUB_REPOSITORY\"" >> pack.toml
-          echo "commit = \"${GITHUB_REF}:${GITHUB_REF_NAME}\"" >> pack.toml
+          echo "commit = \"${GITHUB_REF_NAME}\"" >> pack.toml
           echo "bootstrap  = true" >> pack.toml
       - name: Build idris2-pack
         run: |
+          git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
           pack install pack
 
 # FIXME: use pack instead, once it's working; otherwise the Idris version is wrong

From af4bd1b1d4e6161a4b714850f19a12b740274353 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Wed, 30 Aug 2023 15:20:00 +0200
Subject: [PATCH 11/20] [ ci ] Mark CWD as safe for git-fetch reasons

It's probably fiiine...
---
 .github/workflows/ci-extern-libs.yaml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 2cbb8a2b77..2eec97f2c9 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -285,6 +285,7 @@ jobs:
           echo "bootstrap  = true" >> pack.toml
       - name: Build idris2-pack
         run: |
+          git config --global --add safe.directory "${PWD}"
           git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
           pack install pack
 

From ddf9d1fdd29dc81148b32a61f3c336549934cf65 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Wed, 30 Aug 2023 16:29:43 +0200
Subject: [PATCH 12/20] [ ci ] Restore the REF to the commit pack param

I feel like this is so close to working, and yet so far...
---
 .github/workflows/ci-extern-libs.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 2eec97f2c9..6bb5f8c88d 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -281,7 +281,7 @@ jobs:
         run: |
           echo "[idris2]" > pack.toml
           echo "url = \"https://github.com/$GITHUB_REPOSITORY\"" >> pack.toml
-          echo "commit = \"${GITHUB_REF_NAME}\"" >> pack.toml
+          echo "commit = \"${GITHUB_REF}:${GITHUB_REF_NAME}\"" >> pack.toml
           echo "bootstrap  = true" >> pack.toml
       - name: Build idris2-pack
         run: |

From d39a52b9d5eb92f285c58ef72625f5dfa64c2820 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Thu, 31 Aug 2023 12:20:06 +0200
Subject: [PATCH 13/20] [ ci ] Use 'latest' syntax to fix things

Finally installed pack locally and tested it as well. So quite a bit
more confident that this works (although you never know, CI could just
throw us for a spin for the fun of it)...
---
 .github/workflows/ci-extern-libs.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yaml
index 6bb5f8c88d..9d4e5baa91 100644
--- a/.github/workflows/ci-extern-libs.yaml
+++ b/.github/workflows/ci-extern-libs.yaml
@@ -280,8 +280,8 @@ jobs:
       - name: Toml setup
         run: |
           echo "[idris2]" > pack.toml
-          echo "url = \"https://github.com/$GITHUB_REPOSITORY\"" >> pack.toml
-          echo "commit = \"${GITHUB_REF}:${GITHUB_REF_NAME}\"" >> pack.toml
+          echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
+          echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
           echo "bootstrap  = true" >> pack.toml
       - name: Build idris2-pack
         run: |

From 01f83c48dc01c785d2b474492455f4d4bdbe2c53 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Fri, 1 Sep 2023 10:05:47 +0200
Subject: [PATCH 14/20] [ ci ] Make linter happy

Gods forbid we use a `.yaml` file instead of `.yml` -_-
---
 .github/workflows/{ci-extern-libs.yaml => ci-extern-libs.yml} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename .github/workflows/{ci-extern-libs.yaml => ci-extern-libs.yml} (100%)

diff --git a/.github/workflows/ci-extern-libs.yaml b/.github/workflows/ci-extern-libs.yml
similarity index 100%
rename from .github/workflows/ci-extern-libs.yaml
rename to .github/workflows/ci-extern-libs.yml

From f9f3eab39e6837d8d5e9e4010272b2df5713b031 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Fri, 1 Sep 2023 10:18:29 +0200
Subject: [PATCH 15/20] [ ci ] Enable the pack-lsp test

This is going to be exciting!
---
 .github/workflows/ci-extern-libs.yml | 84 +++++++++++++---------------
 1 file changed, 40 insertions(+), 44 deletions(-)

diff --git a/.github/workflows/ci-extern-libs.yml b/.github/workflows/ci-extern-libs.yml
index 9d4e5baa91..f410358508 100644
--- a/.github/workflows/ci-extern-libs.yml
+++ b/.github/workflows/ci-extern-libs.yml
@@ -160,7 +160,7 @@ jobs:
   # Test that we can build Collie
   ########################################################################
 
-  ubuntu-test-collie:
+  test-collie:
     needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |
@@ -192,7 +192,7 @@ jobs:
   # Test that we can build Frex
   ########################################################################
 
-  ubuntu-test-frex:
+  test-frex:
     needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |
@@ -227,7 +227,7 @@ jobs:
 
   # ELAB
 
-  ubuntu-test-elab:
+  test-elab-util:
     needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |
@@ -257,7 +257,7 @@ jobs:
 
   # PACK
 
-  ubuntu-test-pack:
+  test-pack:
     needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |
@@ -289,51 +289,47 @@ jobs:
           git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
           pack install pack
 
-# FIXME: use pack instead, once it's working; otherwise the Idris version is wrong
-#  ######################################################################
-#  # Test that we can build the LSP
-#  ######################################################################
-#
-#  ubuntu-test-lsp:
-#    needs: ubuntu-self-host-previous-version
-#    runs-on: ubuntu-latest
-#    if: |
-#      !contains(needs.initialise.outputs.commit_message, '[ci:')
-#      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-#    env:
-#      IDRIS2_CG: chez
-#    steps:
-#      - name: Download Idris2 Artifact
-#        uses: actions/download-artifact@v3
-#        with:
-#          name: idris2-nightly-chez
-#          path: ~/.idris2/
-#      - name: Install chezscheme
-#        run: |
-#          sudo apt-get update
-#          sudo apt-get install -y chezscheme
-#          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-#          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-#      - name: Checkout
-#        uses: actions/checkout@v3
-#        with:
-#          repository: 'idris-community/idris2-lsp'
-#      - name: Install libs and API
-#        run: |
-#          git submodule update --init Idris2
-#          cd Idris2
-#          make all
-#          make install-with-src-libs
-#          make install-with-src-api
-#      - name: Build idris2-lsp
-#        run: |
-#          make all
+  ######################################################################
+  # Test that we can build the LSP
+  ######################################################################
+
+  test-lsp-pack:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+      PACK_DIR: /root/.pack
+    container: ghcr.io/stefan-hoeck/idris2-pack:latest
+    strategy:
+      fail-fast: false
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'idris-community/idris2-lsp'
+      - name: Toml setup
+        run: |
+          echo "[idris2]" > pack.toml
+          echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
+          echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
+          echo "bootstrap  = true" >> pack.toml
+      - name: Build pack with PR-Idris
+        run: |
+          git config --global --add safe.directory "${PWD}"
+          git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
+          pack install pack
+      - name: Build+install idris2-lsp
+        run: |
+          pack install-app idris2-lsp
 
   ######################################################################
   # Test that we can use Katla to build html doc of the libs
   ######################################################################
 
-  ubuntu-katla:
+  test-katla-and-html:
     needs: ubuntu-self-host-previous-version
     runs-on: ubuntu-latest
     if: |

From 526847d2ec713218e325112ad12bfa8426664ee3 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Fri, 1 Sep 2023 11:52:50 +0200
Subject: [PATCH 16/20] [ ci ] Don't prompt before building lsp

We trust LSP, at least for CI-purposes
---
 .github/workflows/ci-extern-libs.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci-extern-libs.yml b/.github/workflows/ci-extern-libs.yml
index f410358508..dbcc3670c4 100644
--- a/.github/workflows/ci-extern-libs.yml
+++ b/.github/workflows/ci-extern-libs.yml
@@ -323,7 +323,7 @@ jobs:
           pack install pack
       - name: Build+install idris2-lsp
         run: |
-          pack install-app idris2-lsp
+          pack --no-prompt install-app idris2-lsp
 
   ######################################################################
   # Test that we can use Katla to build html doc of the libs

From 1f97374981d444e7e6b27094d76dac3c36d6e9b2 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Fri, 8 Sep 2023 14:25:52 +0200
Subject: [PATCH 17/20] [ ci ] Avoid work duplication in idris2 vs ext-libs

As per discussion on PR #3067
---
 .github/workflows/ci-extern-libs.yml | 414 ---------------------------
 .github/workflows/ci-idris2.yml      | 270 ++++++++++++++++-
 2 files changed, 269 insertions(+), 415 deletions(-)
 delete mode 100644 .github/workflows/ci-extern-libs.yml

diff --git a/.github/workflows/ci-extern-libs.yml b/.github/workflows/ci-extern-libs.yml
deleted file mode 100644
index dbcc3670c4..0000000000
--- a/.github/workflows/ci-extern-libs.yml
+++ /dev/null
@@ -1,414 +0,0 @@
-name: Build External Libraries
-
-######################################################################
-# Ubuntu testing some libraries.
-# We are particularly interested in libraries that are heavily using
-# dependent types, that are prone to find bugs and regressions in the
-# compiler.
-######################################################################
-
-on:
-  push:
-    branches:
-      - '*'
-    tags:
-      - '*'
-    paths-ignore:
-      - 'docs/**'
-      - 'icons/**'
-      - 'Release/**'
-      - '**.md'
-      - 'CONTRIBUTORS'
-      - 'LICENSE'
-      - 'CHANGELOG.md'
-      - '.github/workflows/ci-bootstrap.yml'
-      - '.github/workflows/ci-lint.yml'
-      - '.github/workflows/ci-sphinx.yml'
-      - '.github/workflows/ci-super-linter.yml'
-  pull_request:
-    branches:
-      - main
-    paths-ignore:
-      - 'docs/**'
-      - 'icons/**'
-      - 'Release/**'
-      - '**.md'
-      - 'CONTRIBUTORS'
-      - 'LICENSE'
-      - '.github/workflows/ci-bootstrap.yml'
-      - '.github/workflows/ci-lint.yml'
-      - '.github/workflows/ci-sphinx.yml'
-      - '.github/workflows/ci-super-linter.yml'
-
-concurrency:
-  group: extlibs-${{ github.ref }}
-  cancel-in-progress: true
-
-env:
-  IDRIS2_MINIMUM_COMPAT_VERSION: 0.6.0
-
-jobs:
-
-  # First 3 jobs blatantly stolen from ci-idris2
-
-  initialise:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout Project
-        uses: actions/checkout@v3
-        with:
-          # for pull_request so we can do HEAD^2
-          fetch-depth: 2
-
-      - name: Get commit message
-        id: get_commit_message
-        run: |
-          if   [[ '${{ github.event_name }}' == 'push' ]]; then
-            echo "commit_message=$(git log --format=%B -n 1 HEAD | tr '\n' ' ')" >> "$GITHUB_OUTPUT"
-          elif [[ '${{ github.event_name }}' == 'pull_request' ]]; then
-            echo "commit_message=$(git log --format=%B -n 1 HEAD^2 | tr '\n' ' ')" >> "$GITHUB_OUTPUT"
-          fi
-
-    outputs:
-      commit_message:
-        echo "${{ steps.get_commit_message.outputs.commit_message }}"
-
-  quick-check:
-    needs: initialise
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci: skip]')
-    env:
-      IDRIS2_CG: chez
-      SCHEME: scheme
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v3
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-
-      # Get our hands on the released version either by using the cache
-      # or by rebuilding it if necessary.
-      - name: Cache Chez Previous Version
-        id: previous-version-cache
-        uses: actions/cache@v3
-        with:
-          path: Idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}
-          key: ${{ runner.os }}-idris2-bootstrapped-chez-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}
-      - name : Build previous version
-        if: steps.previous-version-cache.outputs.cache-hit != 'true'
-        run: |
-          wget "https://www.idris-lang.org/idris2-src/idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz"
-          tar zxvf "idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz"
-          cd "Idris2-$IDRIS2_MINIMUM_COMPAT_VERSION"
-          make bootstrap
-          cd ..
-      - name: Install previous version
-        run: |
-          cd "Idris2-$IDRIS2_MINIMUM_COMPAT_VERSION"
-          make install
-          cd ..
-
-      # Build the current version and save the installation.
-      - name: Build current version
-        run: |
-          make && make install
-      - name: Artifact Idris2 from previous version
-        uses: actions/upload-artifact@v3
-        with:
-          name: ubuntu-installed-idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}-chez
-          path: ~/.idris2/
-
-  ubuntu-self-host-previous-version:
-    needs: [initialise, quick-check]
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: ubuntu]')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v3
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: ubuntu-installed-idris2-${{ env.IDRIS2_MINIMUM_COMPAT_VERSION }}-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Build self-hosted from previous version
-        run: make all IDRIS2_BOOT="idris2 -Werror" && make install
-      - name: Test self-hosted from previous version
-        run: make ci-ubuntu-test INTERACTIVE=''
-      - name: Artifact Idris2
-        uses: actions/upload-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-
-
-  ########################################################################
-  # Test that we can build Collie
-  ########################################################################
-
-  test-collie:
-    needs: ubuntu-self-host-previous-version
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'ohad/collie'
-      - name: Build Collie
-        run: |
-          make
-
-  ########################################################################
-  # Test that we can build Frex
-  ########################################################################
-
-  test-frex:
-    needs: ubuntu-self-host-previous-version
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'frex-project/idris-frex'
-      - name: Build Frex
-        run: |
-          make
-          make test
-
-  ######################################################################
-  # Test that we can build Stefan Höck's elab-util and pack
-  ######################################################################
-
-  # ELAB
-
-  test-elab-util:
-    needs: ubuntu-self-host-previous-version
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'stefan-hoeck/idris2-elab-util'
-      - name: Build idris2-elab-util
-        run: |
-          make all
-
-  # PACK
-
-  test-pack:
-    needs: ubuntu-self-host-previous-version
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-      PACK_DIR: /root/.pack
-    strategy:
-      fail-fast: false
-    # instead of bootstrapping pack, load the dockerimage where it is already
-    # we'll then use pack to build pack with this job's idris2 sources
-    container: ghcr.io/stefan-hoeck/idris2-pack:latest
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'stefan-hoeck/idris2-pack'
-      # by default, pack uses the main idris2 head, not the current job's one
-      - name: Toml setup
-        run: |
-          echo "[idris2]" > pack.toml
-          echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
-          echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
-          echo "bootstrap  = true" >> pack.toml
-      - name: Build idris2-pack
-        run: |
-          git config --global --add safe.directory "${PWD}"
-          git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
-          pack install pack
-
-  ######################################################################
-  # Test that we can build the LSP
-  ######################################################################
-
-  test-lsp-pack:
-    needs: ubuntu-self-host-previous-version
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
-    env:
-      IDRIS2_CG: chez
-      PACK_DIR: /root/.pack
-    container: ghcr.io/stefan-hoeck/idris2-pack:latest
-    strategy:
-      fail-fast: false
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          repository: 'idris-community/idris2-lsp'
-      - name: Toml setup
-        run: |
-          echo "[idris2]" > pack.toml
-          echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
-          echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
-          echo "bootstrap  = true" >> pack.toml
-      - name: Build pack with PR-Idris
-        run: |
-          git config --global --add safe.directory "${PWD}"
-          git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
-          pack install pack
-      - name: Build+install idris2-lsp
-        run: |
-          pack --no-prompt install-app idris2-lsp
-
-  ######################################################################
-  # Test that we can use Katla to build html doc of the libs
-  ######################################################################
-
-  test-katla-and-html:
-    needs: ubuntu-self-host-previous-version
-    runs-on: ubuntu-latest
-    if: |
-      !contains(needs.initialise.outputs.commit_message, '[ci:')
-      || contains(needs.initialise.outputs.commit_message, '[ci: html]')
-    env:
-      IDRIS2_CG: chez
-    steps:
-
-      - name: Initialise DEPLOY variable
-        run: |
-          if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then
-             echo "IDRIS2_DEPLOY=true" >> "$GITHUB_ENV"
-          fi
-
-      - name: Download Idris2 Artifact
-        uses: actions/download-artifact@v3
-        with:
-          name: idris2-nightly-chez
-          path: ~/.idris2/
-      - name: Install build dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y chezscheme markdown
-          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
-          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
-      - name: Checkout idris2
-        uses: actions/checkout@v3
-      - name: Build API
-        run: make install-api
-        shell: bash
-      - name: Checkout collie
-        uses: actions/checkout@v3
-        with:
-          repository: 'ohad/collie'
-      - name: Build and install Collie
-        run: |
-          make install
-      - name: Checkout idrall
-        uses: actions/checkout@v3
-        with:
-          repository: 'alexhumphreys/idrall'
-      - name: Build and install idrall
-        run: |
-          make install
-      - name: Checkout katla
-        uses: actions/checkout@v3
-        with:
-          repository: 'idris-community/katla'
-      - name: Build and install katla
-        run: |
-          make
-          mkdir -p "${HOME}"/.local/bin/
-          cp -r build/exec/* "${HOME}"/.local/bin/
-          echo "${HOME}/.local/bin" >> "$GITHUB_PATH"
-      - name: Checkout idris2
-        uses: actions/checkout@v3
-      - name: Build html doc & landing page
-        run: |
-          make -C libs/prelude/ install docs IDRIS2=idris2
-          make -C libs/base/ install docs IDRIS2=idris2
-          make -C libs/contrib/ install docs IDRIS2=idris2
-          make -C libs/network/ install docs IDRIS2=idris2
-          make -C libs/linear/ install docs IDRIS2=idris2
-          make -C libs/test/ install docs IDRIS2=idris2
-          make -C libs/papers/ install docs IDRIS2=idris2
-
-          cd .github/scripts
-          ./katla.sh
-          cd -
-          cd www/
-          ./katla.sh
-          cd -
-          cp -r www/html/* .github/scripts/html/
-      - name: Deploy HTML
-        uses: JamesIves/github-pages-deploy-action@4.1.3
-        if: ${{ success() && env.IDRIS2_DEPLOY }}
-
-        with:
-          branch: gh-pages
-          folder: .github/scripts/html/
-          git-config-name: Github Actions
diff --git a/.github/workflows/ci-idris2.yml b/.github/workflows/ci-idris2.yml
index 736491fd69..c074275668 100644
--- a/.github/workflows/ci-idris2.yml
+++ b/.github/workflows/ci-idris2.yml
@@ -1,4 +1,4 @@
-name: Idris2
+name: Idris2 and External Libs
 
 on:
   push:
@@ -486,3 +486,271 @@ jobs:
         run: cd tests/idris2/api001 && ./run idris2
         shell: bash
 
+  ######################################################################
+  # Testing some libraries on Ubuntu and pack.
+  #
+  # We are particularly interested in libraries that are heavily using
+  # dependent types, that are prone to find bugs and regressions in the
+  # compiler.
+  ######################################################################
+
+  ######################################################################
+  # Test that we can build Collie
+  ######################################################################
+
+  ub-test-collie:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'ohad/collie'
+      - name: Build Collie
+        run: |
+          make
+
+  ########################################################################
+  # Test that we can build Frex
+  ########################################################################
+
+  ub-test-frex:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'frex-project/idris-frex'
+      - name: Build Frex
+        run: |
+          make
+          make test
+
+  ######################################################################
+  # Test that we can build Stefan Höck's elab-util and pack
+  ######################################################################
+
+  # ELAB-UTIL
+
+  ub-test-elab-util:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'stefan-hoeck/idris2-elab-util'
+      - name: Build idris2-elab-util
+        run: |
+          make all
+
+  # PACK
+  #
+  # N.B. instead of bootstrapping pack, we use the dockerimage where it is
+  # already, and then use pack to rebuild pack with this job's idris2 sources
+
+  ub-pack-test-pack:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+      PACK_DIR: /root/.pack
+    strategy:
+      fail-fast: false
+    # N.B.:
+    container: ghcr.io/stefan-hoeck/idris2-pack:latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'stefan-hoeck/idris2-pack'
+      # by default, pack uses the main idris2 head, not the current job's one
+      - name: Toml setup
+        run: |
+          echo "[idris2]" > pack.toml
+          echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
+          echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
+          echo "bootstrap  = true" >> pack.toml
+      - name: Build idris2-pack
+        run: |
+          git config --global --add safe.directory "${PWD}"
+          git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
+          pack install pack
+
+  ######################################################################
+  # Test that we can build the LSP
+  ######################################################################
+
+  ub-pack-test-lsp:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: libs]')
+    env:
+      IDRIS2_CG: chez
+      PACK_DIR: /root/.pack
+    # LSP is vastly easier to build using pack, so do that
+    container: ghcr.io/stefan-hoeck/idris2-pack:latest
+    strategy:
+      fail-fast: false
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          repository: 'idris-community/idris2-lsp'
+      - name: Toml setup
+        run: |
+          echo "[idris2]" > pack.toml
+          echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
+          echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
+          echo "bootstrap  = true" >> pack.toml
+      # make sure pack is running the PR's Idris2 before building LSP
+      - name: Build pack with PR-Idris
+        run: |
+          git config --global --add safe.directory "${PWD}"
+          git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
+          pack install pack
+      - name: Build+install idris2-lsp
+        run: |
+          pack --no-prompt install-app idris2-lsp
+
+  ######################################################################
+  # Test that we can use Katla to build html doc of the libs
+  ######################################################################
+
+  ub-test-katla-and-html:
+    needs: ubuntu-self-host-previous-version
+    runs-on: ubuntu-latest
+    if: |
+      !contains(needs.initialise.outputs.commit_message, '[ci:')
+      || contains(needs.initialise.outputs.commit_message, '[ci: html]')
+    env:
+      IDRIS2_CG: chez
+    steps:
+
+      - name: Initialise DEPLOY variable
+        run: |
+          if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then
+             echo "IDRIS2_DEPLOY=true" >> "$GITHUB_ENV"
+          fi
+
+      - name: Download Idris2 Artifact
+        uses: actions/download-artifact@v3
+        with:
+          name: idris2-nightly-chez
+          path: ~/.idris2/
+      - name: Install build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme markdown
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          chmod +x "$HOME/.idris2/bin/idris2" "$HOME/.idris2/bin/idris2_app/"*
+      - name: Checkout idris2
+        uses: actions/checkout@v3
+      - name: Build API
+        run: make install-api
+        shell: bash
+      - name: Checkout collie
+        uses: actions/checkout@v3
+        with:
+          repository: 'ohad/collie'
+      - name: Build and install Collie
+        run: |
+          make install
+      - name: Checkout idrall
+        uses: actions/checkout@v3
+        with:
+          repository: 'alexhumphreys/idrall'
+      - name: Build and install idrall
+        run: |
+          make install
+      - name: Checkout katla
+        uses: actions/checkout@v3
+        with:
+          repository: 'idris-community/katla'
+      - name: Build and install katla
+        run: |
+          make
+          mkdir -p "${HOME}"/.local/bin/
+          cp -r build/exec/* "${HOME}"/.local/bin/
+          echo "${HOME}/.local/bin" >> "$GITHUB_PATH"
+      - name: Checkout idris2
+        uses: actions/checkout@v3
+      - name: Build html doc & landing page
+        run: |
+          make -C libs/prelude/ install docs IDRIS2=idris2
+          make -C libs/base/ install docs IDRIS2=idris2
+          make -C libs/contrib/ install docs IDRIS2=idris2
+          make -C libs/network/ install docs IDRIS2=idris2
+          make -C libs/linear/ install docs IDRIS2=idris2
+          make -C libs/test/ install docs IDRIS2=idris2
+          make -C libs/papers/ install docs IDRIS2=idris2
+
+          cd .github/scripts
+          ./katla.sh
+          cd -
+          cd www/
+          ./katla.sh
+          cd -
+          cp -r www/html/* .github/scripts/html/
+      - name: Deploy HTML
+        uses: JamesIves/github-pages-deploy-action@4.1.3
+        if: ${{ success() && env.IDRIS2_DEPLOY }}
+
+        with:
+          branch: gh-pages
+          folder: .github/scripts/html/
+          git-config-name: Github Actions

From 4d27adcbaa1f466cef623ff81eacb7c6010e6b80 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Fri, 8 Sep 2023 14:27:18 +0200
Subject: [PATCH 18/20] [ ci ] Rename idris2 CI job to reflect lib building

The job builds Idris2, but also several external libraries. Name
accordingly.
---
 .github/workflows/{ci-idris2.yml => ci-idris2-and-libs.yml} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename .github/workflows/{ci-idris2.yml => ci-idris2-and-libs.yml} (100%)

diff --git a/.github/workflows/ci-idris2.yml b/.github/workflows/ci-idris2-and-libs.yml
similarity index 100%
rename from .github/workflows/ci-idris2.yml
rename to .github/workflows/ci-idris2-and-libs.yml

From 836476925b3296e69c0626fca35beb2da771f5a1 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 11 Sep 2023 17:18:53 +0200
Subject: [PATCH 19/20] [ ci ] Depend on 'initialise' to make linter happy

---
 .github/workflows/ci-idris2-and-libs.yml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/ci-idris2-and-libs.yml b/.github/workflows/ci-idris2-and-libs.yml
index 2cb868ee8a..dcf39e37a9 100644
--- a/.github/workflows/ci-idris2-and-libs.yml
+++ b/.github/workflows/ci-idris2-and-libs.yml
@@ -499,7 +499,7 @@ jobs:
   ######################################################################
 
   ub-test-collie:
-    needs: ubuntu-self-host-previous-version
+    needs: [initialise, ubuntu-self-host-previous-version]
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')
@@ -531,7 +531,7 @@ jobs:
   ########################################################################
 
   ub-test-frex:
-    needs: ubuntu-self-host-previous-version
+    needs: [initialise, ubuntu-self-host-previous-version]
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')
@@ -566,7 +566,7 @@ jobs:
   # ELAB-UTIL
 
   ub-test-elab-util:
-    needs: ubuntu-self-host-previous-version
+    needs: [initialise, ubuntu-self-host-previous-version]
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')
@@ -599,7 +599,7 @@ jobs:
   # already, and then use pack to rebuild pack with this job's idris2 sources
 
   ub-pack-test-pack:
-    needs: ubuntu-self-host-previous-version
+    needs: [initialise, ubuntu-self-host-previous-version]
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')
@@ -634,7 +634,7 @@ jobs:
   ######################################################################
 
   ub-pack-test-lsp:
-    needs: ubuntu-self-host-previous-version
+    needs: [initialise, ubuntu-self-host-previous-version]
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')
@@ -672,7 +672,7 @@ jobs:
   ######################################################################
 
   ub-test-katla-and-html:
-    needs: ubuntu-self-host-previous-version
+    needs: [initialise, ubuntu-self-host-previous-version]
     runs-on: ubuntu-latest
     if: |
       !contains(needs.initialise.outputs.commit_message, '[ci:')

From 2a96c36fd9c35e91afcbeb8d39160a12078591c0 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 11 Sep 2023 19:19:05 +0200
Subject: [PATCH 20/20] [ ci ] Group pack toml file-writing commands

According to the linter this is better(?)
---
 .github/workflows/ci-idris2-and-libs.yml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/ci-idris2-and-libs.yml b/.github/workflows/ci-idris2-and-libs.yml
index dcf39e37a9..f7d5fe3223 100644
--- a/.github/workflows/ci-idris2-and-libs.yml
+++ b/.github/workflows/ci-idris2-and-libs.yml
@@ -619,10 +619,11 @@ jobs:
       # by default, pack uses the main idris2 head, not the current job's one
       - name: Toml setup
         run: |
-          echo "[idris2]" > pack.toml
-          echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
-          echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
-          echo "bootstrap  = true" >> pack.toml
+          { echo "[idris2]"
+            echo "url = \"https://github.com/${GITHUB_REPOSITORY}\""
+            echo "commit = \"latest:${GITHUB_REF_NAME}\""
+            echo "bootstrap  = true"
+          } > pack.toml
       - name: Build idris2-pack
         run: |
           git config --global --add safe.directory "${PWD}"
@@ -653,10 +654,11 @@ jobs:
           repository: 'idris-community/idris2-lsp'
       - name: Toml setup
         run: |
-          echo "[idris2]" > pack.toml
-          echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
-          echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
-          echo "bootstrap  = true" >> pack.toml
+          { echo "[idris2]"
+            echo "url = \"https://github.com/${GITHUB_REPOSITORY}\""
+            echo "commit = \"latest:${GITHUB_REF_NAME}\""
+            echo "bootstrap  = true"
+          } > pack.toml
       # make sure pack is running the PR's Idris2 before building LSP
       - name: Build pack with PR-Idris
         run: |