Use EISOP release and include jspecify/jdk in jar

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 18 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

@@ -15,6 +15,17 @@ plugins {
 group = 'org.jspecify.reference'
 version = '0.0.0-SNAPSHOT'
 
+sourceSets {
+    main {
+        resources {
+            // Minimized jspecify/jdk
+            srcDirs += [
+                "${buildDir}/generated/resources"
+            ]
+        }
+    }
+}
+
 repositories {
     mavenLocal()
     maven {
@@ -35,10 +46,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 +76,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 +95,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) {
+    assemble.dependsOn(checkerFramework.task(":assembleForJavac"))
+}
 
 // If built with `--include-build path/to/jspecify` then
 // assemble jspecify when assembling the reference checker.
@@ -111,6 +131,54 @@ tasks.withType(JavaCompile).configureEach {
             .collect { "--add-exports=jdk.compiler/com.sun.tools.javac.$it=ALL-UNNAMED" })
 }
 
+tasks.register('includeJSpecifyJDK')  {
+    group = 'Build'
+    shouldRunAfter '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}"
@@ -219,19 +287,21 @@ 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!
+            ]
+        }
     }
 }
 

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.6.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.
@@ -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

initialize-project

@@ -19,8 +19,6 @@
 # that contains your forks. For example, [email protected]:myorg means this
 # script tries to clone the following before falling back to the JSpecify repos:
 #
-# git@github:myorg/checker-framework.git
-# git@github:myorg/jspecify.git
 # git@github:myorg/jdk.git
 
 set -eu
@@ -71,5 +69,3 @@ git_clone() {
 }
 
 git_clone jdk --depth 1 --single-branch
-
-git_clone checker-framework

settings.gradle

@@ -10,12 +10,10 @@ exec {
     executable './initialize-project'
 }
 
-includeBuild("../checker-framework")
-
 dependencyResolutionManagement {
     versionCatalogs {
         libs {
-            version("checkerFramework", "3.42.0-eisop3-SNAPSHOT")
+            version("checkerFramework", "3.42.0-eisop4")
 
             library("checkerFramework-checker", "io.github.eisop", "checker").versionRef("checkerFramework")
             library("checkerFramework-checker-qual", "io.github.eisop", "checker-qual").versionRef("checkerFramework")