agda · andreasabel · Jul 6, 2023 · Jul 21, 2023 · Jul 25, 2023 · Jul 25, 2023
diff --git a/.github/haskell-ci.patch b/.github/haskell-ci.patch
@@ -8,7 +8,7 @@
 +      - .github/workflows/haskell-ci.yml
 +      - agda-stdlib-utils.cabal
 +      - cabal.haskell-ci
-+      - *.hs
++      - "*.hs"
    pull_request:
      branches:
        - master
@@ -17,7 +17,7 @@
 +      - .github/workflows/haskell-ci.yml
 +      - agda-stdlib-utils.cabal
 +      - cabal.haskell-ci
-+      - *.hs
++      - "*.hs"
  jobs:
    linux:
      name: Haskell-CI - Linux - ${{ matrix.compiler }}
diff --git a/.github/tooling/agda-logo.svg b/.github/tooling/agda-logo.svg
diff --git a/travis/index.agda → .github/tooling/index.agda b/travis/index.agda → .github/tooling/index.agda
diff --git a/travis/index.sh → .github/tooling/index.sh b/travis/index.sh → .github/tooling/index.sh
diff --git a/.github/tooling/landing-bottom.html b/.github/tooling/landing-bottom.html
@@ -0,0 +1,4 @@
+      </ul>
+    </div>
+  </body>
+</html>
diff --git a/.github/tooling/landing-top.html b/.github/tooling/landing-top.html
@@ -0,0 +1,24 @@
+<html>
+
+  <head>
+    <title>Documention for the Agda standard library</title>
+  </head>
+
+  <body>
+
+    <div id="container" style="width:50%;min-width:500px;margin:auto">
+      <img src="agda-logo.svg" style="width:80px;float:right" />
+      <h1>Documention for the Agda standard library</h1>
+
+      <hr />
+
+      <h2>Development versions</h2>
+
+      <ul>
+        <li><a href="master">master</a></li>
+        <li><a href="experimental">experimental</a></li>
+      </ul>
+
+      <h2>Released versions</h2>
+
+      <ul>
diff --git a/.github/tooling/landing.sh b/.github/tooling/landing.sh
@@ -0,0 +1,18 @@
+set -eu
+set -o pipefail
+
+rm html/index.html
+
+cat landing-top.html >> landing.html
+
+find html/ -name "index.html" \
+  | grep -v "master\|experimental" \
+  | sed 's|html/\([^\/]*\)/index.html|\1|g' \
+  | sort -r \
+  | sed 's|^\(.*\)$|        <li><a href="\1">\1</a></li>|g' \
+  >> landing.html
+
+cat landing-bottom.html >> landing.html
+
+mv landing.html html/index.html
+mv agda-logo.svg html/
diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
@@ -8,6 +8,7 @@ on:
     branches:
       - master
       - experimental
+  merge_group:
 
 ########################################################################
 ## CONFIGURATION
@@ -46,11 +47,11 @@ on:
 ########################################################################
 
 env:
-  GHC_VERSION: 8.10.7
-  CABAL_VERSION: 3.6.2.0
+  GHC_VERSION: 9.8.2
+  CABAL_VERSION: 3.10.3.0
   CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
   # CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
-  AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -i src/
+  AGDA: agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc
 
 jobs:
   test-stdlib:
@@ -71,21 +72,20 @@ jobs:
 
       - name: Initialise variables
         run: |
-          if [[ '${{ github.ref }}' == 'refs/heads/master' \
-             || '${{ github.base_ref }}' == 'master' ]]; then
-            # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.6.2" >> $GITHUB_ENV;
-            echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV
-          elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \
-               || '${{ github.base_ref }}' == 'experimental' ]]; then
+          if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
+             || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=4d36cb37f8bfb765339b808b13356d760aa6f0ec" >> $GITHUB_ENV;
-            echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV
+            echo "AGDA_COMMIT=f25a71a1c1d22c8702514df22e4f206982c15f40" >> "${GITHUB_ENV}";
+            echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
+          else
+            # Pick Agda version for master
+            echo "AGDA_COMMIT=tags/v2.6.4.3" >> "${GITHUB_ENV}";
+            echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
           fi
 
           if [[ '${{ github.ref }}' == 'refs/heads/master' \
              || '${{ github.ref }}' == 'refs/heads/experimental' ]]; then
-             echo "AGDA_DEPLOY=true" >> $GITHUB_ENV
+             echo "AGDA_DEPLOY=true" >> "${GITHUB_ENV}"
           fi
 
 ########################################################################
@@ -98,7 +98,7 @@ jobs:
       # i.e. if we change either the version of Agda, ghc, or cabal that we want
       # to use for the build.
       - name: Cache ~/.cabal directories
-        uses: actions/cache@v2
+        uses: actions/cache@v4
         id: cache-cabal
         with:
           path: |
@@ -113,18 +113,17 @@ jobs:
 ########################################################################
 
       - name: Install ghc & cabal
-        uses: haskell/actions/setup@v1
+        uses: haskell-actions/setup@v2
         with:
           ghc-version: ${{ env.GHC_VERSION }}
           cabal-version: ${{ env.CABAL_VERSION }}
+          cabal-update: true
 
       - name: Put cabal programs in PATH
-        run: echo "~/.cabal/bin" >> $GITHUB_PATH
-
-      - name: Cabal update
-        run: cabal update
+        run: echo "~/.cabal/bin" >> "${GITHUB_PATH}"
 
       - name: Install alex & happy
+        if: steps.cache-cabal.outputs.cache-hit != 'true'
         run: |
           ${{ env.CABAL_INSTALL }} alex
           ${{ env.CABAL_INSTALL }} happy
@@ -146,14 +145,23 @@ jobs:
 
       # By default github actions do not pull the repo
       - name: Checkout stdlib
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
 
       - name: Test stdlib
         run: |
+          # Including deprecated modules purely for testing
+          cabal run GenerateEverything -- --include-deprecated
+          ${{ env.AGDA }} -WnoUserWarning --safe EverythingSafe.agda
+          ${{ env.AGDA }} -WnoUserWarning Everything.agda
+
+      - name: Prepare HTML index
+        run: |
+          # Regenerating the Everything files without the deprecated modules
           cabal run GenerateEverything
-          cp travis/* .
+          cp .github/tooling/* .
           ./index.sh
           ${{ env.AGDA }} --safe EverythingSafe.agda
+          ${{ env.AGDA }} Everything.agda
           ${{ env.AGDA }} index.agda
 
       - name: Golden testing
@@ -176,10 +184,12 @@ jobs:
           rm -f '${{ env.AGDA_HTML_DIR }}'/*.html
           rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
           ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda
+          cp .github/tooling/* .
+          ./landing.sh
 
       - name: Deploy HTML
         uses: JamesIves/github-pages-deploy-action@4.1.3
-        if: ${{ success() && env.AGDA_DEPLOY }}
+        if: success() && env.AGDA_DEPLOY
 
         with:
           branch: gh-pages