{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":34082065,"defaultBranch":"master","name":"saw-script","ownerLogin":"GaloisInc","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-04-16T21:39:32.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/1584774?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1716563369.0","currentOid":""},"activityList":{"items":[{"before":"59392fd096c1e3806c90db21a084c6cc80c05a53","after":"5ea9e1e4d781633c67407219a92ad299f1620534","ref":"refs/heads/master","pushedAt":"2024-05-24T15:09:29.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"glguy","name":"Eric Mertens","path":"/glguy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12164?s=80&v=4"},"commit":{"message":"Update llvm-pretty submodule target (#2059)","shortMessageHtmlLink":"Update llvm-pretty submodule target (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2314014404\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/saw-script/issues/2059\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/GaloisInc/saw-script/pull/2059/hovercard\" href=\"https://github.com/GaloisInc/saw-script/pull/2059\">#2059</a>)"}},{"before":"e5d1ce6647c3b85d61b901b5a8949bae92d1b484","after":null,"ref":"refs/heads/llvm-pretty-migration","pushedAt":"2024-05-24T15:09:29.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"glguy","name":"Eric Mertens","path":"/glguy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12164?s=80&v=4"}},{"before":null,"after":"e5d1ce6647c3b85d61b901b5a8949bae92d1b484","ref":"refs/heads/llvm-pretty-migration","pushedAt":"2024-05-23T23:25:57.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"glguy","name":"Eric Mertens","path":"/glguy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12164?s=80&v=4"},"commit":{"message":"Update llvm-pretty submodule target","shortMessageHtmlLink":"Update llvm-pretty submodule target"}},{"before":"0f13874c6b839d3e21d11dc5b7d015d25ce94f65","after":null,"ref":"refs/heads/rem/issue#2055","pushedAt":"2024-05-17T02:09:25.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mccleeary-galois","name":null,"path":"/mccleeary-galois","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/139989328?s=80&v=4"}},{"before":"70fe999e65135818874aea145b64fb5fbb78d4fa","after":"59392fd096c1e3806c90db21a084c6cc80c05a53","ref":"refs/heads/master","pushedAt":"2024-05-17T02:09:24.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"mccleeary-galois","name":null,"path":"/mccleeary-galois","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/139989328?s=80&v=4"},"commit":{"message":"Merge pull request #2056 from GaloisInc/rem/issue#2055\n\nFix #2055","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2301193085\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/saw-script/issues/2056\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/GaloisInc/saw-script/pull/2056/hovercard\" href=\"https://github.com/GaloisInc/saw-script/pull/2056\">#2056</a> from GaloisInc/rem/issue#2055"}},{"before":"9371c75bc75573184ac55f8599037bf0b2e2644f","after":"0f13874c6b839d3e21d11dc5b7d015d25ce94f65","ref":"refs/heads/rem/issue#2055","pushedAt":"2024-05-16T21:56:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mccleeary-galois","name":null,"path":"/mccleeary-galois","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/139989328?s=80&v=4"},"commit":{"message":"Change saw-remote-api version to dev v1.1.1.99","shortMessageHtmlLink":"Change saw-remote-api version to dev v1.1.1.99"}},{"before":"ed63d5ebe34f4e838b4270054c4120dc437ecc25","after":"9371c75bc75573184ac55f8599037bf0b2e2644f","ref":"refs/heads/rem/issue#2055","pushedAt":"2024-05-16T20:53:28.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mccleeary-galois","name":null,"path":"/mccleeary-galois","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/139989328?s=80&v=4"},"commit":{"message":"Ready saw-remote-api for v1.1.1 to handle python 3.12","shortMessageHtmlLink":"Ready saw-remote-api for v1.1.1 to handle python 3.12"}},{"before":"8e40029d535c3ddac7b3eb76f7ca6fa87fb171a9","after":"ed63d5ebe34f4e838b4270054c4120dc437ecc25","ref":"refs/heads/rem/issue#2055","pushedAt":"2024-05-16T20:51:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mccleeary-galois","name":null,"path":"/mccleeary-galois","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/139989328?s=80&v=4"},"commit":{"message":"Update .github/workflows/ci.yml\n\nCo-authored-by: Ryan Scott <rscott@galois.com>","shortMessageHtmlLink":"Update .github/workflows/ci.yml"}},{"before":"b683f75b455b3d51502e5d146131f546bc5dae01","after":"8e40029d535c3ddac7b3eb76f7ca6fa87fb171a9","ref":"refs/heads/rem/issue#2055","pushedAt":"2024-05-16T20:51:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mccleeary-galois","name":null,"path":"/mccleeary-galois","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/139989328?s=80&v=4"},"commit":{"message":"Update .github/workflows/ci.yml\n\nCo-authored-by: Ryan Scott <rscott@galois.com>","shortMessageHtmlLink":"Update .github/workflows/ci.yml"}},{"before":null,"after":"b683f75b455b3d51502e5d146131f546bc5dae01","ref":"refs/heads/rem/issue#2055","pushedAt":"2024-05-16T19:32:00.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mccleeary-galois","name":null,"path":"/mccleeary-galois","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/139989328?s=80&v=4"},"commit":{"message":"Ready saw-remote-api for v1.1.1 to handle python 3.12","shortMessageHtmlLink":"Ready saw-remote-api for v1.1.1 to handle python 3.12"}},{"before":"adb59e2c7594979acc25cc7128d95431ff0cc321","after":null,"ref":"refs/heads/sygus-prep","pushedAt":"2024-05-15T13:49:48.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"}},{"before":"1722a84fef506d326edc4ffafe8a654b2ef47c3b","after":"70fe999e65135818874aea145b64fb5fbb78d4fa","ref":"refs/heads/master","pushedAt":"2024-05-15T13:49:47.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"SyGuS, find SMT array write of a fixed size (#2037)\n\n* Find SMT array write of a fixed size.\r\n\r\n* Load SMT array with concrete size.\r\n\r\n* Add test.\r\n\r\n* Add noSatisfyingWriteFreshConstant option.\r\n\r\n* Add invariant substitution to getPoststateObligations.\r\n\r\n* Bump what4.\r\n\r\n* wip\r\n\r\n* wip\r\n\r\n* Use simplified term in resolveSAWPred.\r\n\r\n* Bump crucible.\r\n\r\n* Remove unused sc.\r\n\r\n* Use simplified term in resolveSAWPred.\r\n\r\n* Bump crucible.\r\n\r\n* Update src/SAWScript/Crucible/LLVM/Builtins.hs\r\n\r\nCo-authored-by: Ryan Scott <rscott@galois.com>\r\n\r\n* Fix -Wunused-matches warning\r\n\r\n* Bump crucible, what4 submodules\r\n\r\nThis bumps:\r\n\r\n* The `crucible` submodule to bring in the changes from\r\n  GaloisInc/crucible#1178\r\n* The `what4` submodule to bring in the changes from\r\n  GaloisInc/what4#256\r\n\r\n* Remove debugging-only code\r\n\r\n* Bump cryptol-specs to incorporate GaloisInc/cryptol-specs#72\r\n\r\n* Repair AES example to work with `type Nk = AES256`\r\n\r\n* Add expert options for enabling What4-, Crucible-related SyGuS features\r\n\r\n* Split off separate llvm_verify_fixpoint_chc_x86 command\r\n\r\n* Only enable doPtrCmp optimizations with SimpleFixpointCHC\r\n\r\n* crucible: Revert popFrame refactoring\r\n\r\n* Uniformly apply pushMuxOps option to all ExprBuilders\r\n\r\nSAW creates a variety of different ExprBuilders in the course of a typical SAW\r\nscript, but we were only applying the pushMuxOps option to some of them. This\r\npatch makes the treatment a bit more comprehensive.\r\n\r\nUnfortunately, doing so requires a rather uncomfortable amount of extra\r\nplumbing in `SAWScript.Proof`, but I'm not sure how to do better without\r\nrefactoring all of `SAWScript.Proof` to use `TopLevel` instead of `IO` (and\r\nit's unclear if that is desirable).\r\n\r\n* Bump cryptol-specs, what4, crucible submodules to latest\r\n\r\n* Bump what4, crucible submodules\r\n\r\n* Adapt to recent crucible-llvm API changes\r\n\r\n---------\r\n\r\nCo-authored-by: Andrei Stefanescu <andrei@stefanescu.io>","shortMessageHtmlLink":"SyGuS, find SMT array write of a fixed size (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2164011762\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/saw-script/issues/2037\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/GaloisInc/saw-script/pull/2037/hovercard\" href=\"https://github.com/GaloisInc/saw-script/pull/2037\">#2037</a>)"}},{"before":"48dcbf7bc2551709e3dacd5c682795a039ae2635","after":"adb59e2c7594979acc25cc7128d95431ff0cc321","ref":"refs/heads/sygus-prep","pushedAt":"2024-05-14T17:42:47.000Z","pushType":"push","commitsCount":9,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Adapt to recent crucible-llvm API changes","shortMessageHtmlLink":"Adapt to recent crucible-llvm API changes"}},{"before":"64db69b48ac89d589584fa1f09da3e290aaae686","after":null,"ref":"refs/heads/bump-entree-specs-commit","pushedAt":"2024-05-10T16:16:42.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"}},{"before":"48e0e7d64551e0d80ee456674c6164c789e1ad43","after":"1722a84fef506d326edc4ffafe8a654b2ef47c3b","ref":"refs/heads/master","pushedAt":"2024-05-10T16:16:42.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"CI: Bump entree-specs commit to include fix for GaloisInc/entree-specs#5 (#2054)\n\nThis bumps the pinned `entree-specs` commit to bring in the changes from\r\nGaloisInc/entree-specs#6, which requires `entree-specs` to build with\r\n`coq-itree.5.2.*`. Doing so is necessary to fix the CI failure observed in\r\nGaloisInc/entree-specs#5. Moreover, GaloisInc/entree-specs#6 adds upper version\r\nbounds to `coq-itree` in `entree-specs`' `opam` file, minimizing the likelihood\r\nof such a breakage happening again in the future.","shortMessageHtmlLink":"CI: Bump entree-specs commit to include fix for <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2256850504\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/entree-specs/issues/5\" data-hovercard-type=\"issue\" data-hovercard-url=\"/GaloisInc/entree-specs/issues/5/hovercard\" href=\"https://github.com/GaloisInc/entree-specs/issues/5\">GaloisInc/entree-specs#5</a>"}},{"before":null,"after":"64db69b48ac89d589584fa1f09da3e290aaae686","ref":"refs/heads/bump-entree-specs-commit","pushedAt":"2024-05-10T12:21:48.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"CI: Bump entree-specs commit to include fix for GaloisInc/entree-specs#5\n\nThis bumps the pinned `entree-specs` commit to bring in the changes from\nGaloisInc/entree-specs#6, which requires `entree-specs` to build with\n`coq-itree.5.2.*`. Doing so is necessary to fix the CI failure observed in\nGaloisInc/entree-specs#5. Moreover, GaloisInc/entree-specs#6 adds upper version\nbounds to `coq-itree` in `entree-specs`' `opam` file, minimizing the likelihood\nof such a breakage happening again in the future.","shortMessageHtmlLink":"CI: Bump entree-specs commit to include fix for <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2256850504\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/entree-specs/issues/5\" data-hovercard-type=\"issue\" data-hovercard-url=\"/GaloisInc/entree-specs/issues/5/hovercard\" href=\"https://github.com/GaloisInc/entree-specs/issues/5\">GaloisInc/entree-specs#5</a>"}},{"before":"9ee45fdb7c5a6b923b081f98d6591ca92f32a8a4","after":"48dcbf7bc2551709e3dacd5c682795a039ae2635","ref":"refs/heads/sygus-prep","pushedAt":"2024-04-22T14:11:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Uniformly apply pushMuxOps option to all ExprBuilders\n\nSAW creates a variety of different ExprBuilders in the course of a typical SAW\nscript, but we were only applying the pushMuxOps option to some of them. This\npatch makes the treatment a bit more comprehensive.\n\nUnfortunately, doing so requires a rather uncomfortable amount of extra\nplumbing in `SAWScript.Proof`, but I'm not sure how to do better without\nrefactoring all of `SAWScript.Proof` to use `TopLevel` instead of `IO` (and\nit's unclear if that is desirable).","shortMessageHtmlLink":"Uniformly apply pushMuxOps option to all ExprBuilders"}},{"before":"702444fc2e061ec3ca223f7a64814c4a9c4319ce","after":"3a9b0092cc8c1686cee8b7b1067c361861dfe3e2","ref":"refs/heads/mir-string-slices","pushedAt":"2024-03-29T15:06:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"MIR string slices\n\nThis adds rudimentary support for constructing MIR `str` slice references via\nthe new `mir_str_slice_value` and `mir_str_slice_range_value` SAWScript\nfunctions. These behave much like their cousins `mir_slice_value` and\n`mir_slice_range_value` (which work for array slices), except that they return\nsomething of type `&str` instead of, say, `&[u8]`. See the manual for the full\ndetails and current limitations of the approach.\n\nThe `mir_str_slice_value`/`mir_str_slice_range_value` functions mostly share\nthe same implementation as `mir_slice_value`/`mir_slice_range_value`, except\nfor some minor differences regarding how the underlying types are handled.\nThere is now a new `MirSliceInfo` data type that signals whether we are dealing\nwith a `str` slice or an array slice.\n\nFixes #1997.","shortMessageHtmlLink":"MIR string slices"}},{"before":"49a182eec7db62683b7ecfa46971db5e35d1de83","after":null,"ref":"refs/heads/T2045","pushedAt":"2024-03-28T14:44:51.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mergify[bot]","name":null,"path":"/apps/mergify","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/10562?s=80&v=4"}},{"before":"be24399f385acd966b1cb59331f636e8f1609047","after":"48e0e7d64551e0d80ee456674c6164c789e1ad43","ref":"refs/heads/master","pushedAt":"2024-03-28T14:44:50.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"mergify[bot]","name":null,"path":"/apps/mergify","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/10562?s=80&v=4"},"commit":{"message":"Merge pull request #2047 from GaloisInc/T2045\n\nFix treatment of MIR slices in overrides","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2211308641\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/saw-script/issues/2047\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/GaloisInc/saw-script/pull/2047/hovercard\" href=\"https://github.com/GaloisInc/saw-script/pull/2047\">#2047</a> from GaloisInc/T2045"}},{"before":"4428930732ddf8590ea7bf508f741c0cb7d3d560","after":"49a182eec7db62683b7ecfa46971db5e35d1de83","ref":"refs/heads/T2045","pushedAt":"2024-03-28T13:54:23.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Fix treatment of MIR slices in overrides\n\nAs noted in #2045, the previous way that MIR slice reference valus were handled\nin overrides was horribly broken, as it was registering raw slice references\n(of type `*const T`) at type `&[T; N]`. We now take steps to turn the raw slice\nreference into an array reference before registering it at type `&[T; N]`. See\nthe new `Note [Matching slices in overrides]` for the full story.\n\nFixes #2045.","shortMessageHtmlLink":"Fix treatment of MIR slices in overrides"}},{"before":null,"after":"4428930732ddf8590ea7bf508f741c0cb7d3d560","ref":"refs/heads/T2045","pushedAt":"2024-03-27T16:54:41.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Fix treatment of MIR slices in overrides\n\nAs noted in #2045, the previous way that MIR slice reference valus were handled\nin overrides was horribly broken, as it was registering raw slice references\n(of type `*const T`) at type `&[T; N]`. We now take steps to turn the raw slice\nreference into an array reference before registering it at type `&[T; N]`. See\nthe new `Note [Matching slices in overrides]` for the full story.\n\nFixes #2045.","shortMessageHtmlLink":"Fix treatment of MIR slices in overrides"}},{"before":"369178db0c4d437919e5090cabcc14d388a89c5c","after":null,"ref":"refs/heads/T2043","pushedAt":"2024-03-27T16:51:08.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"}},{"before":"d56bc186983c4ed071c3cfe97fc9904830f64673","after":"be24399f385acd966b1cb59331f636e8f1609047","ref":"refs/heads/master","pushedAt":"2024-03-27T16:51:07.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Bump cryptol submodule, add regression test for #2043 (#2044)\n\nThis bumps the `cryptol` submodule to bring in the changes from\r\nhttps://github.com/GaloisInc/cryptol/pull/1648. As a result, this fixes #2043.\r\nI have added a regression test to ensure that the issue remains fixed.","shortMessageHtmlLink":"Bump cryptol submodule, add regression test for <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2200915313\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/saw-script/issues/2043\" data-hovercard-type=\"issue\" data-hovercard-url=\"/GaloisInc/saw-script/issues/2043/hovercard\" href=\"https://github.com/GaloisInc/saw-script/issues/2043\">#2043</a> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2207963073\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/saw-script/issues/2044\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/GaloisInc/saw-script/pull/2044/hovercard\" href=\"https://github.com/GaloisInc/saw-script/pull/2044\">#2044</a>)"}},{"before":null,"after":"a6b79b96ab9908720aa9b40caa970e04a39de8f9","ref":"refs/heads/dholland-errors","pushedAt":"2024-03-27T00:44:10.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"sauclovian-g","name":"David Holland","path":"/sauclovian-g","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/120141909?s=80&v=4"},"commit":{"message":"Adjust how type errors are printed.\n\n- Adjust the indentation/formatting to make it clear that each error\nmessage is actually one and not two separate ones.\n\n- Instead of always printing the outermost enclosing types and\nsometimes the innermost mismatched types, print each recursive layer\nof the mismatched types. This helps a lot if the type is large.\n\n- Avoid treating each successive argument of functions (since they're\ncurried) as another layer to print. These prints don't help.\n\n- Strengthen the way we carry around the errors while recursing to make\nthese things possible.\n\n- We don't need to carry around the identity of the enclosing context\n(\"m\") while recursing; we print it once at the end of each message,\nand that should be sufficient now that it no longer looks like it's an\nentirely separate message.\n\nPrinting multiple layers of mismatch was inspired by what the OCaml\ncompiler does with complicated types, but none of it's directly\nanalogous.\n\nNote that the actual location of the error is printed by the caller.\nWe were printing the location of the enclosing context as if it was\nthe location of an additional error, and that was part of what was\nsignificantly confusing; it's indented now in a way that makes it\nclear it's supplemental information.\n\nThis change should be an improvement, but it's not meant to be (and\nisn't) the definitive word on any of this. There are still several\nthings that can be improved:\n   - when there's a mismatched function argument, it would be nice to\n     identify which argument it is;\n   - when there are mismatched record types, it would be nice to\n     identify and print only the mismatched fields (this is especially\n     significant because we have ad hoc records);\n   - some of the callers definitely have the expected/found type\n     arguments backwards;\n   - the source positions (in the callers) are not as granular as one\n     would like, e.g. an argument mismatch in a call is usually\n     attributed to the entire application expression.","shortMessageHtmlLink":"Adjust how type errors are printed."}},{"before":null,"after":"369178db0c4d437919e5090cabcc14d388a89c5c","ref":"refs/heads/T2043","pushedAt":"2024-03-26T11:16:15.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Bump cryptol submodule, add regression test for #2043\n\nThis bumps the `cryptol` submodule to bring in the changes from\nhttps://github.com/GaloisInc/cryptol/pull/1648. As a result, this fixes #2043.\nI have added a regression test to ensure that the issue remains fixed.","shortMessageHtmlLink":"Bump cryptol submodule, add regression test for <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2200915313\" data-permission-text=\"Title is private\" data-url=\"https://github.com/GaloisInc/saw-script/issues/2043\" data-hovercard-type=\"issue\" data-hovercard-url=\"/GaloisInc/saw-script/issues/2043/hovercard\" href=\"https://github.com/GaloisInc/saw-script/issues/2043\">#2043</a>"}},{"before":"30d0919ffa137993b2529c8f9398f94ebbd82e1d","after":"702444fc2e061ec3ca223f7a64814c4a9c4319ce","ref":"refs/heads/mir-string-slices","pushedAt":"2024-03-23T19:25:31.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"},"commit":{"message":"Merge branch 'master' into mir-string-slices","shortMessageHtmlLink":"Merge branch 'master' into mir-string-slices"}},{"before":"4fb5a7f2d82fd95d1a90aeeb4b7d0292809b3989","after":null,"ref":"refs/heads/signal-verification","pushedAt":"2024-03-22T15:03:08.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"}},{"before":"dd87fd51ef279aea76d5a322b93009aba3fda7b9","after":null,"ref":"refs/heads/ghc-9.0-9.2-bug","pushedAt":"2024-03-22T15:01:41.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"}},{"before":"c0470b5ebe1643da59a862ee28ff15bf1fd75a4c","after":null,"ref":"refs/heads/mir_verify","pushedAt":"2024-03-22T15:01:35.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"RyanGlScott","name":"Ryan Scott","path":"/RyanGlScott","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2364661?s=80&v=4"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEUyq_GwA","startCursor":null,"endCursor":null}},"title":"Activity · GaloisInc/saw-script"}