{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":325845305,"defaultBranch":"master","name":"vscode-lean4","ownerLogin":"leanprover","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2020-12-31T17:26:54.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/7233018?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726126259.0","currentOid":""},"activityList":{"items":[{"before":"839b438ddd71c86a7b87cd1a5241254ed286d023","after":null,"ref":"refs/heads/mhuisi/leading-bang-completion","pushedAt":"2024-09-12T07:30:59.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"}},{"before":"cbd76b64783ce7168f1b4e9915d9f68ab10966fc","after":"33e54067d5fefcdf7f28e4993324fd486a53421c","ref":"refs/heads/master","pushedAt":"2024-09-12T07:30:57.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"fix: leading bang is a word separator (#527)\n\nFixes #526.","shortMessageHtmlLink":"fix: leading bang is a word separator (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2519595924\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/527\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/527/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/527\">#527</a>)"}},{"before":"1bdeb03eb3e4b1dfe244b2f05296c88055e428ad","after":"839b438ddd71c86a7b87cd1a5241254ed286d023","ref":"refs/heads/mhuisi/leading-bang-completion","pushedAt":"2024-09-11T12:20:17.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"fix: leading bang is a word separator","shortMessageHtmlLink":"fix: leading bang is a word separator"}},{"before":null,"after":"1bdeb03eb3e4b1dfe244b2f05296c88055e428ad","ref":"refs/heads/mhuisi/leading-bang-completion","pushedAt":"2024-09-11T12:11:16.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"fix: leading bang is a word separator","shortMessageHtmlLink":"fix: leading bang is a word separator"}},{"before":"d64bd911347faaa7145a09a86027923b49fed29f","after":"cbd76b64783ce7168f1b4e9915d9f68ab10966fc","ref":"refs/heads/master","pushedAt":"2024-09-10T07:45:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"Release 0.0.178","shortMessageHtmlLink":"Release 0.0.178"}},{"before":"981b0c1b7ab2174e98b1fc5a689d7c1a49458759","after":null,"ref":"refs/heads/mhuisi/remove-right-to-left-symbol","pushedAt":"2024-09-10T07:44:41.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"}},{"before":"63caac0fd014bcea5258fe617a00ae0db06478b1","after":"d64bd911347faaa7145a09a86027923b49fed29f","ref":"refs/heads/master","pushedAt":"2024-09-10T07:44:40.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"chore: remove rial symbol (#525)\n\nCloses #522.","shortMessageHtmlLink":"chore: remove rial symbol (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2515664668\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/525\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/525/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/525\">#525</a>)"}},{"before":null,"after":"981b0c1b7ab2174e98b1fc5a689d7c1a49458759","ref":"refs/heads/mhuisi/remove-right-to-left-symbol","pushedAt":"2024-09-10T07:42:36.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"chore: remove rial symbol","shortMessageHtmlLink":"chore: remove rial symbol"}},{"before":"ae40724f6141a839e9499d70ea45515eacdd29c0","after":"63caac0fd014bcea5258fe617a00ae0db06478b1","ref":"refs/heads/master","pushedAt":"2024-09-10T07:39:35.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"feat: add double parens abbreviations (#523)\n\nCorresponds to [[ and {{ -- they aren't used (yet) in Mathlib but would\r\npotentially be used for LaurentSeries notation.","shortMessageHtmlLink":"feat: add double parens abbreviations (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2514600393\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/523\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/523/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/523\">#523</a>)"}},{"before":"b4834e6c5a0ed419c4d314dd12427064c0ae11d1","after":"22682d87b6210811babc852bdba5c3b240a95bf6","ref":"refs/heads/update_upload-artifact","pushedAt":"2024-09-10T06:47:02.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"semorrison","name":"Kim Morrison","path":"/semorrison","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/477956?s=80&v=4"},"commit":{"message":"Merge branch 'master' into update_upload-artifact","shortMessageHtmlLink":"Merge branch 'master' into update_upload-artifact"}},{"before":"97d7d8c382d1549c18b66cd99ab4df0b6634c8f1","after":"ae40724f6141a839e9499d70ea45515eacdd29c0","ref":"refs/heads/master","pushedAt":"2024-09-10T06:45:40.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"semorrison","name":"Kim Morrison","path":"/semorrison","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/477956?s=80&v=4"},"commit":{"message":"chore: update actions/upload-artifact (#524)\n\nPer\r\nhttps://github.blog/changelog/2024-02-13-deprecation-notice-v1-and-v2-of-the-artifact-actions/.","shortMessageHtmlLink":"chore: update actions/upload-artifact (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2515535370\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/524\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/524/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/524\">#524</a>)"}},{"before":null,"after":"b4834e6c5a0ed419c4d314dd12427064c0ae11d1","ref":"refs/heads/update_upload-artifact","pushedAt":"2024-09-10T06:35:22.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"semorrison","name":"Kim Morrison","path":"/semorrison","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/477956?s=80&v=4"},"commit":{"message":"chore: update actions/upload-artifact","shortMessageHtmlLink":"chore: update actions/upload-artifact"}},{"before":"ab37327c087d9999f812ae4645bd41716306b31f","after":"97d7d8c382d1549c18b66cd99ab4df0b6634c8f1","ref":"refs/heads/master","pushedAt":"2024-08-28T12:14:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"Release 0.0.177","shortMessageHtmlLink":"Release 0.0.177"}},{"before":"ce4cadec9fc46eea4420d90313cfd2886f6d1c4f","after":null,"ref":"refs/heads/mhuisi/discoverability","pushedAt":"2024-08-28T12:13:27.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"}},{"before":"af6d1b1adaa927582a30a2bb0e46a849a45b544a","after":"ab37327c087d9999f812ae4645bd41716306b31f","ref":"refs/heads/master","pushedAt":"2024-08-28T12:13:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"chore: change extension display name (#521)\n\nThis should hopefully make it easier to find the Lean 4 extension when\r\nsearching for \"Lean\" (due to the way that the VS Code fuzzy search\r\nworks). This PR also adds a \"lean4\" keyword so that the extension can\r\nstill be found with the old identifier.","shortMessageHtmlLink":"chore: change extension display name (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2491604278\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/521\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/521/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/521\">#521</a>)"}},{"before":null,"after":"ce4cadec9fc46eea4420d90313cfd2886f6d1c4f","ref":"refs/heads/mhuisi/discoverability","pushedAt":"2024-08-28T09:46:26.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"chore: change extension display name","shortMessageHtmlLink":"chore: change extension display name"}},{"before":"93095f9ed971ac59019408942ac295b56e56807c","after":"af6d1b1adaa927582a30a2bb0e46a849a45b544a","ref":"refs/heads/master","pushedAt":"2024-08-27T08:20:29.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"doc: use emoji-variant for ❌️ (#519)\n\nBased on leanprover/lean4#5015, use emoji-variant selector for ❌️ across\r\nthe Lean universe.","shortMessageHtmlLink":"doc: use emoji-variant for ❌️ (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2487090209\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/519\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/519/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/519\">#519</a>)"}},{"before":"6c2a5e26490279c6366fcc3ae10da9e89054a413","after":null,"ref":"refs/heads/mhuisi/infoview-filter-button-issue","pushedAt":"2024-08-04T15:55:30.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Vtec234","name":"Wojciech Nawrocki","path":"/Vtec234","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/13901751?s=80&v=4"}},{"before":"e15359532db1a80a6915459dc619db46330c02db","after":"93095f9ed971ac59019408942ac295b56e56807c","ref":"refs/heads/master","pushedAt":"2024-08-04T15:55:27.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Vtec234","name":"Wojciech Nawrocki","path":"/Vtec234","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/13901751?s=80&v=4"},"commit":{"message":"fix: filter menu button collapsing goal state (#511)\n\nCloses #505.\r\n\r\n---------\r\n\r\nCo-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>","shortMessageHtmlLink":"fix: filter menu button collapsing goal state (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2431597409\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/511\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/511/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/511\">#511</a>)"}},{"before":"dc1f65a3c002a013699ed39451da696418ac21fb","after":"6c2a5e26490279c6366fcc3ae10da9e89054a413","ref":"refs/heads/mhuisi/infoview-filter-button-issue","pushedAt":"2024-07-30T11:45:26.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Vtec234","name":"Wojciech Nawrocki","path":"/Vtec234","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/13901751?s=80&v=4"},"commit":{"message":"refactor: handle events in <summary>","shortMessageHtmlLink":"refactor: handle events in &lt;summary&gt;"}},{"before":"73dcf3abe9a18cf4a4e38ee8bcbdb0b3014e192d","after":null,"ref":"refs/heads/mhuisi/initial-commit-fix","pushedAt":"2024-07-26T10:00:38.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"}},{"before":"0bab1db6be08083e3b41286627334bd2dd19dc75","after":"e15359532db1a80a6915459dc619db46330c02db","ref":"refs/heads/master","pushedAt":"2024-07-26T10:00:37.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"fix: initial commit not working on fresh Git install (#512)","shortMessageHtmlLink":"fix: initial commit not working on fresh Git install (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2431619848\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/512\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/512/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/512\">#512</a>)"}},{"before":"f6140552b779562cd43e70169d81b13e3a785f5f","after":"73dcf3abe9a18cf4a4e38ee8bcbdb0b3014e192d","ref":"refs/heads/mhuisi/initial-commit-fix","pushedAt":"2024-07-26T08:49:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"fix: properly set empty email","shortMessageHtmlLink":"fix: properly set empty email"}},{"before":"2ee405d8c8127282c3e562e91f77454435ddaaa3","after":"dc1f65a3c002a013699ed39451da696418ac21fb","ref":"refs/heads/mhuisi/infoview-filter-button-issue","pushedAt":"2024-07-26T07:45:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"fix: stop details click event from propagating","shortMessageHtmlLink":"fix: stop details click event from propagating"}},{"before":null,"after":"f6140552b779562cd43e70169d81b13e3a785f5f","ref":"refs/heads/mhuisi/initial-commit-fix","pushedAt":"2024-07-26T07:34:32.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"fix: initial commit not working on fresh Git install","shortMessageHtmlLink":"fix: initial commit not working on fresh Git install"}},{"before":null,"after":"2ee405d8c8127282c3e562e91f77454435ddaaa3","ref":"refs/heads/mhuisi/infoview-filter-button-issue","pushedAt":"2024-07-26T07:20:20.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"fix: filter menu button collapsing goal state","shortMessageHtmlLink":"fix: filter menu button collapsing goal state"}},{"before":"53c7b8d49e4a15d4159fae24994a2c61cd3d2f41","after":"0bab1db6be08083e3b41286627334bd2dd19dc75","ref":"refs/heads/master","pushedAt":"2024-07-23T07:40:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"Release 0.0.176","shortMessageHtmlLink":"Release 0.0.176"}},{"before":"ba21fcf26b9164a13aec0165789266a121608eb7","after":null,"ref":"refs/heads/mhuisi/download-project-suggestions","pushedAt":"2024-07-23T07:39:24.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"}},{"before":"adcff5ef5d63c1114f7123eab67a153be6e9657e","after":"53c7b8d49e4a15d4159fae24994a2c61cd3d2f41","ref":"refs/heads/master","pushedAt":"2024-07-23T07:39:22.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"feat: download project presets (#507)","shortMessageHtmlLink":"feat: download project presets (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2422676396\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/vscode-lean4/issues/507\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/vscode-lean4/pull/507/hovercard\" href=\"https://github.com/leanprover/vscode-lean4/pull/507\">#507</a>)"}},{"before":"96eb1f24bb356d10202ab6d451eca3389dcf7292","after":"ba21fcf26b9164a13aec0165789266a121608eb7","ref":"refs/heads/mhuisi/download-project-suggestions","pushedAt":"2024-07-23T07:35:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mhuisi","name":"Marc Huisinga","path":"/mhuisi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10852073?s=80&v=4"},"commit":{"message":"doc: minor manual update","shortMessageHtmlLink":"doc: minor manual update"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xMlQwNzozMDo1OS4wMDAwMDBazwAAAAS0Dz_I","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xMlQwNzozMDo1OS4wMDAwMDBazwAAAAS0Dz_I","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNy0yM1QwNzozNTo1OC4wMDAwMDBazwAAAASGjlKZ"}},"title":"Activity · leanprover/vscode-lean4"}