Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[minor] March 31 Update to 3.4 (#253)
* 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>
- Loading branch information
12 people
authored
Mar 31, 2024
1 parent
6f2ec8a
commit 070bf4d