{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":671237247,"defaultBranch":"master","name":"busycoq","ownerLogin":"meithecatte","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2023-07-26T21:30:12.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/23580910?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1709561587.0","currentOid":""},"activityList":{"items":[{"before":"166447fd21336ff24a105c617c769b74410e3300","after":"ce2f22e1616632924622016d9cbb8ba0847b2c6a","ref":"refs/heads/master","pushedAt":"2024-07-22T12:08:23.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Merge pull request #4 from int-y1/bb33-494\n\nProve BB(3,3) id 494 doesn't halt","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2407837666\" data-permission-text=\"Title is private\" data-url=\"https://github.com/meithecatte/busycoq/issues/4\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/meithecatte/busycoq/pull/4/hovercard\" href=\"https://github.com/meithecatte/busycoq/pull/4\">#4</a> from int-y1/bb33-494"}},{"before":"af8f82298ecf312b3fa16dd12ac1644b9f128e18","after":"166447fd21336ff24a105c617c769b74410e3300","ref":"refs/heads/master","pushedAt":"2024-05-02T23:00:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Update timings\n\nThey are consistently 5s lower after a rustc update","shortMessageHtmlLink":"Update timings"}},{"before":"608ee6cb21dbeb2fc46346ee73d21c9353fb860b","after":"af8f82298ecf312b3fa16dd12ac1644b9f128e18","ref":"refs/heads/master","pushedAt":"2024-05-02T22:45:54.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"update dependencies","shortMessageHtmlLink":"update dependencies"}},{"before":"e09d3e48b0c8e8e9eb709a631b4afb3a70c0677c","after":"608ee6cb21dbeb2fc46346ee73d21c9353fb860b","ref":"refs/heads/master","pushedAt":"2024-04-22T20:34:48.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"bouncers: simplify control flow in find_progressions","shortMessageHtmlLink":"bouncers: simplify control flow in find_progressions"}},{"before":"98993849e3e3d38d0ae29cbe2e74dd04b458abe1","after":"e09d3e48b0c8e8e9eb709a631b4afb3a70c0677c","ref":"refs/heads/master","pushedAt":"2024-04-22T19:30:50.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"README: update results","shortMessageHtmlLink":"README: update results"}},{"before":"f65801efb47802b39ab36598e8dd1874d654c55a","after":"98993849e3e3d38d0ae29cbe2e74dd04b458abe1","ref":"refs/heads/master","pushedAt":"2024-04-22T16:39:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"README: update results","shortMessageHtmlLink":"README: update results"}},{"before":"8b9f2ac90e73a69af272e9bc6804f8b1257f9a36","after":"f65801efb47802b39ab36598e8dd1874d654c55a","ref":"refs/heads/master","pushedAt":"2024-04-22T16:22:20.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"bouncers: Use a greedy tape splitting algorithm by default","shortMessageHtmlLink":"bouncers: Use a greedy tape splitting algorithm by default"}},{"before":"9f7d51e99c207667d51c67073ff9fd8a5da23fd6","after":"8b9f2ac90e73a69af272e9bc6804f8b1257f9a36","ref":"refs/heads/master","pushedAt":"2024-04-22T16:10:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"bouncers: Use a greedy tape splitting algorithm by default","shortMessageHtmlLink":"bouncers: Use a greedy tape splitting algorithm by default"}},{"before":"8baf94bc657333788fa1044b13a2ffa31e0c148f","after":"9f7d51e99c207667d51c67073ff9fd8a5da23fd6","ref":"refs/heads/master","pushedAt":"2024-04-22T15:45:49.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"memo: avoid using Cell\n\nTurns out this is not actually necessary. Improves the performance by\nabout 20%.","shortMessageHtmlLink":"memo: avoid using Cell"}},{"before":"e60b77b290c157d6dd9d6ad2a09602393bc433d9","after":"8baf94bc657333788fa1044b13a2ffa31e0c148f","ref":"refs/heads/master","pushedAt":"2024-04-22T14:07:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"memo: avoid using Cell\n\nTurns out this is not actually necessary. Improves the performance by\nabout 20%.","shortMessageHtmlLink":"memo: avoid using Cell"}},{"before":"21fa66fee84455dc8a131d5618983e5d3defa5d1","after":"e60b77b290c157d6dd9d6ad2a09602393bc433d9","ref":"refs/heads/master","pushedAt":"2024-04-16T18:37:08.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Switch to a released version of itertools\n\nThe commit we need has ended up in a release.","shortMessageHtmlLink":"Switch to a released version of itertools"}},{"before":"faece083f37702b4ff09834e56ac888f7df0a93c","after":"21fa66fee84455dc8a131d5618983e5d3defa5d1","ref":"refs/heads/master","pushedAt":"2024-04-07T21:04:52.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"enumerate: define halting-equivalence","shortMessageHtmlLink":"enumerate: define halting-equivalence"}},{"before":"912afa5230408fb8fc52d67e51855ea0a82a89c7","after":"faece083f37702b4ff09834e56ac888f7df0a93c","ref":"refs/heads/master","pushedAt":"2024-04-01T14:40:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Add the cubic-finned machines to the README","shortMessageHtmlLink":"Add the cubic-finned machines to the README"}},{"before":"f93915a5a269169dcbc0f003f9415f2bb12d2a14","after":"912afa5230408fb8fc52d67e51855ea0a82a89c7","ref":"refs/heads/master","pushedAt":"2024-04-01T14:33:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Prove cubic-finned #3\n\nAlso modify existing proofs to avoid using a single variable in\ntwo exponents. Their being necessary was an artifact of a shortcoming\nof a previous version of the `finned` tactic – and in the current proof,\nit is necessary to avoid them instead. Modify all the other proofs for\nconsistency.","shortMessageHtmlLink":"Prove cubic-finned <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2267078162\" data-permission-text=\"Title is private\" data-url=\"https://github.com/meithecatte/busycoq/issues/3\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/meithecatte/busycoq/pull/3/hovercard\" href=\"https://github.com/meithecatte/busycoq/pull/3\">#3</a>"}},{"before":"e84cdfcac8f8c5ca6f6e4c8da8f16734cbb7a344","after":"f93915a5a269169dcbc0f003f9415f2bb12d2a14","ref":"refs/heads/master","pushedAt":"2024-04-01T13:50:20.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Contribute Finned4.v (same as Finned5, basically).","shortMessageHtmlLink":"Contribute Finned4.v (same as Finned5, basically)."}},{"before":"e1e6219eef2f6dbc8612f6276e4837e685ceefdc","after":"e84cdfcac8f8c5ca6f6e4c8da8f16734cbb7a344","ref":"refs/heads/master","pushedAt":"2024-04-01T13:49:20.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Merge pull request #2 from UncombedCoconut/master\n\nContribute Finned4.v (same as Finned5, basically).","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2218303727\" data-permission-text=\"Title is private\" data-url=\"https://github.com/meithecatte/busycoq/issues/2\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/meithecatte/busycoq/pull/2/hovercard\" href=\"https://github.com/meithecatte/busycoq/pull/2\">#2</a> from UncombedCoconut/master"}},{"before":"482f41535364d8bbb9823559ae0ddced204131a6","after":"e1e6219eef2f6dbc8612f6276e4837e685ceefdc","ref":"refs/heads/master","pushedAt":"2024-04-01T13:48:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Remove unnecessary import of Lia\n\nIt was only there for debugging","shortMessageHtmlLink":"Remove unnecessary import of Lia"}},{"before":"1932207c5dd54080f14f94f636c07c366c3da2e1","after":"482f41535364d8bbb9823559ae0ddced204131a6","ref":"refs/heads/master","pushedAt":"2024-04-01T13:35:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Prove cubic-finned #2","shortMessageHtmlLink":"Prove cubic-finned <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2218303727\" data-permission-text=\"Title is private\" data-url=\"https://github.com/meithecatte/busycoq/issues/2\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/meithecatte/busycoq/pull/2/hovercard\" href=\"https://github.com/meithecatte/busycoq/pull/2\">#2</a>"}},{"before":"ecbeb4561ef147f71ea8e92e9a12364c5815c28f","after":"1932207c5dd54080f14f94f636c07c366c3da2e1","ref":"refs/heads/master","pushedAt":"2024-04-01T11:39:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"BackwardsReasoning: fix proof\n\nAn unrelated change caused Coq to pick a different name, and\nI accidentally used the fragile name of the variable instead\nof the match found by Ltac match.","shortMessageHtmlLink":"BackwardsReasoning: fix proof"}},{"before":"795816bd1c14850b7f19cc780ceaeee1f589199c","after":"ecbeb4561ef147f71ea8e92e9a12364c5815c28f","ref":"refs/heads/master","pushedAt":"2024-03-31T23:25:56.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Prove cubic-finned #1","shortMessageHtmlLink":"Prove cubic-finned <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2103887508\" data-permission-text=\"Title is private\" data-url=\"https://github.com/meithecatte/busycoq/issues/1\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/meithecatte/busycoq/pull/1/hovercard\" href=\"https://github.com/meithecatte/busycoq/pull/1\">#1</a>"}},{"before":"0f627b4b41fe35be65680232651fef16b20df113","after":"795816bd1c14850b7f19cc780ceaeee1f589199c","ref":"refs/heads/master","pushedAt":"2024-03-28T10:42:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Finned5: solve the closure condition automatically","shortMessageHtmlLink":"Finned5: solve the closure condition automatically"}},{"before":"1846cb279b6410de12fe311cf85b7149e9e97118","after":"0f627b4b41fe35be65680232651fef16b20df113","ref":"refs/heads/master","pushedAt":"2024-03-26T14:07:44.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Prove cubic-finned #5","shortMessageHtmlLink":"Prove cubic-finned #5"}},{"before":"698cd0e493da25d5b946a504d74cfdcc982ecad7","after":"1846cb279b6410de12fe311cf85b7149e9e97118","ref":"refs/heads/master","pushedAt":"2024-03-26T14:02:17.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Prove cubic-finned #5","shortMessageHtmlLink":"Prove cubic-finned #5"}},{"before":"1c23203761602c199a7ac5ea6f7947fb80851d93","after":"698cd0e493da25d5b946a504d74cfdcc982ecad7","ref":"refs/heads/master","pushedAt":"2024-03-26T13:52:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Prove cubic-finned #5","shortMessageHtmlLink":"Prove cubic-finned #5"}},{"before":"83000222093f9f5ba85f70ee937133124206a9af","after":"1c23203761602c199a7ac5ea6f7947fb80851d93","ref":"refs/heads/master","pushedAt":"2024-03-26T08:53:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Use progress_nonhalt_{simple,cond} where possible","shortMessageHtmlLink":"Use progress_nonhalt_{simple,cond} where possible"}},{"before":"f6fb6a690a1085e9c42546b12ec461647bf15f5d","after":"83000222093f9f5ba85f70ee937133124206a9af","ref":"refs/heads/master","pushedAt":"2024-03-26T08:21:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"TM: add progress_nonhalt_cond","shortMessageHtmlLink":"TM: add progress_nonhalt_cond"}},{"before":"e38873ba6970c52358627ffdc52d03957570f800","after":"f6fb6a690a1085e9c42546b12ec461647bf15f5d","ref":"refs/heads/master","pushedAt":"2024-03-22T19:41:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Enumerate: is_child_of and properties","shortMessageHtmlLink":"Enumerate: is_child_of and properties"}},{"before":"2a5ae4b96789dae5e673a7a452f0dea88f927c78","after":"e38873ba6970c52358627ffdc52d03957570f800","ref":"refs/heads/master","pushedAt":"2024-03-20T22:00:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Simplify the div2 support for zify","shortMessageHtmlLink":"Simplify the div2 support for zify"}},{"before":"92bb08d09fc3c03a3f9b9ba6378cd5f495dce49d","after":"2a5ae4b96789dae5e673a7a452f0dea88f927c78","ref":"refs/heads/master","pushedAt":"2024-03-20T19:11:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Teach lia about div2","shortMessageHtmlLink":"Teach lia about div2"}},{"before":"5d24eb41d48dfa2fd17ba529988f72f44f0117dd","after":"92bb08d09fc3c03a3f9b9ba6378cd5f495dce49d","ref":"refs/heads/master","pushedAt":"2024-03-20T16:59:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"meithecatte","name":"Maja Kądziołka","path":"/meithecatte","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/23580910?s=80&v=4"},"commit":{"message":"Enumerate: calculate actual max zvisits for a specific TM","shortMessageHtmlLink":"Enumerate: calculate actual max zvisits for a specific TM"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNy0yMlQxMjowODoyMy4wMDAwMDBazwAAAASFusFn","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNy0yMlQxMjowODoyMy4wMDAwMDBazwAAAASFusFn","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wMy0yMFQxNjo1OToxNy4wMDAwMDBazwAAAAQa6ZHI"}},"title":"Activity · meithecatte/busycoq"}