Repository navigation
Leftover unchecked and deprecation lint fixes from the this-escape workstream (stacked on #4004) - #4005
Closed
wadoon wants to merge 10 commits into
Closed
Leftover unchecked and deprecation lint fixes from the this-escape workstream (stacked on #4004)#4005wadoon wants to merge 10 commits into
wadoon wants to merge 10 commits into
Conversation
wadoon
changed the title
Enable all javac lint warnings (-Xlint:all) in the shared JavaCompile configuration. The compiler tags each warning with its category ([deprecation], [unchecked], [rawtypes], ...), which allows grouping and tackling them category by category. Add scripts/collect-warnings.py that runs a full testClasses build, parses the compiler output and writes build/warnings/warnings.md with the warnings grouped by category, then by module and source file, plus a summary table. Co-Authored-By: OpenCode (KIT Medium)
Snapshot of the warnings reported by javac -Xlint:all on a clean testClasses build (619 warnings, 13 categories, 15 modules), generated by scripts/collect-warnings.py and grouped by category, module and file. The script now reports source files relative to the repository root so the generated inventory is machine independent. Co-Authored-By: OpenCode (KIT Medium)
Documents the workstream partition (disjoint file ownership), per-category strategy and the binding ground rules for the -Xlint:all cleanup. Co-Authored-By: OpenCode (KIT Medium)
Suppress deliberate uses of deprecated APIs (ImmutableArray term/label containers, Location#getFileURI, Proof#add, old Proof constructor) in key.core test sources with @SuppressWarnings and a rationale comment. No test logic or assertions are changed. Co-Authored-By: OpenCode (KIT Medium)
Suppress deliberate uses of deprecated APIs in key.util test sources: StringsTest keeps testing the deprecated Strings helpers, IOUtilTest constructs URLs via the deprecated URL(String) constructor. All changes are @SuppressWarnings annotations with a rationale comment; no test logic is changed. Co-Authored-By: OpenCode (KIT Medium)
Regenerated from a clean full rebuild (--rerun-tasks): 224 warnings remaining (baseline: 619). The incremental baseline under-reported warnings that a full recompile reveals (see workstream reports); every fix of the six workstreams is integrated, so this snapshot reflects the honest residual in files outside the original workstream scope. Co-Authored-By: OpenCode (KIT Medium)
javac limits printed warnings to 100 per compilation unit by default, which truncated the warning inventory (a single file can emit far more, e.g. TestApplyTaclet). With -Xmaxwarns 100000 the collect-warnings.py inventory is no longer silently capped. Co-Authored-By: OpenCode (KIT Medium)
With -Xmaxwarns 100000 the inventory is no longer capped at 100 warnings per file: 1809 warnings total (deprecation 834, serial 351, this-escape 310, unchecked 141, rawtypes 79, auxiliaryclass 48, ...). This supersedes the cap-truncated snapshot (224) and the original baseline (619). Co-Authored-By: OpenCode (KIT Medium)
Suppress the inherited-getter constructor escapes in the well-definedness contract classes and the unchecked goal-chooser-builder overrides reported against every concrete profile subclass. Co-Authored-By: OpenCode (KIT Medium)
Suppress the intentional handler-wiring escape; keep the deprecated ImmutableArray parameter of translate() because callers pass term.subs() which still returns ImmutableArray (migrating would break those call sites). Co-Authored-By: OpenCode (KIT Medium)
wadoon
force-pushed
the
weigl/cleanwarnings
branch
from
October 25, 2026 00:57
ca48198 to
69d92cc
Compare
wadoon
force-pushed
the
weigl/cw-this-escape
branch
from
October 25, 2026 00:57
b5d9c72 to
56ddb4c
Compare
wadoon
force-pushed
the
weigl/cleanwarnings
branch
3 times, most recently
from
October 25, 2026 01:04
69d92cc to
34aee9a
Compare
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
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.
What
This branch originally fixed the javac
[this-escape]lint warnings(constructor publishes
thisbefore completion) in 12 modules. Per thecampaign cleanup decision, all this-escape fixes were REMOVED from
history; the serial/this-escape workstream is gone.
@SuppressWarnings("unchecked")inkey.core.wd(WdProfile),@SuppressWarnings("deprecation")inkeyext.isabelletranslation(
IsabelleMasterHandler).No this-escape/serial suppression,
serialVersionUIDortransientremains in the branch range. 2 commits total.
Verification
History pattern-scan over the rewritten range is clean (
this-escape,serial,@Serial,serialVersionUID,transient); the final treediff contains only removals of campaign content plus the two kept
warning fixes above.
Draft — part of the warning-cleanup stack on
weigl/cleanwarnings(→ PR #4001). No test-assertion, logic or signature changes.
Commits carry
Co-Authored-By: OpenCode (KIT Medium).Linear-stack head:
56ddb4c800(re-based on the rebuilt #4004).