Skip to content

EXPERIMENT: emit part structure as a string - #690

Draft
robsimmons wants to merge 5 commits into
mainfrom
serialize-part-structure
Draft

EXPERIMENT: emit part structure as a string#690
robsimmons wants to merge 5 commits into
mainfrom
serialize-part-structure

Conversation

@robsimmons

Copy link
Copy Markdown
Collaborator

No description provided.

@robsimmons

Copy link
Copy Markdown
Collaborator Author

!bench

@leanprover-radar

leanprover-radar commented Dec 28, 2025

Copy link
Copy Markdown

Benchmark results for 1f9f081 against 14ee777 are in! @robsimmons

Medium changes (3✅)
  • refman-no-opt-args/build/.total//generated C: -3MiB (-1.5%)
  • refman-o0/build/.total//generated C: -3MiB (-1.5%)
  • refman/build/.total//generated C: -3MiB (-1.5%)
@robsimmons

Copy link
Copy Markdown
Collaborator Author

!bench

@leanprover-radar

leanprover-radar commented Dec 28, 2025

Copy link
Copy Markdown

Benchmark results for 39b8837 against 14ee777 are in! @robsimmons

No significant changes detected.

@robsimmons
robsimmons force-pushed the serialize-part-structure branch from 6d6319a to 5465638 Compare December 28, 2025 04:19
@robsimmons robsimmons changed the title refactor: emit part structure as a string May 1, 2026
@robsimmons robsimmons changed the title Experiment: emit part structure as a string May 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

2 participants