Skip to content

fix(ci): stage JPF annotation jars via dependency:copy-dependencies - #159

Merged
bernardladenthin merged 1 commit into
mainfrom
claude/formal-verification
Sep 13, 2026
Merged

fix(ci): stage JPF annotation jars via dependency:copy-dependencies#159
bernardladenthin merged 1 commit into
mainfrom
claude/formal-verification

Conversation

@bernardladenthin

Copy link
Copy Markdown
Owner

Summary

Follow-up to #158. On the first hosted-runner dispatch, the jpf-interleavings job failed in its first step (before JPF ran): parsing the dependency:build-classpath output string with tr/while/case worked locally but not on the CI shell, so the annotation jars were never staged and the test -f guard aborted the step.

  • Replace the classpath-string parsing with mvn dependency:copy-dependencies -DincludeScope=compile -DoutputDirectory=target/anno, then copy the three annotation jars (checker-qual / jspecify / error-prone) by unambiguous glob to the stable unversioned names the .jpf classpath expects.
  • Robust across platforms and dependency-version bumps; drops -q and lists the staged jars for diagnosability.

The rest of the JPF chain (jpf-core build with the AtomicLong model patch, --release 8 harness compile, RunJPF) is unchanged. ESC and RAC (the always-on jobs) are unaffected.

Test plan

  • Re-verified locally in Docker (JDK 11) with the exact repo harness/config and the copy-dependencies-staged lib: JPF "no errors detected", ~14,049 states
  • dependency:copy-dependencies confirmed to include the optional annotation jars

Checklist

  • Conventional Commits
  • No security-sensitive changes

🤖 Generated with Claude Code

https://claude.ai/code/session_01TU5B8DDtDwKSS6ohSfoz2Y

The jpf-interleavings job's first step failed on the hosted runner while parsing the
build-classpath string with tr/while/case (worked locally, not on the CI shell), so JPF never
ran. Replace that with `mvn dependency:copy-dependencies -DincludeScope=compile` into a directory
and copy the three annotation jars (checker-qual/jspecify/error-prone) by unambiguous glob to the
stable unversioned names the .jpf classpath expects. Robust across platforms and version bumps;
also drops -q and lists the staged jars for diagnosability. Re-verified locally in Docker: JPF
"no errors detected", ~14k states.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TU5B8DDtDwKSS6ohSfoz2Y
@sonarqubecloud

Copy link
Copy Markdown

@bernardladenthin
bernardladenthin merged commit 795f3c3 into main Sep 13, 2026
17 of 21 checks passed
@bernardladenthin
bernardladenthin deleted the claude/formal-verification branch September 13, 2026 10:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant