Conversation
…nd (#302) * fix: handle spaces and quotes in forge filenames w.r.t. run IDs * windows-specific test scripting * add to gitignore * remote temp file * fix for windows
Merging integer/set optimization into dev branch.
* fix: join parsing, regression test, note on 2nd issue * add: semantics test * add: tests, no-op change to parser for readability
* fix: join parsing, regression test, note on 2nd issue * add: semantics test * add: tests, no-op change to parser for readability * add: revisions to get core (strings, for the moment) to sterling * fix: unsat but no core * stop sending core in place of source * Froglet Error Message Changes (#306) * update: error messages --------- Co-authored-by: shoujohnny <[email protected]>
This commit is part of the effort to add Typed Racket annotations to more of Forge's core files. However, the way that the AST was structured made using static types difficult: it wasn't always clear what the type of child nodes was, because node/expr/op contained the children field, and a relational expression might have children that are formulas, expressions, or integer expressions. Now these are broken down into different AST types.
Misc. code hardening, E2E suite in Playwright.
* Updating sterling * Forcing re-run
* Updating Sterling version * Also making semantic version updater more robust
- Site 1-2 (sigs-functional.rkt): update-bindings uses raise-forge-error
with format-tuple-set for readable atom names
- Site 3 (breaks.rkt): handle ni-only bounds (#f upper) by merging with
scope-resolved upper; defensive guard in sbound->bound
- Site 4 (pardinus.rkt): convert raw raise to raise-forge-error
- Site 4 (send-to-solver.rkt): inheritance blame via find-blame-descendant;
field bounds errors show which atoms are missing from which sigs
- Add format-tuple-set helper to shared.rkt
- Add bounds error tests and location-tracking tests
Resolves: forge-3ow, forge-5rm, forge-l7w
Co-Authored-By: Claude Opus 4.6 <[email protected]>
…sigs
The reader now reorders paragraphs into tiers before emitting the module:
0. option problem_type (file-level config; needed before var sigs)
1. sig, pred, fun (foundations)
2. inst (references sigs eagerly)
3. everything else (commands, other options — source order)
This lets users write run/check before the sigs they reference, matching
how imports (open) are already hoisted to the top of the module.
Also fix stale error-test regexes: bsl-join-right and froglet-join-right
tests now expect "is not a field" instead of the old Racket-level
"not an object" message.
Resolves: forge-1am
Co-Authored-By: Claude Opus 4.6 <[email protected]>
Wrap get-bounds in with-handlers so clear-breaker-state runs even when bounds resolution throws. Adds regression test. Co-Authored-By: Claude Opus 4.6 <[email protected]>
Propagate lang from nodeinfo in build-box-join so Froglet checks fire for box joins. Add sing? to allowed LHS types for int index args. Co-Authored-By: Claude Opus 4.6 <[email protected]>
Previously, field upper bounds silently dropped tuples referencing atoms outside the sig. Now validates and errors consistently with 'ni' bounds. Co-Authored-By: Claude Opus 4.6 <[email protected]>
Adds partition logic to send-to-solver.rkt that gives child sigs disjoint atom slices from parent surplus, eliminating cardinality constraints when children fit. Includes inspection tests, equivalence tests, inst-interaction tests, and cardinality requirement tests. Co-Authored-By: Claude Opus 4.6 <[email protected]>
Add ns-benchmark.frg to crypto examples: same NS scenario with three bounding strategies (exact, nonexact keys, nonexact all) for regression testing the bounds partition optimization. Tighten comments in test files to be stable documentation rather than session notes. Co-Authored-By: Claude Opus 4.6 <[email protected]>
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
2 participants
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.
This PR adds better temporal-Forge support in Sterling, provides a missing native library (for Linux 64-bit), resolves a regression introduced into the ABAC domain model, and refactors the internal CI suite for efficiency and completeness (i.e., around ABAC).