Skip to content

Deep-compress elaborated term to save into attributes#555

Merged
nikswamy merged 1 commit intomainfrom
_mtzguido_539
Feb 10, 2026
Merged

Deep-compress elaborated term to save into attributes#555
nikswamy merged 1 commit intomainfrom
_mtzguido_539

Conversation

@tahina-pro
Copy link
Member

This PR is @mtzguido 's suggestion from #539 (comment), as an alternative to #539 .

@tahina-pro tahina-pro requested a review from nikswamy February 10, 2026 01:02
@tahina-pro
Copy link
Member Author

With this PR, project-everest/everparse#244 (more precisely https://github.com/tahina-pro/quackyducky/tree/_taramana_smt_univs_2025_pulse_555 ) manages to verify src/lowparse/LowParse.Pulse.Recursive.fst with --admit_smt_queries true, which is necessary to build EverParse binary packages on Linux and MacOS, as attested by the successful builds at https://github.com/tahina-pro/quackyducky/actions/runs/21845152774, https://github.com/tahina-pro/quackyducky/actions/runs/21838222217, https://github.com/tahina-pro/quackyducky/actions/runs/21838215149

@nikswamy nikswamy merged commit 1c00c23 into main Feb 10, 2026
2 checks passed
@tahina-pro
Copy link
Member Author

Thanks a lot Nik and Guido!

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.

2 participants