{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":184748176,"defaultBranch":"master","name":"lean4","ownerLogin":"Kha","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2019-05-03T12:02:10.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/109126?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1719244511.0","currentOid":""},"activityList":{"items":[{"before":"02a6b9640e2c6c4f5ea3a536c86619bc3607b811","after":"928cfaedfbd5f84aa14187bb0894177d2594bc63","ref":"refs/heads/tac-term-tac2","pushedAt":"2024-06-24T15:59:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"test doc","shortMessageHtmlLink":"test doc"}},{"before":null,"after":"02a6b9640e2c6c4f5ea3a536c86619bc3607b811","ref":"refs/heads/tac-term-tac2","pushedAt":"2024-06-24T15:55:11.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix: tactics in terms in tactic combinators breaking incrementality","shortMessageHtmlLink":"fix: tactics in terms in tactic combinators breaking incrementality"}},{"before":"aa7dc1c3c27604d5f82547c390eb72317d993f6b","after":"3854949a1c605dc147e64f189262fcef2fcb8a8e","ref":"refs/heads/import-case","pushedAt":"2024-06-23T14:43:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix","shortMessageHtmlLink":"fix"}},{"before":null,"after":"aa7dc1c3c27604d5f82547c390eb72317d993f6b","ref":"refs/heads/import-case","pushedAt":"2024-06-23T09:22:50.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix: make import resolution case-sensitive on all platforms","shortMessageHtmlLink":"fix: make import resolution case-sensitive on all platforms"}},{"before":"3345a74ad16149dfa57320ca041b1582e095b1ae","after":"a08eebd14b5e772fdad4f4d8494e09af73bf1123","ref":"refs/heads/het-snaps-cmdline","pushedAt":"2024-06-22T10:33:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"try marking environment persistent after each command","shortMessageHtmlLink":"try marking environment persistent after each command"}},{"before":"2ea22dd77b24279cb8625fea6106ba2bc46bb176","after":null,"ref":"refs/heads/unboxed-init","pushedAt":"2024-06-20T10:51:40.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"}},{"before":null,"after":"2ea22dd77b24279cb8625fea6106ba2bc46bb176","ref":"refs/heads/unboxed-init","pushedAt":"2024-06-20T09:54:27.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix: missing unboxing in interpreter when loading initialized value","shortMessageHtmlLink":"fix: missing unboxing in interpreter when loading initialized value"}},{"before":"726767b1212e31538aebe343906ea0ff0f30e30d","after":"018084925b1762c66d7e50bf06f7b1a58d224139","ref":"refs/heads/std","pushedAt":"2024-06-19T13:15:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix Nix","shortMessageHtmlLink":"fix Nix"}},{"before":"91272a29f780f0721be418dc80ceb5d2b0654d0e","after":"726767b1212e31538aebe343906ea0ff0f30e30d","ref":"refs/heads/std","pushedAt":"2024-06-19T12:35:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix Nix","shortMessageHtmlLink":"fix Nix"}},{"before":"fffac07b9822d8b8a605dfb6137b253785f94ee2","after":"91272a29f780f0721be418dc80ceb5d2b0654d0e","ref":"refs/heads/std","pushedAt":"2024-06-19T12:09:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix Nix","shortMessageHtmlLink":"fix Nix"}},{"before":"ab7df0b0619f7fd81649f9a1d0a9caa9b45f5b2f","after":"fffac07b9822d8b8a605dfb6137b253785f94ee2","ref":"refs/heads/std","pushedAt":"2024-06-19T12:01:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"copyright","shortMessageHtmlLink":"copyright"}},{"before":"dae132c6d3793f359fbc730b25e4ed66b557a2c6","after":"ab7df0b0619f7fd81649f9a1d0a9caa9b45f5b2f","ref":"refs/heads/std","pushedAt":"2024-06-19T11:59:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"Std/","shortMessageHtmlLink":"Std/"}},{"before":"d92c863fb03761fe5a07d225dd48c7e6a7a0c10c","after":"dae132c6d3793f359fbc730b25e4ed66b557a2c6","ref":"refs/heads/std","pushedAt":"2024-06-19T11:53:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"Std.lean","shortMessageHtmlLink":"Std.lean"}},{"before":null,"after":"d92c863fb03761fe5a07d225dd48c7e6a7a0c10c","ref":"refs/heads/std","pushedAt":"2024-06-19T11:42:21.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"feat: introduce `Std`","shortMessageHtmlLink":"feat: introduce <code>Std</code>"}},{"before":"8fbbb3008cce4abc092700fb9d38f7f1f2475c0d","after":"45459a9ccc1e5baf410c06872a57ad53f5cc6a19","ref":"refs/heads/incr-next-if","pushedAt":"2024-06-18T12:27:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"test: `open Classical` leak","shortMessageHtmlLink":"test: <code>open Classical</code> leak"}},{"before":"d7a16852e932c3e7a59c4f4f62e5a993733c7847","after":"019b0c88ff091da84ef42820d35e4aabfb010dc3","ref":"refs/heads/lake-in-cmake","pushedAt":"2024-06-17T10:58:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix Windows","shortMessageHtmlLink":"fix Windows"}},{"before":"c4209f36805347505a0633553f8026f07affc4fa","after":"d7a16852e932c3e7a59c4f4f62e5a993733c7847","ref":"refs/heads/lake-in-cmake","pushedAt":"2024-06-16T19:48:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"missing ROOT replacement","shortMessageHtmlLink":"missing ROOT replacement"}},{"before":"c9e84810153bff4377f4f13132a8d73f32abebaf","after":"c4209f36805347505a0633553f8026f07affc4fa","ref":"refs/heads/lake-in-cmake","pushedAt":"2024-06-16T19:36:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix standalone build","shortMessageHtmlLink":"fix standalone build"}},{"before":"b4a7c7b641f0b74ca83a2254ec17f2e8be9d0c40","after":"c9e84810153bff4377f4f13132a8d73f32abebaf","ref":"refs/heads/lake-in-cmake","pushedAt":"2024-06-16T19:26:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"ah","shortMessageHtmlLink":"ah"}},{"before":null,"after":"b4a7c7b641f0b74ca83a2254ec17f2e8be9d0c40","ref":"refs/heads/lake-in-cmake","pushedAt":"2024-06-16T16:32:41.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"chore: USE_LAKE: integrate into CMake","shortMessageHtmlLink":"chore: USE_LAKE: integrate into CMake"}},{"before":null,"after":"aa161a63eead6d59330159221d23e481eccec733","ref":"refs/heads/parallel-linting","pushedAt":"2024-06-14T14:30:31.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"feat: parallel linting","shortMessageHtmlLink":"feat: parallel linting"}},{"before":null,"after":"8fbbb3008cce4abc092700fb9d38f7f1f2475c0d","ref":"refs/heads/incr-next-if","pushedAt":"2024-06-14T10:16:10.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"feat: incremental `next` and tactic `if`","shortMessageHtmlLink":"feat: incremental <code>next</code> and tactic <code>if</code>"}},{"before":"b25d74c82bb0e52ac59667fac747b04e836265b3","after":"e1c5206284adfa8ebcae57c8c49fc0d997a9b6cb","ref":"refs/heads/unknown-pkg","pushedAt":"2024-06-13T15:38:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tydeu","name":"Mac Malone","path":"/tydeu","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9020483?s=80&v=4"},"commit":{"message":"chore: lake: update `tests/badImport`","shortMessageHtmlLink":"chore: lake: update <code>tests/badImport</code>"}},{"before":"2a5a5c5c9d23f4b3ec545f60ebe3591807639fd7","after":"b25d74c82bb0e52ac59667fac747b04e836265b3","ref":"refs/heads/unknown-pkg","pushedAt":"2024-06-13T11:51:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"Update src/Lean/Util/Path.lean\n\nCo-authored-by: Mac Malone <tydeu@hatpress.net>","shortMessageHtmlLink":"Update src/Lean/Util/Path.lean"}},{"before":"a125555d238b0496eaab4df3f02df46230a63428","after":"00fb88c6e2f567753b105c6a995ed5fc31d147a7","ref":"refs/heads/fix-unrebased-prs","pushedAt":"2024-06-13T09:42:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix","shortMessageHtmlLink":"fix"}},{"before":"89d8efbbd7afd92b5a6db1b1dd8d152263acd8ea","after":"a125555d238b0496eaab4df3f02df46230a63428","ref":"refs/heads/fix-unrebased-prs","pushedAt":"2024-06-13T09:40:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix","shortMessageHtmlLink":"fix"}},{"before":"0c6397ca6e5e533e3cb6813ef2ff3907127c513c","after":"89d8efbbd7afd92b5a6db1b1dd8d152263acd8ea","ref":"refs/heads/fix-unrebased-prs","pushedAt":"2024-06-13T09:39:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix","shortMessageHtmlLink":"fix"}},{"before":"99425565a3aa8e1e55e64a3b7682432203c20f57","after":"0c6397ca6e5e533e3cb6813ef2ff3907127c513c","ref":"refs/heads/fix-unrebased-prs","pushedAt":"2024-06-13T09:36:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix","shortMessageHtmlLink":"fix"}},{"before":"ec2beadde297334352a660f269933831483821e4","after":"99425565a3aa8e1e55e64a3b7682432203c20f57","ref":"refs/heads/fix-unrebased-prs","pushedAt":"2024-06-13T09:28:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix","shortMessageHtmlLink":"fix"}},{"before":"eadf3c4a3de7c1666a5a6b4f7ccbe8c375981a8f","after":"ec2beadde297334352a660f269933831483821e4","ref":"refs/heads/fix-unrebased-prs","pushedAt":"2024-06-13T09:18:11.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix","shortMessageHtmlLink":"fix"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEbbVE8wA","startCursor":null,"endCursor":null}},"title":"Activity · Kha/lean4"}