Skip to content

32-bit recoder for trace files#1966

Open
digama0 wants to merge 1 commit into
developfrom
recode32
Open

32-bit recoder for trace files#1966
digama0 wants to merge 1 commit into
developfrom
recode32

Conversation

@digama0
Copy link
Copy Markdown
Contributor

@digama0 digama0 commented May 12, 2026

Summary

  • Add a streaming recode32 binary that converts PolyML's 64-bit .tr heap dumps to a 32-bit narrow format, halving the size of pointers and headers
  • The 32-bit variant is identified by an 8-byte magic TR32\0\0\0\xFF; the final byte cannot collide with a valid 64-bit flags byte (which is always 00–03)
  • ProofTraceParser gains a Heap32 variant that decodes the narrow format in-place; all sh* accessors dispatch on the variant
  • Tracing.export pipes through recode32 when the (default-on) recode_32bit flag is set
  • The recoder raises Fail rather than silently truncating when a value does not fit in 32 bits
  • recode32 is built automatically by Holmake (via POLYC) into $HOLDIR/bin/recode32 when --trknl is enabled, since src/tracing/yes is in the kernel sequence for that build

Test plan

  • Build with --trknl and confirm $HOLDIR/bin/recode32 is produced
  • Verify .tr.gz files are roughly half the size of the 64-bit format
  • Confirm ProofTraceParser.parse decodes the new files correctly via ProofTraceReplay

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