Repository navigation
chore(formal-verification): OpenJML 21.0.28 - #169
Merged
Merged
Conversation
- OPENJML_VERSION 21.0.27 -> 21.0.28, SHA-256 from the release asset digest of openjml-ubuntu-24.04-21.0.28.zip. - Verified locally with 21.0.28 (default solver z3 5.1.0): ESC 14/14 clean proofs, RAC suite 285/285. - Bundled-spec workarounds stay: 21.0.28 was built from Specs 1a91cb6, before the Atomic* fix (OpenJML/Specs#29, OpenJML/OpenJML#982, merged into dev-21). ArrayDeque.jml and the jdk/release JAVA_VERSION key are still broken too. - Invariants re-tested per the bump checklist: RAC compiles them now but throws NoSuchFieldError in non-static inner-class constructors (minimal reproducer in TODO.md); invariants stay omitted. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018mLGtytvtJU7aNshBpnrB5
bernardladenthin
had a problem deploying
to
maven-central
October 6, 2026 22:18 — with 
GitHub Actions
Failure
GitHub Actions
Failure
bernardladenthin
had a problem deploying
to
startgate
October 6, 2026 22:18 — with
GitHub Actions
Error
GitHub Actions
Error
bernardladenthin
had a problem deploying
to
maven-central
October 6, 2026 22:18 — with
GitHub Actions
Failure
GitHub Actions
Failure
|
This is a well-executed tool version bump with thorough testing and comprehensive documentation. All changes are appropriate and safe. What is Good:
Technical Soundness:
No issues found:
Ready to merge once CI confirms formal verification passes (ESC 14/14, RAC 285/285). |
|
5 of 6 tasks
This branch had an error being deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
openjml-ubuntu-24.04-21.0.28.zip. 21.0.28 switches the default solver to z3 5.1.0; ESC and RAC results are unchanged.setup-openjmlstay. 21.0.28 was built from Specs1a91cb6, which predates theAtomic*fix (Fix RAC IllegalAccessError in Atomic{Long,Integer,Boolean} constructor specs OpenJML/Specs#29 and Add testspecs cases for Atomic{Long,Integer,Boolean} construction OpenJML/OpenJML#982, both merged intodev-21on 2026-10-05).ArrayDeque.jmland the missingJAVA_VERSIONkey are still broken in 21.0.28 as well.NoSuchFieldErrorin constructors of non-static inner classes. There is a minimal reproducer in TODO.md, and the invariants stay omitted.Test plan
JAVA_VERSIONpatched): ESC 14/14 clean proofs, RAC suite 285/285check-shared-files,check-run-scripts,check-release-gate, Spotless cleanRelated issues / PRs
Refs OpenJML/Specs#29, OpenJML/OpenJML#982, OpenJML/OpenJML#806
Checklist
CONTRIBUTING.mdandCODE_OF_CONDUCT.mdSECURITY.md)🤖 Generated with Claude Code
https://claude.ai/code/session_018mLGtytvtJU7aNshBpnrB5