build: upgrade many things in ci

.github/README.md

@@ -19,9 +19,14 @@ Aya is under active development, so please expect bugs, usability or performance
 + Dependent types, including pi-types, sigma types, indexed families, etc.
   You could write a [sized-vector type][gadt].
 + Set-level cubical type theory (XTT).
-  + Demonstration of [higher-inductive-inductive-recursive types][hiir].
+  + Demonstration of [quotient-inductive-inductive types][hiir],
+    no forward declaration or mutual block needed!
+    We infer the type checking order by how definitions use each other.
+  + Proof of `funExt` in [Paths.aya][funExt].
 + Pattern matching with first-match semantics.
   Checkout the [red-black tree][rbtree] (without deletion yet).
++ A JIT-compiler that translates Aya code to higher-order abstract syntax in Java.
+  This makes the interpreter to run tree-sort 10x faster! See [benchmark code][tbtree-bench].
 + Overlapping and order-independent patterns. Very [useful][oop] in theorem proving.
 + A literate programming mode with inline code fragment support, inspired from Agda and [1lab].
   You may preview the features (in Chinese)
@@ -32,10 +37,6 @@ Aya is under active development, so please expect bugs, usability or performance
 + A fairly good termination checker.
   We adapted some code from Agda's implementation to accept
   [more definitions][foetus] (which are rejected by, e.g. Arend).
-+ Inference of type checking order. That is to say,
-  no syntax for forward-declarations is needed for [mutual recursions][mutual],
-  induction-recursion, or induction-induction.
-+ See also stdlib candidates [style guide][stdlib-style]. We have a grand plan!
 
 See also [use as a library](#use-as-a-library).
 
@@ -71,13 +72,12 @@ of IDE is IntelliJ IDEA, version 2023.3 or higher is required.
 [gadt]: ../cli-impl/src/test/resources/shared/src/Data/Vec.aya
 [regularity]: ../cli-impl/src/test/resources/shared/src/Paths.aya
 [funExt]: ../cli-impl/src/test/resources/shared/src/Paths.aya
-[rbtree]: ../cli-impl/src/test/resources/shared/src/Data/Tree/RedBlack/Direct.aya
+[rbtree]: ../jit-compiler/src/test/resources/TreeSort.aya
+[tbtree-bench]: ../jit-compiler/src/test/java/RedBlackTreeTest.java
 [hiir]: ../cli-impl/src/test/resources/shared/src/TypeTheory/Thorsten.aya
 [assoc]: ../base/src/test/resources/success/src/Assoc.aya
 [foetus]: ../base/src/test/resources/success/src/FoetusLimitation.aya
-[mutual]: ../base/src/test/resources/success/src/Order.aya
 [maven-repo]: https://repo1.maven.org/maven2/org/aya-prover
-[stdlib-style]: ../cli-impl/src/test/resources/shared
 
 ## Use as a library
 

.github/workflows/commit-check.yaml

@@ -8,7 +8,7 @@ jobs:
   commit-check:
     runs-on: ubuntu-20.04
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           fetch-depth: 0
           ref: ${{ github.event.pull_request.head.sha }}

.github/workflows/extract-version.yaml

@@ -19,7 +19,7 @@ jobs:
       isSnapshot: ${{ steps.check.outputs.isSnapshot }}
       javaVersion: ${{ steps.check.outputs.javaVersion }}
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Extract versions from Gradle's libs.versions.toml
         id: check
         shell: bash

.github/workflows/gradle-check.yaml

@@ -14,24 +14,24 @@ jobs:
     needs: [check-aya-version]
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Setup Java ${{ needs.check-aya-version.outputs.javaVersion }}
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           distribution: 'liberica'
           java-version: ${{ needs.check-aya-version.outputs.javaVersion }}
-      - uses: gradle/gradle-build-action@v2
+      - uses: gradle/gradle-build-action@v3
         with:
           arguments: testCodeCoverageReport --no-daemon --stacktrace --warning-mode all
       - name: Test report
-        uses: mikepenz/action-junit-report@v3
+        uses: mikepenz/action-junit-report@v4
         if: always()
         with:
           check_name: junit-tests
           report_paths: '**/build/test-results/test/TEST-*.xml'
       - name: Upload coverage to Codecov
         if: github.base_ref != null
-        uses: codecov/codecov-action@v3
+        uses: codecov/codecov-action@v4
         with:
           token: ${{ secrets.CODECOV_TOKEN }}
           files: ./build/reports/jacoco/testCodeCoverageReport/testCodeCoverageReport.xml

.github/workflows/nightly-build.yaml

@@ -27,14 +27,14 @@ jobs:
       ossrhUsername: ${{ secrets.OSSRHUSERNAME }}
       ossrhPassword: ${{ secrets.OSSRHPASSWORD }}
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Setup Java ${{ needs.check-aya-version.outputs.javaVersion }}
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           distribution: 'liberica'
           java-version: ${{ needs.check-aya-version.outputs.javaVersion }}
       - name: gradle publish
-        uses: gradle/gradle-build-action@v2
+        uses: gradle/gradle-build-action@v3
         with:
           arguments: publish --info --no-daemon --stacktrace --warning-mode all
 
@@ -55,22 +55,22 @@ jobs:
             platform: 'windows-x64'
             binaryExt: '.exe'
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Setup Java ${{ needs.check-aya-version.outputs.javaVersion }}
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           distribution: 'liberica'
           java-version: ${{ needs.check-aya-version.outputs.javaVersion }}
 
       - name: Run task jlinkAyaZip
-        uses: gradle/gradle-build-action@v2
+        uses: gradle/gradle-build-action@v3
         with:
           arguments: jlinkAyaZip --info --no-daemon --stacktrace --warning-mode all
         if: matrix.os == 'ubuntu-latest'
 
       - name: Run task fatJar
-        uses: gradle/gradle-build-action@v2
+        uses: gradle/gradle-build-action@v3
         with:
           arguments: fatJar --no-daemon --stacktrace --warning-mode all
         if: matrix.os == 'ubuntu-latest'

gradle/libs.versions.toml

@@ -9,10 +9,10 @@ java = "21"
 
 # https://github.com/JetBrains/java-annotations
 annotations = "24.1.0"
-kala = "0.72.0"
+kala = "0.73.0"
 # https://picocli.info
 picocli = "4.7.6"
-build-util = "0.0.22"
+build-util = "0.0.24"
 # https://github.com/jline/jline3
 jline = "3.26.1"
 # https://github.com/commonmark/commonmark-java