Skip to content

OpenJML 21.0.29 (drops the AtomicLong spec workaround) and the shared Claude/Gradle pins - #187

Merged
bernardladenthin merged 2 commits into
mainfrom
claude/determined-feynman-97mrit
Oct 20, 2026
Merged

bernardladenthin merged 2 commits into
mainfrom
claude/determined-feynman-97mrit

Conversation

@bernardladenthin

@bernardladenthin bernardladenthin commented Oct 20, 2026 •

Copy link
Copy Markdown
Owner

Summary

Part of the 2026-10-20 cross-repo dependency sweep (one PR each in BAF, java-llama.cpp, srcmorph, BroomCabinet and workspace). All Maven dependencies and plugins here were already current.

  • formal-verification.yml: OpenJML 21.0.28 → 21.0.29, released today. The SHA-256 is the release asset's digest from the release page and matches the downloaded zip.
  • setup-openjml (fixups v2, new cache key):
  • Class invariants, re-tried as the bump checklist asks:
    • The minimal reproducer in TODO.md now runs clean.
    • The four candidate invariants still break RAC on this class: NoSuchMethodError on StreamBuffer$SBOutputStream.JML$INV$$<n>(), 106 errors.
    • They stay out; CLAUDE.md, TODO.md and the .jml note record the new symptom.
  • anthropics/claude-code-action v1.0.252 → v1.0.255 (same commit in all four repos), Gradle 9.8.2 in verify-signing-key-gradle, shared-files.sha256 rewritten (incl. the stale scorecard.yml / osv-scanner.yml hashes Dependabot left).

Test plan

  • Affected unit / integration tests pass locally, with 21.0.29 run the way the workflow runs it: ESC 14/14 clean proofs (1.7 s), RAC compile plus the full suite against the RAC classes 285/285 with the bundled AtomicLong.jml
  • Workflows parse as YAML; check-run-scripts.py is clean
  • CI is green on this branch (the formal-verification workflow runs on this PR)
  • Docs / CHANGELOG updated where applicable

Related issues / PRs

Refs OpenJML/OpenJML#1012 (invariant defect, new symptom on 21.0.29), OpenJML/Specs#29. Sibling PRs of the same sweep in the other repos.

Checklist

  • I have read CONTRIBUTING.md and CODE_OF_CONDUCT.md
  • My commits follow Conventional Commits
  • No security-sensitive changes (if there are, I have notified the maintainer privately per SECURITY.md)

🤖 Generated with Claude Code

https://claude.ai/code/session_011CYhRUUCqwrHXPuEhS9W4M

- formal-verification.yml: OpenJML 21.0.28 -> 21.0.29 (SHA-256 from the
  release asset digest). Measured locally: ESC 14/14 (1.7 s, SMT commands
  are pipelined now), RAC 285/285.
- setup-openjml (fixups v2, new cache key): the AtomicLong.jml rm is gone,
  the upstream fix (OpenJML/Specs#29) shipped in 21.0.29 and the suite
  passes against the bundled file; ArrayDeque.jml is still broken and still
  deleted; the JAVA_VERSION repair is a no-op on 21.0.29, kept as a guard.
- Class invariants re-tried as the bump checklist asks: the minimal
  reproducer runs clean on 21.0.29, but the four candidate invariants still
  break RAC on this class (NoSuchMethodError on SBOutputStream.JML$INV$$<n>(),
  106 errors, then a hang). They stay out; CLAUDE.md, TODO.md and the .jml
  note record the new symptom.
- anthropics/claude-code-action v1.0.252 -> v1.0.255 (same commit in all four
  repositories), Gradle 9.8.1 -> 9.8.2 in the shared
  verify-signing-key-gradle job; shared-files.sha256 rewritten, including
  the scorecard.yml / osv-scanner.yml hashes Dependabot had left stale.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011CYhRUUCqwrHXPuEhS9W4M
The stall seen while re-trying the class invariants is most likely
OpenJML/OpenJML#1050 (a stack trace per call for skipped specification
clauses; fixed on dev-21, not yet in 21.0.29), not part of the invariant
defect, so the notes record only the NoSuchMethodError and its count.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011CYhRUUCqwrHXPuEhS9W4M
@bernardladenthin
bernardladenthin merged commit 673a5a9 into main Oct 20, 2026
9 of 12 checks passed
@bernardladenthin
bernardladenthin deleted the claude/determined-feynman-97mrit branch October 20, 2026 22:54
@sonarqubecloud

Copy link
Copy Markdown

This branch had an error being deployed

1 failed deployment
maven-central — 90e730af Deployed Oct 20, 2026 by bernardladenthin via Verify GPG signing key (no secrets printed) #337
startgate — 90e730af Deployed Oct 20, 2026 by bernardladenthin via Start gate (abort window) #337
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.

2 participants