Fix missing error check in AST for expr->intexpr conversion; add new test modality #247
Conversation
This file contains 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
…not name); inferring atom types for evaluator
tnelson
added a commit
that referenced
this pull request
Mar 31, 2024
* fix: sem ver up; push action is from another repo * fix: remove old forge/forge/forge/check-ex-spec * Replacing where blocks with test-suite construct (#171) Co-authored-by: Siddhartha Prasad <siddharthaprasad@siddharthas-mbp.devices.brown.edu> Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * Typed Froglet (#154) Basic `#lang froglet`. The behavior is 99% `forge/bsl` and 1% static type checks. More to coming. * don't export unnamed tests / runs (#172) * Property Where Syntax update (#174) Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * froglet / bsl: allow +, -> in examples (#173) * bump version * restore the syntax-local-context of example blocks (#178) move the syntax-parameterize INSIDE the example form, so the whole thing still appears in a module context and the subterms get covered by the parameterize * ci: revert froglet install, forge works for both (#176) * ci: use LOCAL forge, not pkg forge * feat: universal dylibs for minisat, minisatp, glucose * froglet: fix internal arity error * no examples in temporal mode (#179) * flush logs at toplevel (#177) * froglet checkpoint (#185) * froglet: save type env, restore on import * froglet: start type#, change op errors * froglet: build syntax->type hash * typed-froglet: more typechecking, preds expect formulas * froglet: add context to typechecker, re-enable field typechecks +more deparsing context = expr subexpr example, need this to turn checks on / off * example: quick fix for multi-line bounds put the stx-parameterize around every bound is there a cleaner way? * examples: use one syntax-parameterize, not N, flatten bounds later (#189) * typed froglet checkpoint (#188) * froglet: fix conflicts with dev * ... other commits in pr * fix ci * local froglet, not pkgs * forge/bsl: don't use 'froglet' in runtime error messages * uncomment error tests * ci: use local froglet * server: relax regexp for java version allow a major number only, no minor number * add flag to hide preds (#181) * Unset _JAVA__OPTIONS in `java>=1.9?' (#193) * One pardinus (#187) Multiple solver states in one Pardinus process, indexed by run name * Logging: anonymize paths in error outputs, print boring string on failure (#196) * detect use of temporal operators without temporal mode * parser: change ~literal to ~datum (#201) the brag parser puts symbols in head position, not identifiers, so ~literal (which compares free-identifier=?) isn't right and ~datum is better, so students can define a sig Name {} or whatever without breaking the expander * feat: test case for PR 201 * forge/bsl: allow + -> in inst blocks (#202) * forge/bsl: allow + -> in inst blocks * inst, flatten * ^ fix require * fix: metadata transmission to sterling * print git branch, commit, timestamp info (#195) * print git branch, commit, timestamp info * ^ return void, don't print * ^ get forge pkg path * housekeeping: relocate OLD, consolidate * feat: updated Sterling for dev testing * add binary-tree vis example * static example * fix: faster Edge object rendering * add tree3 viz example * minor change to tree3 * fix: CI badge * CI badge * improved tree3 * update Sterling: events, arcs, images, pictures * fix: sterling update * add do-time macro, time a few spots (#210) * semanticVersion: canonize major/minor numbers (#205) Use 2.5 instead of 2.5.0 as a version number Racket prefers this, to have a canonical normal form Fix #204 * Crypto DSL for Guttmanfest (#209) * crypto: rough initial import from old * fix: properly send Skolem relation arity * . * fix: upper bounds for 'exactly' scoped but non 'one' subsigs * racket to racket/base * racket->racket/base * cleanup: no longer need kodkod-cli * racket->racket/base * more racket->racket/base * more pruning dependencies * move old example folder out of package dir * working on examples cleanup/updating * forge: more examples dir cleanup * forge: more cleanup * minor cleanup, enable run_sterling option to carry a filename * sending script text if provided, fix relative paths (#216) * Basic updates to AST, parsing to prep for 2024 (#217) * work toward pred/fun spacer AST nodes * example: odd DrRacket behavior? * working on spacers * working on spacers, but getting data needed requires remembering multiplicites * adapting macros for spacers, stop overloading int comparison ops * continuing work * working * working * working; expanding tests for fun * working; domain and range are OK * continuing work on testing fun metadata * update test suite; quantifier forms. quantifiers currently throw away multiplicity info * working to add metadata to pred declaration * minor fix for grouped variable declarations * working on robustness for mexpr struct * clear todos * working * working: splitting off parsing for bounds * working: don't forget cardinality * holding partial work for stability, do not use * cleanup: minor, crypto domain * working on revised inst stx * intermediate work * working * remove old printf * some fixes * fix for reachable, seq library todo * fix: seq library, builtin generator macro * add: .frg~ to gitignore * fix: confirm in froglet * fix: cleanup of many, but not all, filepath require specs * add: skeletal pattern for piecewise bind * intermediate: save work on piecewise bounds * add: some documentation * save intermediate work, testing * fix; testing; enum todos * small fix, add tests for plinear * intermediate: improve tests, need to add 'no' func * todo: ni stream error; piecewise limit domain * fix: lower bound cannot be #f; better error * add ni case for piecewise bounds * fix: piecewise bounds domain * add: error tests for piecewise binds * working on syntax loc for bounds errors, putting issue down for now * fix: helper functions can safely 'return' an intexpr * add: fun test for non-nullary case * fix: Sterling rebuild from dev branch * add: #lang forge/temporal * add: 5 simple examples * fix: f4_counter * add: Mia's viz for crypto * add: GCW puzzle example, original vis script * add: network lab adaptation to Forge * fix: join on helper functions, crypto example * add: reflect crypto example * update: add note on narrowing, minimal example * ABAC DSL, some fixes (#220) * working on ABAC DSL import from 2019 * add reader * fix: for convenience in forge/core, allow n-ary union in the eval-exp func * working * working * working on abac * working on abac * policy queries, cleanup display for example 1 * abac updates, remove TODOs in examples * abac + pre-Pardinus error addition * fix for unused request variables in abac * minor: double-check implicit and in inst * fix: bug if running from unsaved editor in drracket * doc/errmsg: some comments in forgeserver * fix: typos: duplicate test names * fix: missed one * fix: stopgap to show an actual message if out of instances * fix: readable errors, although Sterling displays poorly * update: sterling * fix: stop trying to reload a run_sterling file if it doesn't exist * update Sterling: pre-load script * fix: consistent update outside of strict dev mode * fix: improve error in case set comprehension is used improperly * Retain sytnax loc (#221) * fix: preserve no-field sig stxloc * working on fixing more stxloc flow to bounds * temporary: researching syntax-object srcloc, may have found issue * temporary: confirmed hypothesis, need to use datum->syntax with srcloc argument * cleanup: remove debug prints, add warning in reader * fix: saving more stxloc information --------- Co-authored-by: tbn <tbn@eng-kt-lt01.brown.edu> Co-authored-by: tbn <tbn@tstaffs-MacBook-Pro.local> * fix: preserve stx loc when desugaring test, example * Roll in better handling of some errors, propagate stxloc; beginnings of srcloc tests (#223) * working on improving srcloc display in errors * working on improving errors * fix: resolve eq/hash issues caused by making formulas procedures * working on being able to test srcloc info * working on validating srclocs * minor fixes * working * working --------- Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> * add: test case confirming 'no' works for piecewise insts * fix: source location reported for test failure * Fix usererror illformed block (#227) * working on improving srcloc display in errors * working on improving errors * fix: resolve eq/hash issues caused by making formulas procedures * working on being able to test srcloc info * working on validating srclocs * minor fixes * working * working * fix: preserve source location of pred/fun use sites: * fix: revert prior change, switch to raise-forge-error in some places * fix: more raise-forge-error, 2 more tests * fix: better error if a run is given a non-formula * working --------- Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> * fix: better errors for non-field arguments to reachable * add: improve error when reachable given too few args * Adding universal quantification to asserts (#228) * Adding quantified assertion test * Closer * Trying to have better test names * Adding temp names * PRE DISJ * I think disj is fixed * Quantified asserts * I believe this works now * Minor change * add: 2 test cases for quantified assertions' --------- Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> Co-authored-by: Tim Nelson <tbnelson@gmail.com> * Add improved error for piecewise bind definition (#230) * fix: add better error if piecewise binds don't fit within available sig atoms * fix: better error * Shoring up core language's ability to give a target instance to solver for minimization etc. (#231) * starting work on target o * working * Error for piecewise bounds if an atom is named that isn't present in the domain sig (#233) * fix: add better error if piecewise binds don't fit within available sig atoms * fix: better error * If unable to open a browser for Sterling, keep running the server and print the url (#234) * fix: attempting to fail with workaround if no browser auto-opening * fix * fix: add newline * Error if an integer literal appears which is bigger than the given bitwidth (#232) * initial test case, before writing error * draft: intermediate work * working * working * working * fix tests, add verbose 0 to some * add: int structure confirmation for 5 Int * fix: properly parse assertions with quantifiers inside suites * Error for "detached" negative numeric constants (#235) * error message with loc for detatched negative parsing * add: test just to be safe * Sig and Field AST nodes will now properly record their use location (#236) * working on preserving use-site location for sig references * working * add: field use locs * add: missing files * Quantified assert fix (#239) * Added test * Works for the number case, need more complicated exprs * Adding more * Added some more tests --------- Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * Allowing multiple failing tests in a Forge run (#242) * prototype of all-tests-before-failure * add output of test failures to forge/bsl * Reporting forge errors to stderr * Adding multiple failure test * Test update * add: more prototype code for multi-test-failure testing * it works * Added tests * Adding a forge bsl test --------- Co-authored-by: Tim Nelson <tbnelson@gmail.com> Co-authored-by: Siddhartha Prasad <siddharthaprasad@Siddharthas-MacBook-Pro.local> * Error message if no parent sig scope, but child scopes exceed default (#243) * fix: sterling: show Skolem tags, empty instance box message * fix: double-check runs for failing examples need de-duplicated names * Fix: better handling for multiple-tests (#245) * Basic type-checking for predicate use, pred/fun syntax location use site fix (#244) * Add basic typechecking for helper functions (#248) * feat: func typechecks added * Error message updated and deprimify prototype * first attempt at DFS * feat: added deprimify * change deprimify to use values --------- Co-authored-by: k-mouline <karim_mouline@brown.edu> * Fix missing error check in AST for expr->intexpr conversion; add new test modality (#247) * Infer type of atoms sent from evaluator (#249) * feat: clean up core display so that VSCode can highlight matches * Feat granular cores (#252) * progress: reconstructing subformula from path string * fix source-location for some-quantified variables -- TODO, fix for all, etc. * working: adding qvar macro use to preserve stx loc * fix: sum quant labeling. TODO: temporal-mode formula mapping * working: be more robust to unknown formulas as cores * fix deparser for add/subtract/multiply/divide * minor: say how many total formulas in header --------- Co-authored-by: Siddhartha Prasad <nivsidad@gmail.com> Co-authored-by: Siddhartha Prasad <siddharthaprasad@siddharthas-mbp.devices.brown.edu> Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> Co-authored-by: Ben Greenman <benjaminlgreenman@gmail.com> Co-authored-by: Jakob <jakob@memeware.net> Co-authored-by: tbn <tbn@eng-kt-lt01.brown.edu> Co-authored-by: tbn <tbn@tstaffs-MacBook-Pro.local> Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> Co-authored-by: Siddhartha Prasad <siddharthaprasad@Siddharthas-MacBook-Pro.local> Co-authored-by: k-mouline <karim_mouline@brown.edu>
tnelson
added a commit
that referenced
this pull request
Apr 2, 2024
…255) * fix: sem ver up; push action is from another repo * fix: remove old forge/forge/forge/check-ex-spec * Replacing where blocks with test-suite construct (#171) Co-authored-by: Siddhartha Prasad <siddharthaprasad@siddharthas-mbp.devices.brown.edu> Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * Typed Froglet (#154) Basic `#lang froglet`. The behavior is 99% `forge/bsl` and 1% static type checks. More to coming. * don't export unnamed tests / runs (#172) * Property Where Syntax update (#174) Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * froglet / bsl: allow +, -> in examples (#173) * bump version * restore the syntax-local-context of example blocks (#178) move the syntax-parameterize INSIDE the example form, so the whole thing still appears in a module context and the subterms get covered by the parameterize * ci: revert froglet install, forge works for both (#176) * ci: use LOCAL forge, not pkg forge * feat: universal dylibs for minisat, minisatp, glucose * froglet: fix internal arity error * no examples in temporal mode (#179) * flush logs at toplevel (#177) * froglet checkpoint (#185) * froglet: save type env, restore on import * froglet: start type#, change op errors * froglet: build syntax->type hash * typed-froglet: more typechecking, preds expect formulas * froglet: add context to typechecker, re-enable field typechecks +more deparsing context = expr subexpr example, need this to turn checks on / off * example: quick fix for multi-line bounds put the stx-parameterize around every bound is there a cleaner way? * examples: use one syntax-parameterize, not N, flatten bounds later (#189) * typed froglet checkpoint (#188) * froglet: fix conflicts with dev * ... other commits in pr * fix ci * local froglet, not pkgs * forge/bsl: don't use 'froglet' in runtime error messages * uncomment error tests * ci: use local froglet * server: relax regexp for java version allow a major number only, no minor number * add flag to hide preds (#181) * Unset _JAVA__OPTIONS in `java>=1.9?' (#193) * One pardinus (#187) Multiple solver states in one Pardinus process, indexed by run name * Logging: anonymize paths in error outputs, print boring string on failure (#196) * detect use of temporal operators without temporal mode * parser: change ~literal to ~datum (#201) the brag parser puts symbols in head position, not identifiers, so ~literal (which compares free-identifier=?) isn't right and ~datum is better, so students can define a sig Name {} or whatever without breaking the expander * feat: test case for PR 201 * forge/bsl: allow + -> in inst blocks (#202) * forge/bsl: allow + -> in inst blocks * inst, flatten * ^ fix require * fix: metadata transmission to sterling * print git branch, commit, timestamp info (#195) * print git branch, commit, timestamp info * ^ return void, don't print * ^ get forge pkg path * housekeeping: relocate OLD, consolidate * feat: updated Sterling for dev testing * add binary-tree vis example * static example * fix: faster Edge object rendering * add tree3 viz example * minor change to tree3 * fix: CI badge * CI badge * improved tree3 * update Sterling: events, arcs, images, pictures * fix: sterling update * add do-time macro, time a few spots (#210) * semanticVersion: canonize major/minor numbers (#205) Use 2.5 instead of 2.5.0 as a version number Racket prefers this, to have a canonical normal form Fix #204 * Crypto DSL for Guttmanfest (#209) * crypto: rough initial import from old * fix: properly send Skolem relation arity * . * fix: upper bounds for 'exactly' scoped but non 'one' subsigs * racket to racket/base * racket->racket/base * cleanup: no longer need kodkod-cli * racket->racket/base * more racket->racket/base * more pruning dependencies * move old example folder out of package dir * working on examples cleanup/updating * forge: more examples dir cleanup * forge: more cleanup * minor cleanup, enable run_sterling option to carry a filename * sending script text if provided, fix relative paths (#216) * Basic updates to AST, parsing to prep for 2024 (#217) * work toward pred/fun spacer AST nodes * example: odd DrRacket behavior? * working on spacers * working on spacers, but getting data needed requires remembering multiplicites * adapting macros for spacers, stop overloading int comparison ops * continuing work * working * working * working; expanding tests for fun * working; domain and range are OK * continuing work on testing fun metadata * update test suite; quantifier forms. quantifiers currently throw away multiplicity info * working to add metadata to pred declaration * minor fix for grouped variable declarations * working on robustness for mexpr struct * clear todos * working * working: splitting off parsing for bounds * working: don't forget cardinality * holding partial work for stability, do not use * cleanup: minor, crypto domain * working on revised inst stx * intermediate work * working * remove old printf * some fixes * fix for reachable, seq library todo * fix: seq library, builtin generator macro * add: .frg~ to gitignore * fix: confirm in froglet * fix: cleanup of many, but not all, filepath require specs * add: skeletal pattern for piecewise bind * intermediate: save work on piecewise bounds * add: some documentation * save intermediate work, testing * fix; testing; enum todos * small fix, add tests for plinear * intermediate: improve tests, need to add 'no' func * todo: ni stream error; piecewise limit domain * fix: lower bound cannot be #f; better error * add ni case for piecewise bounds * fix: piecewise bounds domain * add: error tests for piecewise binds * working on syntax loc for bounds errors, putting issue down for now * fix: helper functions can safely 'return' an intexpr * add: fun test for non-nullary case * fix: Sterling rebuild from dev branch * add: #lang forge/temporal * add: 5 simple examples * fix: f4_counter * add: Mia's viz for crypto * add: GCW puzzle example, original vis script * add: network lab adaptation to Forge * fix: join on helper functions, crypto example * add: reflect crypto example * update: add note on narrowing, minimal example * ABAC DSL, some fixes (#220) * working on ABAC DSL import from 2019 * add reader * fix: for convenience in forge/core, allow n-ary union in the eval-exp func * working * working * working on abac * working on abac * policy queries, cleanup display for example 1 * abac updates, remove TODOs in examples * abac + pre-Pardinus error addition * fix for unused request variables in abac * minor: double-check implicit and in inst * fix: bug if running from unsaved editor in drracket * doc/errmsg: some comments in forgeserver * fix: typos: duplicate test names * fix: missed one * fix: stopgap to show an actual message if out of instances * fix: readable errors, although Sterling displays poorly * update: sterling * fix: stop trying to reload a run_sterling file if it doesn't exist * update Sterling: pre-load script * fix: consistent update outside of strict dev mode * fix: improve error in case set comprehension is used improperly * Retain sytnax loc (#221) * fix: preserve no-field sig stxloc * working on fixing more stxloc flow to bounds * temporary: researching syntax-object srcloc, may have found issue * temporary: confirmed hypothesis, need to use datum->syntax with srcloc argument * cleanup: remove debug prints, add warning in reader * fix: saving more stxloc information --------- Co-authored-by: tbn <tbn@eng-kt-lt01.brown.edu> Co-authored-by: tbn <tbn@tstaffs-MacBook-Pro.local> * fix: preserve stx loc when desugaring test, example * Roll in better handling of some errors, propagate stxloc; beginnings of srcloc tests (#223) * working on improving srcloc display in errors * working on improving errors * fix: resolve eq/hash issues caused by making formulas procedures * working on being able to test srcloc info * working on validating srclocs * minor fixes * working * working --------- Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> * add: test case confirming 'no' works for piecewise insts * fix: source location reported for test failure * Fix usererror illformed block (#227) * working on improving srcloc display in errors * working on improving errors * fix: resolve eq/hash issues caused by making formulas procedures * working on being able to test srcloc info * working on validating srclocs * minor fixes * working * working * fix: preserve source location of pred/fun use sites: * fix: revert prior change, switch to raise-forge-error in some places * fix: more raise-forge-error, 2 more tests * fix: better error if a run is given a non-formula * working --------- Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> * fix: better errors for non-field arguments to reachable * add: improve error when reachable given too few args * Adding universal quantification to asserts (#228) * Adding quantified assertion test * Closer * Trying to have better test names * Adding temp names * PRE DISJ * I think disj is fixed * Quantified asserts * I believe this works now * Minor change * add: 2 test cases for quantified assertions' --------- Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> Co-authored-by: Tim Nelson <tbnelson@gmail.com> * Add improved error for piecewise bind definition (#230) * fix: add better error if piecewise binds don't fit within available sig atoms * fix: better error * Shoring up core language's ability to give a target instance to solver for minimization etc. (#231) * starting work on target o * working * Error for piecewise bounds if an atom is named that isn't present in the domain sig (#233) * fix: add better error if piecewise binds don't fit within available sig atoms * fix: better error * If unable to open a browser for Sterling, keep running the server and print the url (#234) * fix: attempting to fail with workaround if no browser auto-opening * fix * fix: add newline * Error if an integer literal appears which is bigger than the given bitwidth (#232) * initial test case, before writing error * draft: intermediate work * working * working * working * fix tests, add verbose 0 to some * add: int structure confirmation for 5 Int * fix: properly parse assertions with quantifiers inside suites * Error for "detached" negative numeric constants (#235) * error message with loc for detatched negative parsing * add: test just to be safe * Sig and Field AST nodes will now properly record their use location (#236) * working on preserving use-site location for sig references * working * add: field use locs * add: missing files * Quantified assert fix (#239) * Added test * Works for the number case, need more complicated exprs * Adding more * Added some more tests --------- Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * Allowing multiple failing tests in a Forge run (#242) * prototype of all-tests-before-failure * add output of test failures to forge/bsl * Reporting forge errors to stderr * Adding multiple failure test * Test update * add: more prototype code for multi-test-failure testing * it works * Added tests * Adding a forge bsl test --------- Co-authored-by: Tim Nelson <tbnelson@gmail.com> Co-authored-by: Siddhartha Prasad <siddharthaprasad@Siddharthas-MacBook-Pro.local> * Error message if no parent sig scope, but child scopes exceed default (#243) * fix: sterling: show Skolem tags, empty instance box message * fix: double-check runs for failing examples need de-duplicated names * Fix: better handling for multiple-tests (#245) * Basic type-checking for predicate use, pred/fun syntax location use site fix (#244) * Add basic typechecking for helper functions (#248) * feat: func typechecks added * Error message updated and deprimify prototype * first attempt at DFS * feat: added deprimify * change deprimify to use values --------- Co-authored-by: k-mouline <karim_mouline@brown.edu> * Fix missing error check in AST for expr->intexpr conversion; add new test modality (#247) * Infer type of atoms sent from evaluator (#249) * feat: clean up core display so that VSCode can highlight matches * Feat granular cores (#252) * progress: reconstructing subformula from path string * fix source-location for some-quantified variables -- TODO, fix for all, etc. * working: adding qvar macro use to preserve stx loc * fix: sum quant labeling. TODO: temporal-mode formula mapping * working: be more robust to unknown formulas as cores * fix deparser for add/subtract/multiply/divide * minor: say how many total formulas in header * Fix: core top-level wrapping, syntax-location at top-level in "check" macro (#254) * fix: wrap top-level fmla indexes in Pardinus * add: some fuzz tests for cores * fix: source location preservation in assertion->check macros * fix: optional pred in check macro --------- Co-authored-by: Siddhartha Prasad <nivsidad@gmail.com> Co-authored-by: Siddhartha Prasad <siddharthaprasad@siddharthas-mbp.devices.brown.edu> Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> Co-authored-by: Ben Greenman <benjaminlgreenman@gmail.com> Co-authored-by: Jakob <jakob@memeware.net> Co-authored-by: tbn <tbn@eng-kt-lt01.brown.edu> Co-authored-by: tbn <tbn@tstaffs-MacBook-Pro.local> Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> Co-authored-by: Siddhartha Prasad <siddharthaprasad@Siddharthas-MacBook-Pro.local> Co-authored-by: k-mouline <karim_mouline@brown.edu>
tnelson
added a commit
that referenced
this pull request
May 31, 2024
* fix: sem ver up; push action is from another repo * fix: remove old forge/forge/forge/check-ex-spec * Replacing where blocks with test-suite construct (#171) Co-authored-by: Siddhartha Prasad <siddharthaprasad@siddharthas-mbp.devices.brown.edu> Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * Typed Froglet (#154) Basic `#lang froglet`. The behavior is 99% `forge/bsl` and 1% static type checks. More to coming. * don't export unnamed tests / runs (#172) * Property Where Syntax update (#174) Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * froglet / bsl: allow +, -> in examples (#173) * bump version * restore the syntax-local-context of example blocks (#178) move the syntax-parameterize INSIDE the example form, so the whole thing still appears in a module context and the subterms get covered by the parameterize * ci: revert froglet install, forge works for both (#176) * ci: use LOCAL forge, not pkg forge * feat: universal dylibs for minisat, minisatp, glucose * froglet: fix internal arity error * no examples in temporal mode (#179) * flush logs at toplevel (#177) * froglet checkpoint (#185) * froglet: save type env, restore on import * froglet: start type#, change op errors * froglet: build syntax->type hash * typed-froglet: more typechecking, preds expect formulas * froglet: add context to typechecker, re-enable field typechecks +more deparsing context = expr subexpr example, need this to turn checks on / off * example: quick fix for multi-line bounds put the stx-parameterize around every bound is there a cleaner way? * examples: use one syntax-parameterize, not N, flatten bounds later (#189) * typed froglet checkpoint (#188) * froglet: fix conflicts with dev * ... other commits in pr * fix ci * local froglet, not pkgs * forge/bsl: don't use 'froglet' in runtime error messages * uncomment error tests * ci: use local froglet * server: relax regexp for java version allow a major number only, no minor number * add flag to hide preds (#181) * Unset _JAVA__OPTIONS in `java>=1.9?' (#193) * One pardinus (#187) Multiple solver states in one Pardinus process, indexed by run name * Logging: anonymize paths in error outputs, print boring string on failure (#196) * detect use of temporal operators without temporal mode * parser: change ~literal to ~datum (#201) the brag parser puts symbols in head position, not identifiers, so ~literal (which compares free-identifier=?) isn't right and ~datum is better, so students can define a sig Name {} or whatever without breaking the expander * feat: test case for PR 201 * forge/bsl: allow + -> in inst blocks (#202) * forge/bsl: allow + -> in inst blocks * inst, flatten * ^ fix require * fix: metadata transmission to sterling * print git branch, commit, timestamp info (#195) * print git branch, commit, timestamp info * ^ return void, don't print * ^ get forge pkg path * housekeeping: relocate OLD, consolidate * feat: updated Sterling for dev testing * add binary-tree vis example * static example * fix: faster Edge object rendering * add tree3 viz example * minor change to tree3 * fix: CI badge * CI badge * improved tree3 * update Sterling: events, arcs, images, pictures * fix: sterling update * add do-time macro, time a few spots (#210) * semanticVersion: canonize major/minor numbers (#205) Use 2.5 instead of 2.5.0 as a version number Racket prefers this, to have a canonical normal form Fix #204 * Crypto DSL for Guttmanfest (#209) * crypto: rough initial import from old * fix: properly send Skolem relation arity * . * fix: upper bounds for 'exactly' scoped but non 'one' subsigs * racket to racket/base * racket->racket/base * cleanup: no longer need kodkod-cli * racket->racket/base * more racket->racket/base * more pruning dependencies * move old example folder out of package dir * working on examples cleanup/updating * forge: more examples dir cleanup * forge: more cleanup * minor cleanup, enable run_sterling option to carry a filename * sending script text if provided, fix relative paths (#216) * Basic updates to AST, parsing to prep for 2024 (#217) * work toward pred/fun spacer AST nodes * example: odd DrRacket behavior? * working on spacers * working on spacers, but getting data needed requires remembering multiplicites * adapting macros for spacers, stop overloading int comparison ops * continuing work * working * working * working; expanding tests for fun * working; domain and range are OK * continuing work on testing fun metadata * update test suite; quantifier forms. quantifiers currently throw away multiplicity info * working to add metadata to pred declaration * minor fix for grouped variable declarations * working on robustness for mexpr struct * clear todos * working * working: splitting off parsing for bounds * working: don't forget cardinality * holding partial work for stability, do not use * cleanup: minor, crypto domain * working on revised inst stx * intermediate work * working * remove old printf * some fixes * fix for reachable, seq library todo * fix: seq library, builtin generator macro * add: .frg~ to gitignore * fix: confirm in froglet * fix: cleanup of many, but not all, filepath require specs * add: skeletal pattern for piecewise bind * intermediate: save work on piecewise bounds * add: some documentation * save intermediate work, testing * fix; testing; enum todos * small fix, add tests for plinear * intermediate: improve tests, need to add 'no' func * todo: ni stream error; piecewise limit domain * fix: lower bound cannot be #f; better error * add ni case for piecewise bounds * fix: piecewise bounds domain * add: error tests for piecewise binds * working on syntax loc for bounds errors, putting issue down for now * fix: helper functions can safely 'return' an intexpr * add: fun test for non-nullary case * fix: Sterling rebuild from dev branch * add: #lang forge/temporal * add: 5 simple examples * fix: f4_counter * add: Mia's viz for crypto * add: GCW puzzle example, original vis script * add: network lab adaptation to Forge * fix: join on helper functions, crypto example * add: reflect crypto example * update: add note on narrowing, minimal example * ABAC DSL, some fixes (#220) * working on ABAC DSL import from 2019 * add reader * fix: for convenience in forge/core, allow n-ary union in the eval-exp func * working * working * working on abac * working on abac * policy queries, cleanup display for example 1 * abac updates, remove TODOs in examples * abac + pre-Pardinus error addition * fix for unused request variables in abac * minor: double-check implicit and in inst * fix: bug if running from unsaved editor in drracket * doc/errmsg: some comments in forgeserver * fix: typos: duplicate test names * fix: missed one * fix: stopgap to show an actual message if out of instances * fix: readable errors, although Sterling displays poorly * update: sterling * fix: stop trying to reload a run_sterling file if it doesn't exist * update Sterling: pre-load script * fix: consistent update outside of strict dev mode * fix: improve error in case set comprehension is used improperly * Retain sytnax loc (#221) * fix: preserve no-field sig stxloc * working on fixing more stxloc flow to bounds * temporary: researching syntax-object srcloc, may have found issue * temporary: confirmed hypothesis, need to use datum->syntax with srcloc argument * cleanup: remove debug prints, add warning in reader * fix: saving more stxloc information --------- Co-authored-by: tbn <tbn@eng-kt-lt01.brown.edu> Co-authored-by: tbn <tbn@tstaffs-MacBook-Pro.local> * fix: preserve stx loc when desugaring test, example * Roll in better handling of some errors, propagate stxloc; beginnings of srcloc tests (#223) * working on improving srcloc display in errors * working on improving errors * fix: resolve eq/hash issues caused by making formulas procedures * working on being able to test srcloc info * working on validating srclocs * minor fixes * working * working --------- Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> * add: test case confirming 'no' works for piecewise insts * fix: source location reported for test failure * Fix usererror illformed block (#227) * working on improving srcloc display in errors * working on improving errors * fix: resolve eq/hash issues caused by making formulas procedures * working on being able to test srcloc info * working on validating srclocs * minor fixes * working * working * fix: preserve source location of pred/fun use sites: * fix: revert prior change, switch to raise-forge-error in some places * fix: more raise-forge-error, 2 more tests * fix: better error if a run is given a non-formula * working --------- Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> * fix: better errors for non-field arguments to reachable * add: improve error when reachable given too few args * Adding universal quantification to asserts (#228) * Adding quantified assertion test * Closer * Trying to have better test names * Adding temp names * PRE DISJ * I think disj is fixed * Quantified asserts * I believe this works now * Minor change * add: 2 test cases for quantified assertions' --------- Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> Co-authored-by: Tim Nelson <tbnelson@gmail.com> * Add improved error for piecewise bind definition (#230) * fix: add better error if piecewise binds don't fit within available sig atoms * fix: better error * Shoring up core language's ability to give a target instance to solver for minimization etc. (#231) * starting work on target o * working * Error for piecewise bounds if an atom is named that isn't present in the domain sig (#233) * fix: add better error if piecewise binds don't fit within available sig atoms * fix: better error * If unable to open a browser for Sterling, keep running the server and print the url (#234) * fix: attempting to fail with workaround if no browser auto-opening * fix * fix: add newline * Error if an integer literal appears which is bigger than the given bitwidth (#232) * initial test case, before writing error * draft: intermediate work * working * working * working * fix tests, add verbose 0 to some * add: int structure confirmation for 5 Int * fix: properly parse assertions with quantifiers inside suites * Error for "detached" negative numeric constants (#235) * error message with loc for detatched negative parsing * add: test just to be safe * Sig and Field AST nodes will now properly record their use location (#236) * working on preserving use-site location for sig references * working * add: field use locs * add: missing files * Quantified assert fix (#239) * Added test * Works for the number case, need more complicated exprs * Adding more * Added some more tests --------- Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> * Allowing multiple failing tests in a Forge run (#242) * prototype of all-tests-before-failure * add output of test failures to forge/bsl * Reporting forge errors to stderr * Adding multiple failure test * Test update * add: more prototype code for multi-test-failure testing * it works * Added tests * Adding a forge bsl test --------- Co-authored-by: Tim Nelson <tbnelson@gmail.com> Co-authored-by: Siddhartha Prasad <siddharthaprasad@Siddharthas-MacBook-Pro.local> * Error message if no parent sig scope, but child scopes exceed default (#243) * fix: sterling: show Skolem tags, empty instance box message * fix: double-check runs for failing examples need de-duplicated names * Fix: better handling for multiple-tests (#245) * Basic type-checking for predicate use, pred/fun syntax location use site fix (#244) * Add basic typechecking for helper functions (#248) * feat: func typechecks added * Error message updated and deprimify prototype * first attempt at DFS * feat: added deprimify * change deprimify to use values --------- Co-authored-by: k-mouline <karim_mouline@brown.edu> * Fix missing error check in AST for expr->intexpr conversion; add new test modality (#247) * Infer type of atoms sent from evaluator (#249) * feat: clean up core display so that VSCode can highlight matches * Feat granular cores (#252) * progress: reconstructing subformula from path string * fix source-location for some-quantified variables -- TODO, fix for all, etc. * working: adding qvar macro use to preserve stx loc * fix: sum quant labeling. TODO: temporal-mode formula mapping * working: be more robust to unknown formulas as cores * fix deparser for add/subtract/multiply/divide * minor: say how many total formulas in header * Fix: core top-level wrapping, syntax-location at top-level in "check" macro (#254) * fix: wrap top-level fmla indexes in Pardinus * add: some fuzz tests for cores * fix: source location preservation in assertion->check macros * fix: optional pred in check macro * Feat priming checks (#256) * Struct implemented * struct mostly supported * now it works * priming check added * testing: social network electrum test corrections * last duplicate removed --------- Co-authored-by: Tim Nelson <tbnelson@gmail.com> * feat: xor operator (macro, surface); tests (#257) * working on examples dir * add: more examples from the public repo * add: Prim's * improve Prim model performance * fix: error in malformed inst case, some cleanup --------- Co-authored-by: Siddhartha Prasad <nivsidad@gmail.com> Co-authored-by: Siddhartha Prasad <siddharthaprasad@siddharthas-mbp.devices.brown.edu> Co-authored-by: Siddhartha Prasad <siddhartha.a.prasad@gmail.com> Co-authored-by: Ben Greenman <benjaminlgreenman@gmail.com> Co-authored-by: Jakob <jakob@memeware.net> Co-authored-by: tbn <tbn@eng-kt-lt01.brown.edu> Co-authored-by: tbn <tbn@tstaffs-MacBook-Pro.local> Co-authored-by: tbn <tbn@somerville2.local> Co-authored-by: tbn <tbn@eng-kt-lt01.ad.brown.edu> Co-authored-by: Siddhartha Prasad <siddharthaprasad@Siddharthas-MacBook-Pro.local> Co-authored-by: k-mouline <karim_mouline@brown.edu> Co-authored-by: Karim Mouline <113158763+k-mouline@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Tests within a
test expectblock can now useis forge_error; which will pass only if a Racket user-error is produced by running the test. We use Racket user-errors here because they are whatreport-forge-errorproduces: they don't have a confusing stack trace, the message can (and usually does) contain a source location, etc.