Use an EISOP CF build

.github/workflows/build.yml

@@ -19,6 +19,11 @@ jobs:
         with:
           repository: jspecify/jspecify
           path: jspecify
+      - name: Check out eisop/checker-framework
+        uses: actions/checkout@v4
+        with:
+          repository: eisop/checker-framework
+          path: checker-framework
       - name: Set up Java
         uses: actions/setup-java@v4
         with:
@@ -27,18 +32,19 @@ jobs:
       - name: Set up Gradle
         uses: gradle/gradle-build-action@v3
       - name: Build and Test
-        run: ./gradlew build conformanceTests demoTest --include-build ../jspecify
+        run: ./gradlew build conformanceTests demoTest --include-build ../jspecify --include-build ../checker-framework
         env:
           SHALLOW: 1
-      - name: Check out jspecify/samples-google-prototype
+          JSPECIFY_CONFORMANCE_TEST_MODE: details
+      - name: Check out jspecify/samples-google-prototype-eisop
         if: always()
         run: |
-          git fetch --depth=1 origin samples-google-prototype
-          git checkout samples-google-prototype
+          git fetch --depth=1 origin samples-google-prototype-eisop
+          git checkout samples-google-prototype-eisop
         working-directory: jspecify
       - name: Run Samples Tests
         if: always()
-        run: ./gradlew jspecifySamplesTest --include-build ../jspecify
+        run: ./gradlew jspecifySamplesTest --include-build ../jspecify --include-build ../checker-framework
 
   publish-snapshot:
     name: Publish Conformance Test Framework Snapshot

README.md

@@ -17,21 +17,21 @@ But that's its *only* job. Notably, it is:
 
 ## Relationship to Checker Framework and EISOP
 
-The [EISOP project](https://eisop.github.io/) maintains a fork of [Checker Framework](https://checkerframework.org/), and JSpecify conformance is one of its primary goals.
+The [EISOP project](https://eisop.github.io/) maintains a fork of the [Checker Framework](https://checkerframework.org/), and JSpecify conformance is one of its goals.
 
-This tool happens to be built on top of another fork of these ([here](https://github.com/jspecify/checker-framework)). However, please view this relationship as **implementation detail** only. Building a reference checker from scratch would simply have been too difficult, so we needed to base it on some existing tool. The choice of which tool was made purely for expediency and is **subject to change**.
+This tool is built on top of the [EISOP Checker Framework](https://github.com/eisop/checker-framework). However, please view this relationship as **implementation detail** only. Building a reference checker from scratch would simply have been too difficult, so we needed to base it on some existing tool. The choice of which tool was made purely for expediency and is **subject to change**.
 
 ## Usage
 
-Building and running this tool requires building code from several other repositories, but these instructions will take care of that automatically.
+Building and running this tool depends on code from several other repositories, but these instructions will take care of that automatically.
 
 These instructions might require workarounds or fail outright. Please file an issue if you have any trouble!
 
 ### Prework
 
 Ideally set `JAVA_HOME` to a JDK 11 or JDK 17 installation.
 
-Make sure you have Apache Maven installed and in your PATH, or the Gradle build will fail:
+Make sure you have Apache Maven installed and in your PATH, or the `demo` script will fail:
 
 ```sh
 mvn

build.gradle

@@ -9,12 +9,25 @@ plugins {
     id 'com.diffplug.spotless' version '6.25.0'
     id 'io.github.gradle-nexus.publish-plugin' version '1.3.0'
     id 'net.ltgt.errorprone' version '3.0.1'
+    // To show task list as a tree, run: ./gradlew <taskname> taskTree
+    id 'com.dorongold.task-tree' version '4.0.0'
 }
 
 // Nexus Publish plugin requires a group/version at the root project.
 group = 'org.jspecify.reference'
 version = '0.0.0-SNAPSHOT'
 
+sourceSets {
+    main {
+        resources {
+            // Minimized jspecify/jdk
+            srcDirs += [
+                "${buildDir}/generated/resources"
+            ]
+        }
+    }
+}
+
 repositories {
     mavenLocal()
     maven {
@@ -35,10 +48,14 @@ nexusPublishing {
 }
 
 ext {
-    checkerFramework = gradle.includedBuild("checker-framework")
+    // null if not included with `--include-build path/to/checker-framework`
+    checkerFramework = gradle.includedBuilds.find { it.name == 'checker-framework' }
 
     // null if not included with `--include-build path/to/jspecify`
     jspecify = gradle.includedBuilds.find { it.name == 'jspecify' }
+
+    // Location of the jspecify/jdk clone, relative to this directory
+    jspecifyJdkHome = '../jdk'
 }
 
 configurations {
@@ -61,8 +78,10 @@ java {
 dependencies {
     implementation libs.checkerFramework.checker
     implementation libs.checkerFramework.checker.qual
-    implementation libs.checkerFramework.framework
-    implementation libs.checkerFramework.javacutil
+    // Eventually, we would want to only depend on `framework` and
+    // `javacutil` artifacts instead of the entire `checker`.
+    // implementation libs.checkerFramework.framework
+    // implementation libs.checkerFramework.javacutil
 
     implementation libs.jspecify
 
@@ -78,8 +97,11 @@ dependencies {
     errorprone libs.errorProne.core
 }
 
-// Assemble checker-framework when assembling the reference checker.
-assemble.dependsOn(checkerFramework.task(":assemble"))
+// If built with `--include-build path/to/checker-framework` then
+// assemble checker-framework when assembling the reference checker.
+if (checkerFramework != null) {
+    compileJava.dependsOn(checkerFramework.task(":checker:assembleForJavac"))
+}
 
 // If built with `--include-build path/to/jspecify` then
 // assemble jspecify when assembling the reference checker.
@@ -111,6 +133,54 @@ tasks.withType(JavaCompile).configureEach {
             .collect { "--add-exports=jdk.compiler/com.sun.tools.javac.$it=ALL-UNNAMED" })
 }
 
+tasks.register('includeJSpecifyJDK')  {
+    group = 'Build'
+    dependsOn 'compileJava'
+
+    def srcDir = "${jspecifyJdkHome}/src"
+    // This directory needs to be stored at the top-level of the resulting .jar file.
+    // org.checkerframework.framework.stub.AnnotationFileElementTypes will then load
+    // the JDK classes from here instead of from checker.jar.
+    def dstDir = "${buildDir}/generated/resources/annotated-jdk/src/"
+
+    inputs.dir file(srcDir)
+    outputs.dir file(dstDir)
+
+    doLast {
+        FileTree srcTree = fileTree(dir: srcDir)
+        NavigableSet<String> specFiles = new TreeSet<>();
+        srcTree.visit { FileVisitDetails fvd ->
+            if (!fvd.file.isDirectory() && fvd.file.name.matches('.*\\.java')) {
+                fvd.getFile().readLines().any { line ->
+                    if (line.contains('org.jspecify')) {
+                        specFiles.add(fvd.file.absolutePath)
+                        return true;
+                    }
+                }
+            }
+        }
+        String absoluteSrcDir = file(srcDir).absolutePath
+        int srcPrefixSize = absoluteSrcDir.size()
+        copy {
+            from(srcDir)
+            into(dstDir)
+            for (String specFile : specFiles) {
+                include specFile.substring(srcPrefixSize)
+            }
+        }
+        javaexec {
+            classpath = sourceSets.main.runtimeClasspath
+            standardOutput = System.out
+            errorOutput = System.err
+
+            mainClass = 'org.checkerframework.framework.stub.JavaStubifier'
+            args dstDir
+        }
+    }
+}
+
+processResources.dependsOn(includeJSpecifyJDK)
+
 tasks.withType(Test).configureEach {
     if (!JavaVersion.current().java9Compatible) {
         jvmArgs "-Xbootclasspath/p:${configurations.errorproneJavac.asPath}"
@@ -138,8 +208,10 @@ tasks.withType(Test).configureEach {
 
 test {
     include '**/NullSpecTest$Minimal.class'
-
     inputs.files("${rootDir}/tests/minimal")
+
+    include '**/NullSpecTest$Regression.class'
+    inputs.files("${rootDir}/tests/regression")
 }
 
 tasks.register('jspecifySamplesTest', Test) {
@@ -217,24 +289,27 @@ tasks.register('demoTest', Exec)  {
  See https://github.com/jspecify/jspecify-reference-checker/issues/81
  */
 
-def cfQualJar =
-        checkerFramework.projectDir.toPath()
-        .resolve("checker-qual/build/libs/checker-qual-${libs.versions.checkerFramework.get()}.jar")
-
-if (!cfQualJar.toFile().exists()) {
-    mkdir(cfQualJar.parent)
-    exec {
-        executable 'jar'
-        args = [
-            'cf',
-            cfQualJar,
-            buildFile.path // Use this build script file!
-        ]
+if (checkerFramework != null) {
+    def cfQualJar =
+            checkerFramework.projectDir.toPath()
+            .resolve("checker-qual/build/libs/checker-qual-${libs.versions.checkerFramework.get()}.jar")
+
+    if (!cfQualJar.toFile().exists()) {
+        mkdir(cfQualJar.parent)
+        exec {
+            executable 'jar'
+            args = [
+                'cf',
+                cfQualJar,
+                buildFile.path // Use this build script file!
+            ]
+        }
     }
 }
 
 spotless {
     java {
+        target '**/*.java'
         googleJavaFormat()
         formatAnnotations()
     }
@@ -260,3 +335,47 @@ eclipse.classpath {
         }
     }
 }
+
+publishing {
+    publications {
+        jspecifyReferenceChecker(MavenPublication) {
+            pom {
+                groupId = 'org.jspecify.reference'
+                artifactId = 'checker'
+                version = project.version
+                name = 'JSpecify Reference Checker'
+                description = 'The JSpecify Reference Checker'
+                url = 'http://jspecify.org/'
+                from components.java
+                licenses {
+                    license {
+                        name = 'The Apache License, Version 2.0'
+                        url = 'http://www.apache.org/licenses/LICENSE-2.0.txt'
+                    }
+                }
+                scm {
+                    connection = 'scm:git:[email protected]:jspecify/jspecify-reference-checker.git'
+                    developerConnection = 'scm:git:[email protected]:jspecify/jspecify-reference-checker.git'
+                    url = 'https://github.com/jspecify/jspecify-reference-checker'
+                }
+                developers {
+                    developer {
+                        id = 'cpovirk'
+                        name = 'Chris Povirk'
+                        email = '[email protected]'
+                    }
+                    developer {
+                        id = 'netdpb'
+                        name = 'David P. Baker'
+                        email = '[email protected]'
+                    }
+                    developer {
+                        id = 'wmdietl'
+                        name = 'Werner M. Dietl'
+                        email = '[email protected]'
+                    }
+                }
+            }
+        }
+    }
+}

demo

@@ -15,6 +15,20 @@ if [ ! -e "${jspecify}" ]; then
       -DoutputDirectory="$(dirname "${jspecify}")"
   fi
 fi
+
+checkerFrameworkDir="${dir}/../checker-framework/"
+checkerFrameworkJar="${checkerFrameworkDir}/checker/dist/checker.jar"
+if [ ! -e "${checkerFrameworkJar}" ]; then
+  cfVersion="3.42.0-eisop4"
+  checkerFrameworkJar="${dir}/build/checker-${cfVersion}-all.jar"
+  if [ ! -e "${checkerFrameworkJar}" ]; then
+    echo "Downloading $(basename "${checkerFrameworkJar}") from Maven central"
+    mvn -q org.apache.maven.plugins:maven-dependency-plugin:3.7.1:copy \
+      -Dartifact="io.github.eisop:checker:${cfVersion}:jar:all" \
+      -DoutputDirectory="$(dirname "${checkerFrameworkJar}")"
+  fi
+fi
+
 jspecify_reference_checker="${dir}/build/libs/jspecify-reference-checker-0.0.0-SNAPSHOT.jar"
 if [ ! -e "${jspecify_reference_checker}" ]; then
   echo "Assembling jspecify-reference-checker"
@@ -25,9 +39,11 @@ ourclasspath="${jspecify}:${jspecify_reference_checker}"
 
 export CLASSPATH="${ourclasspath}:$CLASSPATH"
 
-$dir/../checker-framework/checker/bin/javac \
+java -jar "${checkerFrameworkJar}" \
   -processorpath "${ourclasspath}" \
   -processor com.google.jspecify.nullness.NullSpecChecker \
+  -checkerQualJar "${checkerFrameworkJar}" \
+  -checkerUtilJar "${checkerFrameworkJar}" \
   -AcheckImpl \
   -AassumePure \
   -AsuppressWarnings=contracts.conditional.postcondition.false.methodref,contracts.conditional.postcondition.false.override,contracts.conditional.postcondition.true.methodref,contracts.conditional.postcondition.true.override,purity.methodref,purity.overriding,type.anno.before.decl.anno,type.anno.before.modifier \

docs/development.md

@@ -1,14 +1,14 @@
 # Development
 
-## Codevelopment with Checker Framework fork
+## Codevelopment with the EISOP Checker Framework
 
-This project depends on
-an [unreleased fork of the Checker Framework][jspecify-checker-framework].
-(The [main-eisop branch] represents ongoing work to depend on a released version
-of the [EISOP] fork instead.)
+This project depends on the [EISOP Checker Framework][EISOP].
+
+To codevelop changes with the EISOP Checker Framework, clone it into the
+sibling directory `../checker-framwork` and pass
+`--include-build path/to/checker-framework` to Gradle when building
+this project.
 
-Because of that dependency, this build clones that unreleased fork into the
-sibling directory `../checker-framwork`.
 _That_ build then clones some other projects into other sibling directories. It
 expects `../jdk` to contain an annotated JDK, so our build
 clones [JSpecify's][jspecify-jdk] there.
@@ -29,7 +29,7 @@ clone the repo (or your fork) somewhere, and pass
 `--include-build path/to/jspecify` to Gradle when building. The local clone will
 be used for both the annotations and the conformance test suite.
 
-By default the reference checker depends on version `0.3.0` of the annotations,
+By default the reference checker depends on version `1.0.0` of the annotations,
 and version `0.0.0-SNAPSHOT` of the conformance test suite.
 
 In order to depend on a different published version of either artifact, set
@@ -40,7 +40,6 @@ Gradle properties on the command line.
   of the conformance test suite.
 
 [EISOP]: https://github.com/eisop/checker-framework
-[jspecify-checker-framework]: https://github.com/jspecify/checker-framework
 [jspecify-jdk]: https://github.com/jspecify/jdk
 [jspecify-jspecify]: https://github.com/jspecify/jspecify
 [main-eisop branch]: https://github.com/jspecify/jspecify-reference-checker/tree/main-eisop

gradle.properties

@@ -1,3 +1,3 @@
-org.jspecify\:jspecify=0.3.0
+org.jspecify\:jspecify=1.0.0
 org.jspecify.conformance\:conformance-test-framework=0.0.0-SNAPSHOT
 org.jspecify.conformance\:conformance-tests=0.0.0-SNAPSHOT

gradle/wrapper/gradle-wrapper.properties

@@ -1,6 +1,6 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.6-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.10-bin.zip
 networkTimeout=10000
 validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME