Repository navigation

Improve AutoCorrode automation and timing diagnostics - #281

Merged

hanno-becker merged 46 commits into

mainfrom

timing-and-autolocality-port

Oct 6, 2026

Merged

Improve AutoCorrode automation and timing diagnostics#281
hanno-becker merged 46 commits into
mainfrom
timing-and-autolocality-port

Commits on Sep 24, 2026
- Honor explicit Isabelle heap directory overrides
  hanno-becker
  committed
  a629bf6
- Crush: Skip inactive callback-free timers
  hanno-becker
  committed
  bc81b29
- Crush: Reuse the ucincl discharge solver
  hanno-becker
  committed
  a1185c4
- Crush: Prepare the mandatory ucincl solver once
  hanno-becker
  committed
  1d995cc
- Crush: Avoid disabled REPEAT_SMART diagnostics
  hanno-becker
  committed
  70f6e94
- Crush: Reuse premise lists in REPEAT_SMART
  hanno-becker
  committed
  ee04463
- Misc: Add generic set, list, and multiset facts
  
  Lawrence Paulson
  authored and
  hanno-becker
  committed
  9f6bf0a
- AutoCorrode: Derive locality rewrites on demand
  hanno-becker
  committed
  a7a5b4a
- AutoCorrode: Match helper certificates by application
  hanno-becker
  committed
  ff43a9b
- AutoCorrode: Infer records for explicit locality facts
  hanno-becker
  committed
  489a53a
- AutoCorrode: Add fine-grained PIDE timing
  hanno-becker
  committed
  96b2235
- Crush: Publish fine-grained timing profiles
  hanno-becker
  committed
  76b7fba
- I/P: Inspect fine-grained PIDE timings
  hanno-becker
  committed
  43a13e2
- Scala plugins: Normalize Isabelle installation paths
  hanno-becker
  committed
  cf58765
- Fine-Grained Timing: Build source hierarchy asynchronously
  hanno-becker
  committed
  3a7cc1a
- AutoCorrode: Separate timing session from panel component
  hanno-becker
  committed
  76db658
- Crush: Try crule branches before premise unfolding
  hanno-becker
  committed
  d88b054
- AutoLocality: Don't unfold baked-in logical-core constants
  
  Lawrence Paulson
  authored and
  hanno-becker
  committed
  cdb8459
- Balance meta-comment (*<*)/(*>*) markers
  
  Lawrence Paulson
  authored and
  hanno-becker
  committed
  d34f479
- Fine-Grained Timing: Apply the threshold to every sink
  hanno-becker
  committed
  c88b679
- Fine-Grained Timing: Report failed methods as failed
  hanno-becker
  committed
  77bfc60
- Fine-Grained Timing: Collect complete timing reports
  hanno-becker
  committed
  0545c9a
- Fine-Grained Timing: Track subgoal blocks in proof scopes
  hanno-becker
  committed
  4e51477
- I/R: Don't cap zstd decompression of PIDE exports
  hanno-becker
  committed
  a3e3cc5
- AutoCorrode: Avoid duplicate Isabelle component registrations
  hanno-becker
  committed
  b4f1f13
Commits on Sep 25, 2026
- AutoLocality: Merge sibling dispatchers by dispatch key
  hanno-becker
  committed
  72f6719
Commits on Sep 28, 2026
- Fine-Grained Timing: Decode entries from mixed reports
  hanno-becker
  committed
  d42d448
Commits on Oct 5, 2026
- AutoCorrode: Use typed artifacts for record generation
  hanno-becker
  committed
  ee23857
- Fine-Grained Timing: Report exceptions from profiled pulls
  hanno-becker
  committed
  445a2a7
- AutoLocality: Unfold helpers after ambiguous lookup
  hanno-becker
  committed
  4e3cd7b
- Fine-Grained Timing: Preserve raised invocation outcomes
  hanno-becker
  committed
  14fb9cf
- Fine-Grained Timing: Aggregate Calls by invocation timing
  hanno-becker
  committed
  ffd1925
- AutoCorrode: Ignore stale component registrations
  hanno-becker
  committed
  f63d8b3
- AutoLocality: Decline ambiguous simproc lookups
  hanno-becker
  committed
  f219688
- Misc: Add `quiet_context` to open a named context silently
  hanno-becker
  committed
  069fa43
- Make AutoCorrode weakest preconditions resource-exact
  
  ike-mulder-aws
  authored and
  hanno-becker
  committed
  68379cb
- Crush: Add a guarded order branch
  hanno-becker
  committed
  9dc4b70
- Make precise pure assertions canonical
  
  ike-mulder-aws
  authored and
  hanno-becker
  committed
  1ce1952
- Crush: Commit to the first closure proof when inserting ⊤
  hanno-becker
  committed
  164a384
- Crush: Fold word bounds into the order branch
  hanno-becker
  committed
  3ed77d4
- Crush: Strip unused sorts before clarsimp branches
  hanno-becker
  committed
  c8f84a5
- Crush: Don't rerun a step that a big step has just failed on
  hanno-becker
  committed
  6713fbf
- Crush: Skip a step on a goal whose conclusion is a pending guard
  hanno-becker
  committed
  2f8faec
- Crush: Skip the clarsimp fallback that repeats a filtered call
  hanno-becker
  committed
  06d9370
- Crush: Don't hide every premise when the conclusion has no constants
  hanno-becker
  committed
  68d6fe0
Commits on Oct 6, 2026
- AutoLocality: Derive disjoint projections linearly
  hanno-becker
  committed
  879b415

Commits

Commits on Sep 24, 2026

Commits on Sep 25, 2026

Commits on Sep 28, 2026

Commits on Oct 5, 2026

Commits on Oct 6, 2026