Post-submission improvements (base for post-POPL'26 work)#3
Open
bollu wants to merge 4 commits into
Open
Conversation
…ie-breaks) Points the leanwuzla submodule at the min-max-two-tuples branch tip that threads two independent tie-break Bools (zpm/zmp) per (operator, format) through fp.min/ fp.max (fp-lean-private f7a5e86 provides the two-arg smtMin/smtMax). Closes the completeness gap where a single shared tie-break excluded the same-sign-for-both- orderings models of min/max on differing-signed zeros. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…gures
Paper figures must not reveal the tool identity. Renames the display labels
(bench.tool2label) used in the cactus legend + endpoint annotations, the LaTeX
macro suffixes (plot._texname override: Ours / OursNokernel / OursNancanon), and
the per-tool tex section comments -- so no "FP-Lean"/"fplean" string appears in
cactus.{png,pdf,tex}. The internal ToolName ids ("fplean", ...) are unchanged
(they still key commands, run dirs, and the manifest); only the figure-facing
strings are anonymized.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… into fp) Points at the fp-branch tip after PR #8 merged; content-identical to the prior 6a67c0b pin, now on the canonical integration branch. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Post-submission improvement: incorporates the parser-error-fixes work (n-ary/chained fp.lt/fp.leq/fp.gt/fp.geq desugaring), resolving the 4 schanda kernel-solver errors. Branches off the POPL'26 submission snapshot (341cc3c). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
1 participant
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.
Branch for post-submission improvements, based off the POPL'26 submission snapshot
(tag
popl26-submission-9-july-1800, commit341cc3c). Bringsmainup to thesubmission state and adds the first parser fix.
Included
smtlib-rand+instcombine-small, per-(operator,format) two-tuple min/max tie-breaks, anonymized "ours"/"ours (nokernel)" plot labels.784c984): n-aryfp.lt/fp.leq/fp.gt/fp.geq((fp.lt a b c) = (and (fp.lt a b) (fp.lt b c))) — resolves the 4 schanda kernel-solver errors, all matching bitwuzla.Companion
post-submission-improvementbranches exist onfp-lean-privateandleanwuzla-privatefor the ongoing work on the remaining kernel-solver failure buckets (unsupported-BitVec-fragment audit,to_fpwiring after fp-lean PR #119, maxSteps).🤖 Generated with Claude Code