{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":444890312,"defaultBranch":"master","name":"boogie","ownerLogin":"atomb","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2022-01-05T17:22:14.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/24929?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1713387220.0","currentOid":""},"activityList":{"items":[{"before":"7a8b3fae5608f9a9163f9baf1f4a65eb892af958","after":"10e362ad22af5d98490b59f01a3eb27f02125b89","ref":"refs/heads/issue-5126","pushedAt":"2024-04-18T17:45:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Remove one more unnecessary change","shortMessageHtmlLink":"Remove one more unnecessary change"}},{"before":"cd51f296cd1cddf9ae74c3d634bfe433b65dfb00","after":"7a8b3fae5608f9a9163f9baf1f4a65eb892af958","ref":"refs/heads/issue-5126","pushedAt":"2024-04-18T17:43:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Remove obsolete change","shortMessageHtmlLink":"Remove obsolete change"}},{"before":"e64b370fb05e7ff51f50aca5c0fd3cad76157f48","after":"cd51f296cd1cddf9ae74c3d634bfe433b65dfb00","ref":"refs/heads/issue-5126","pushedAt":"2024-04-17T22:11:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Fix test","shortMessageHtmlLink":"Fix test"}},{"before":null,"after":"e64b370fb05e7ff51f50aca5c0fd3cad76157f48","ref":"refs/heads/issue-5126","pushedAt":"2024-04-17T20:53:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Make /randomizeVcIterations:1 the same as no flag\n\nThis change ensures that, when specifying `/randomizeVcIterations:n`,\nthe first iteration is equivalent to that achieved by\n`/normalizeNames:1`. One consequence of this is that normalized names\nare always chosen pseudo-randomly (though deterministically, since it\nalways starts with a fixed seed, which is 0 if not otherwise specified).\n\nFixes dafny-lang/dafny#5126","shortMessageHtmlLink":"Make /randomizeVcIterations:1 the same as no flag"}},{"before":"7e04b93f7c05528350525d64bc7e5175636418d8","after":"e762e69d08bf10606abde9e472cdc36c3e8b2144","ref":"refs/heads/issue-863","pushedAt":"2024-04-11T11:53:44.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"keyboardDrummer","name":"Remy Willems","path":"/keyboardDrummer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3121201?s=80&v=4"},"commit":{"message":"Merge branch 'master' into issue-863","shortMessageHtmlLink":"Merge branch 'master' into issue-863"}},{"before":"a6b33ff39cd5d3fe63688bc85b2727c4014f3213","after":"7e04b93f7c05528350525d64bc7e5175636418d8","ref":"refs/heads/issue-863","pushedAt":"2024-04-10T17:22:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Add a minimal README to the Houdini package","shortMessageHtmlLink":"Add a minimal README to the Houdini package"}},{"before":"44e2251e4dd5c7571bfbafb16a6c3f1c46f35832","after":"25de4ac657044e9cdf38c6f3b3afc724f0a617cc","ref":"refs/heads/parse-exp-without-decimal","pushedAt":"2024-04-10T17:06:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Add unit tests for model parsing","shortMessageHtmlLink":"Add unit tests for model parsing"}},{"before":"01ca761d6124e9303e30cbb04791e8e4bf8d3d50","after":"44e2251e4dd5c7571bfbafb16a6c3f1c46f35832","ref":"refs/heads/parse-exp-without-decimal","pushedAt":"2024-04-09T22:45:54.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Merge branch 'master' into parse-exp-without-decimal","shortMessageHtmlLink":"Merge branch 'master' into parse-exp-without-decimal"}},{"before":null,"after":"a6b33ff39cd5d3fe63688bc85b2727c4014f3213","ref":"refs/heads/issue-863","pushedAt":"2024-04-09T17:56:14.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Add missing string interpolation\n\nThe fact that we didn't detect this earlier makes it clear that this\nfunctionality wasn't being tested. Unfortunately, it's not immediately\nclear to me how to write a test that would exercise the relevant code.","shortMessageHtmlLink":"Add missing string interpolation"}},{"before":"df9599bbcd2b66d7267c3e0ca8d9dc90b99948ec","after":"06e4b03536acbab43ddec500c330834bf7139e9e","ref":"refs/heads/allow-timelimit-and-rlimit","pushedAt":"2024-04-08T17:28:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Fix test that expected old behavior","shortMessageHtmlLink":"Fix test that expected old behavior"}},{"before":null,"after":"df9599bbcd2b66d7267c3e0ca8d9dc90b99948ec","ref":"refs/heads/allow-timelimit-and-rlimit","pushedAt":"2024-04-08T17:00:53.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Allow both timeLimit and rlimit together\n\nSometimes we want to set a resource limit _and_ a time limit, where the\ngoal of the former is to have deterministic bounds but the goal of the\nlatter is to ensure timely CI completion. In this case, a good value for\nthe time limit should be much larger than the time we would expect to be\nrequired to exceed the resource limit. This will ensure that execution\nis usually deterministic, but in the rare case where resource count and\ntime are far from each other it'll still guarantee reasonable\ntermination.","shortMessageHtmlLink":"Allow both timeLimit and rlimit together"}},{"before":"e2a462ca9433334de09957874dad110e965415ba","after":"01ca761d6124e9303e30cbb04791e8e4bf8d3d50","ref":"refs/heads/parse-exp-without-decimal","pushedAt":"2024-04-05T00:10:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Different approach to recognizing reals","shortMessageHtmlLink":"Different approach to recognizing reals"}},{"before":null,"after":"e2a462ca9433334de09957874dad110e965415ba","ref":"refs/heads/parse-exp-without-decimal","pushedAt":"2024-04-04T01:42:46.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Parse model values of the form 5e1 (no decimal)","shortMessageHtmlLink":"Parse model values of the form 5e1 (no decimal)"}},{"before":"29979dc812de2c8d19edc426c455b87b7c105d98","after":"fbafb12d0dd3623d7c98156b910118eb5479b047","ref":"refs/heads/basic-lean-auto","pushedAt":"2024-03-19T21:55:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Use `foreach` instead of `ForEach`","shortMessageHtmlLink":"Use <code>foreach</code> instead of <code>ForEach</code>"}},{"before":"dd8359fb813e9f91741b92960a3f56d52093bf7e","after":"29979dc812de2c8d19edc426c455b87b7c105d98","ref":"refs/heads/basic-lean-auto","pushedAt":"2024-03-19T21:00:15.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Allow `goto` to have no targets","shortMessageHtmlLink":"Allow <code>goto</code> to have no targets"}},{"before":"64a4b5a530490cbc9e26b1aa6eadfdfc597a3a12","after":"dba121cec59b0c96d5180fd81a7573e8932e7e3f","ref":"refs/heads/low-rlimit-fix","pushedAt":"2024-03-12T22:47:44.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Bump version","shortMessageHtmlLink":"Bump version"}},{"before":"9a2c57a8fc025f7e198cf66621f630e25b1129fb","after":"64a4b5a530490cbc9e26b1aa6eadfdfc597a3a12","ref":"refs/heads/low-rlimit-fix","pushedAt":"2024-03-12T20:09:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Add .expect file; bump version","shortMessageHtmlLink":"Add .expect file; bump version"}},{"before":null,"after":"9a2c57a8fc025f7e198cf66621f630e25b1129fb","ref":"refs/heads/low-rlimit-fix","pushedAt":"2024-03-12T19:59:48.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Fix crash on low rlimit","shortMessageHtmlLink":"Fix crash on low rlimit"}},{"before":"2f8b3a968a392fe67246faa9f5e39760208ee748","after":"dd8359fb813e9f91741b92960a3f56d52093bf7e","ref":"refs/heads/basic-lean-auto","pushedAt":"2024-03-07T23:54:38.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'upstream/master' into basic-lean-auto","shortMessageHtmlLink":"Merge remote-tracking branch 'upstream/master' into basic-lean-auto"}},{"before":"dcc1033f1aef46ebf927be5a3df1e4e6f1b017c4","after":"c050e197a7884864baff58895b7e81dc6ed8683a","ref":"refs/heads/fix-focus-crash-2","pushedAt":"2024-03-07T22:13:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"keyboardDrummer","name":"Remy Willems","path":"/keyboardDrummer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3121201?s=80&v=4"},"commit":{"message":"Increment patch number","shortMessageHtmlLink":"Increment patch number"}},{"before":null,"after":"dcc1033f1aef46ebf927be5a3df1e4e6f1b017c4","ref":"refs/heads/fix-focus-crash-2","pushedAt":"2024-03-07T21:52:42.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Reset predecessors before focusing\n\nThere are two calls to `FocusAndSplit` in Boogie. Before one, there was\nalready a call to `ResetPredecessors`, but not before the other. Now\nthey both work on an implementation where the `Predecessors` attributes\nhas been reset.","shortMessageHtmlLink":"Reset predecessors before focusing"}},{"before":null,"after":"47ecd5dcd83b3a39e8e1413f492977aa24967881","ref":"refs/heads/fix-focus-crash","pushedAt":"2024-03-07T00:28:22.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Fix map lookup error in focus computation","shortMessageHtmlLink":"Fix map lookup error in focus computation"}},{"before":"9d58eb54f04d625080b583fb0f6029cb275da992","after":"2f8b3a968a392fe67246faa9f5e39760208ee748","ref":"refs/heads/basic-lean-auto","pushedAt":"2024-03-06T19:53:58.000Z","pushType":"push","commitsCount":9,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Move use of passive program to a separate method","shortMessageHtmlLink":"Move use of passive program to a separate method"}},{"before":"ce2ff9dacea0c843849705b761eaf19f52d2c576","after":"0bbb1e7992bfba01c115636f4805661b2b28f96e","ref":"refs/heads/concurrent-split-coverage","pushedAt":"2024-02-19T16:49:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Revert \"Undo obsolete imports\"\n\nThis reverts commit fe61fb96ad3cf4784e1f4121dddafde8cac9295f.","shortMessageHtmlLink":"Revert \"Undo obsolete imports\""}},{"before":"fe61fb96ad3cf4784e1f4121dddafde8cac9295f","after":"ce2ff9dacea0c843849705b761eaf19f52d2c576","ref":"refs/heads/concurrent-split-coverage","pushedAt":"2024-02-19T16:46:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Revert \"Clone Split instead of using ConcurrentBag\"\n\nThis reverts commit 5de1b5fc1e30a5d67ad6c3b8e72fdd2fb3b771e5.","shortMessageHtmlLink":"Revert \"Clone Split instead of using ConcurrentBag\""}},{"before":"f1e5a59e97c955b4033ab8e4af435d7b8e3f4cb6","after":"fe61fb96ad3cf4784e1f4121dddafde8cac9295f","ref":"refs/heads/concurrent-split-coverage","pushedAt":"2024-02-15T23:32:48.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Undo obsolete imports","shortMessageHtmlLink":"Undo obsolete imports"}},{"before":"154fee435c645e1cf5ace0f98d87df1a6be7a0dd","after":"9d58eb54f04d625080b583fb0f6029cb275da992","ref":"refs/heads/basic-lean-auto","pushedAt":"2024-02-14T22:05:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Pin the version of lean-auto for reproducibility","shortMessageHtmlLink":"Pin the version of lean-auto for reproducibility"}},{"before":"bf46f9549356134bfda8d587d0d3740336f86f81","after":"154fee435c645e1cf5ace0f98d87df1a6be7a0dd","ref":"refs/heads/basic-lean-auto","pushedAt":"2024-02-14T19:30:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Ensure Lean dependencies are actually built","shortMessageHtmlLink":"Ensure Lean dependencies are actually built"}},{"before":"4fc941dda1a3dd7ee12e08388d07be669dc9d598","after":"bf46f9549356134bfda8d587d0d3740336f86f81","ref":"refs/heads/basic-lean-auto","pushedAt":"2024-02-14T19:25:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Change setup-lean action name","shortMessageHtmlLink":"Change setup-lean action name"}},{"before":"300ed902cce65e6a5658b20dc5a61cc65ccb30a4","after":"4fc941dda1a3dd7ee12e08388d07be669dc9d598","ref":"refs/heads/basic-lean-auto","pushedAt":"2024-02-14T19:24:30.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"atomb","name":"Aaron Tomb","path":"/atomb","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/24929?s=80&v=4"},"commit":{"message":"Fix Lean installation","shortMessageHtmlLink":"Fix Lean installation"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAENGvnYAA","startCursor":null,"endCursor":null}},"title":"Activity · atomb/boogie"}