Merge from main branch.

.github/workflows/build.yml

@@ -17,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        java_version: [11, 17, 18, 19]
+        java_version: [11, 17, 21]
         experimental: [false]
     continue-on-error: ${{ matrix.experimental }}
     steps:

.github/workflows/docs.yml

@@ -4,32 +4,32 @@ on:
   push:
     branches: [ main ]
   pull_request:
-    branches:
-      - main
+    branches: [ main ]
 
 jobs:
   # Runs on PRs and push to ensure the documentation successfully builds.
   build:
     name: Build Documentation
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - name: Check out project
+        uses: actions/checkout@v4
 
-      - uses: actions/setup-node@v4
+      - name: Set up Java
+        uses: actions/setup-java@v4
         with:
-          node-version: 18
+          distribution: temurin
+          java-version: 22
 
-      - name: Install Dependencies
-        run: npm install
-        working-directory: docs
+      - name: Set up Gradle
+        uses: gradle/actions/setup-gradle@v3
 
-      - name: Build Documentation
-        run: npm run build
-        working-directory: docs
+      - name: Build docs
+        run: ./gradlew buildDocs
 
-      - uses: actions/upload-artifact@v4
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v3
         with:
-          name: document
           path: docs/build
 
   # Deploys the documentation if this is a push to the main branch.
@@ -38,15 +38,18 @@ jobs:
     if: github.event_name == 'push' && github.ref == 'refs/heads/main'
     needs: build
     runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
 
-      - uses: actions/download-artifact@v4
-        with:
-          name: document
-          path: docs/build
+    # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
+    permissions:
+      pages: write      # to deploy to Pages
+      id-token: write   # to verify the deployment originates from an appropriate source
 
-      - uses: JamesIves/[email protected]
-        with:
-          branch: gh-pages
-          folder: docs/build
+    # Deploy to the github-pages environment
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4

build.gradle

@@ -16,8 +16,9 @@
 
 plugins {
     id 'java-library'
+    id 'com.diffplug.spotless' version '6.25.0'
+    id 'com.github.node-gradle.node' version '7.0.2'
     id 'io.github.gradle-nexus.publish-plugin' version '1.3.0' apply false
-    id 'com.diffplug.spotless' version '6.18.0'
     id 'net.ltgt.errorprone' version '3.0.1'
 }
 
@@ -71,4 +72,22 @@ javadoc {
     options.encoding = 'UTF-8'
 }
 
+node {
+    download = true
+    nodeProjectDir = file("${project.projectDir}/docs")
+}
+
+tasks.register('buildDocs') {
+    group 'Build'
+    description 'Builds the jspecify.org website.'
+    dependsOn('npm_run_build')
+    dependsOn('javadoc')
+    doLast {
+        copy {
+            from tasks.named('javadoc')
+            into "${project.projectDir}/docs/build/docs/api"
+        }
+    }
+}
+
 defaultTasks 'spotlessApply', 'build'

docs/docs/spec.md

@@ -737,7 +737,7 @@ A type is null-exclusive under every parameterization if it has a
 ## Nullness-subtype-establishing path
 
 > Note that this definition is used both by the definition of
-> [null-inclusive under every parameterization] and by the third condition in
+> [null-exclusive under every parameterization] and by the third condition in
 > the definition [nullness subtyping] itself (the "type-variable case").
 
 `A` has a nullness-subtype-establishing path to `F` if both of the following