{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":325645198,"defaultBranch":"main","name":"lean.nvim","ownerLogin":"Julian","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2020-12-30T20:48:01.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/329822?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1717165927.0","currentOid":""},"activityList":{"items":[{"before":"625fc67771334ca9e45f0c8437a6c5ca90a515b5","after":"6781f42f1cbf574f217a6a1948aa0f36812df1e8","ref":"refs/heads/main","pushedAt":"2024-06-01T13:00:55.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"vim.loop is also deprecated.","shortMessageHtmlLink":"vim.loop is also deprecated."}},{"before":"3b88d421f29f199da35db94fb3a4c870baaf72df","after":null,"ref":"refs/heads/pre-commit-ci-update-config","pushedAt":"2024-05-31T14:32:07.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"}},{"before":"91377b346a78ad2f5cfe8c65dc5126a7e1c538e8","after":"625fc67771334ca9e45f0c8437a6c5ca90a515b5","ref":"refs/heads/main","pushedAt":"2024-05-31T14:32:06.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Merge pull request #339 from Julian/pre-commit-ci-update-config\n\n[pre-commit.ci] pre-commit autoupdate","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2319567430\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Julian/lean.nvim/issues/339\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Julian/lean.nvim/pull/339/hovercard\" href=\"https://github.com/Julian/lean.nvim/pull/339\">#339</a> from Julian/pre-commit-ci-update-config"}},{"before":"8473b85f7e5819293b705036508fdfa653671518","after":"91377b346a78ad2f5cfe8c65dc5126a7e1c538e8","ref":"refs/heads/main","pushedAt":"2024-05-28T06:11:49.000Z","pushType":"pr_merge","commitsCount":6,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Merge pull request #337 from MithicSpirit/infoview-opts\n\nfeat(infoview): more buffer options","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2317251689\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Julian/lean.nvim/issues/337\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Julian/lean.nvim/pull/337/hovercard\" href=\"https://github.com/Julian/lean.nvim/pull/337\">#337</a> from MithicSpirit/infoview-opts"}},{"before":null,"after":"3b88d421f29f199da35db94fb3a4c870baaf72df","ref":"refs/heads/pre-commit-ci-update-config","pushedAt":"2024-05-27T17:37:16.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"pre-commit-ci[bot]","name":null,"path":"/apps/pre-commit-ci","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/68672?s=80&v=4"},"commit":{"message":"[pre-commit.ci] pre-commit autoupdate\n\nupdates:\n- [github.com/lunarmodules/luacheck: v1.1.2 → v1.2.0](https://github.com/lunarmodules/luacheck/compare/v1.1.2...v1.2.0)","shortMessageHtmlLink":"[pre-commit.ci] pre-commit autoupdate"}},{"before":"9624068eae6930b79ce213ff6072277ccbf13c42","after":"8473b85f7e5819293b705036508fdfa653671518","ref":"refs/heads/main","pushedAt":"2024-05-26T14:17:07.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Merge pull request #338 from MithicSpirit/nvim-lsp-setup\n\nfix(abbr): don't stop abbr on `{}()`","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2317257715\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Julian/lean.nvim/issues/338\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Julian/lean.nvim/pull/338/hovercard\" href=\"https://github.com/Julian/lean.nvim/pull/338\">#338</a> from MithicSpirit/nvim-lsp-setup"}},{"before":"59de4adaee51271ab74adad4e2c1f31368e6e1bc","after":"9624068eae6930b79ce213ff6072277ccbf13c42","ref":"refs/heads/main","pushedAt":"2024-05-26T14:13:56.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Fix whatever shared state has broken the tests in 0.10.\n\nI really don't understand what's changed here.\n\nThe only thing this does is essentially creates a new buffer for some of\nthe pin_spec tests (with the same contents as previous). All the rest of\nthe diff is whitespace noise.\n\nBut some poking around didn't really show me what was happening, and\ngiven that I don't observe any issue when manually replicating the test,\nI'm just going with this for now.","shortMessageHtmlLink":"Fix whatever shared state has broken the tests in 0.10."}},{"before":"bfef3cb5df05b15c29240425ad1686bbf142b776","after":"59de4adaee51271ab74adad4e2c1f31368e6e1bc","ref":"refs/heads/main","pushedAt":"2024-05-22T10:28:23.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Merge pull request #336 from mattrobball/main\n\nchore: adapt to changes in client fields for `vim.lsp.client`","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2310148649\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Julian/lean.nvim/issues/336\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Julian/lean.nvim/pull/336/hovercard\" href=\"https://github.com/Julian/lean.nvim/pull/336\">#336</a> from mattrobball/main"}},{"before":"2828898ad6f6ac6c1c9f404d72bd3d56546b0c72","after":"bfef3cb5df05b15c29240425ad1686bbf142b776","ref":"refs/heads/main","pushedAt":"2024-05-17T07:52:55.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Update the Lean version for our sample project.","shortMessageHtmlLink":"Update the Lean version for our sample project."}},{"before":"023cde8c59ecd02b7478587737450a88041d5856","after":"2828898ad6f6ac6c1c9f404d72bd3d56546b0c72","ref":"refs/heads/main","pushedAt":"2024-04-09T21:01:12.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Merge pull request #335 from Julian/pre-commit-ci-update-config\n\n[pre-commit.ci] pre-commit autoupdate","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2231771825\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Julian/lean.nvim/issues/335\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Julian/lean.nvim/pull/335/hovercard\" href=\"https://github.com/Julian/lean.nvim/pull/335\">#335</a> from Julian/pre-commit-ci-update-config"}},{"before":"c73c4fab411bc35e420dd591c125ad9b05b4be23","after":null,"ref":"refs/heads/pre-commit-ci-update-config","pushedAt":"2024-04-09T21:01:12.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"}},{"before":"ceeea9cf6baa890eebf2a45d8fa2f69c7d080c7f","after":"c73c4fab411bc35e420dd591c125ad9b05b4be23","ref":"refs/heads/pre-commit-ci-update-config","pushedAt":"2024-04-08T17:48:40.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"pre-commit-ci[bot]","name":null,"path":"/apps/pre-commit-ci","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/68672?s=80&v=4"},"commit":{"message":"[pre-commit.ci] pre-commit autoupdate\n\nupdates:\n- [github.com/pre-commit/pre-commit-hooks: v4.5.0 → v4.6.0](https://github.com/pre-commit/pre-commit-hooks/compare/v4.5.0...v4.6.0)","shortMessageHtmlLink":"[pre-commit.ci] pre-commit autoupdate"}},{"before":"d3dfd0edc861b44044194747b81bb9fae4460f76","after":"023cde8c59ecd02b7478587737450a88041d5856","ref":"refs/heads/main","pushedAt":"2024-03-29T16:59:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Drop some old legacy code.\n\nThis was a polyfill for changes in 0.7 or 0.6 even.","shortMessageHtmlLink":"Drop some old legacy code."}},{"before":"1b35a32538a773a7e79cf52740f485528b3ecb8f","after":"d3dfd0edc861b44044194747b81bb9fae4460f76","ref":"refs/heads/main","pushedAt":"2024-03-29T15:23:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Minor internal refactor removing non-table usages of vim.opt.\n\nIt's due for upstream removal eventually, in favor of vim.wo/vim.bo.\n\nSee e.g. neovim/neovim#20107","shortMessageHtmlLink":"Minor internal refactor removing non-table usages of vim.opt."}},{"before":"2dc102db03e83afc473c80a7d962974841e13b54","after":"1b35a32538a773a7e79cf52740f485528b3ecb8f","ref":"refs/heads/main","pushedAt":"2024-03-20T00:08:24.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Merge pull request #334 from mars0i/e21nomod\n\nAdded warning about E21 error due to nomodifiable.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2196070870\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Julian/lean.nvim/issues/334\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Julian/lean.nvim/pull/334/hovercard\" href=\"https://github.com/Julian/lean.nvim/pull/334\">#334</a> from mars0i/e21nomod"}},{"before":"ee5e4fecfb0f97eb2e779e011a310fffa7d2429c","after":null,"ref":"refs/heads/dependabot/github_actions/extractions/setup-just-2","pushedAt":"2024-03-04T11:47:28.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"}},{"before":"525da718ad7e91d3d1dffda6dc2703d153987e20","after":"2dc102db03e83afc473c80a7d962974841e13b54","ref":"refs/heads/main","pushedAt":"2024-03-04T11:47:27.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Merge pull request #331 from Julian/dependabot/github_actions/extractions/setup-just-2\n\nBump extractions/setup-just from 1 to 2","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2166045984\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Julian/lean.nvim/issues/331\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Julian/lean.nvim/pull/331/hovercard\" href=\"https://github.com/Julian/lean.nvim/pull/331\">#331</a> from Julian/dependabot/github_actions/extract…"}},{"before":null,"after":"ee5e4fecfb0f97eb2e779e011a310fffa7d2429c","ref":"refs/heads/dependabot/github_actions/extractions/setup-just-2","pushedAt":"2024-03-04T06:31:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"dependabot[bot]","name":null,"path":"/apps/dependabot","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/29110?s=80&v=4"},"commit":{"message":"Bump extractions/setup-just from 1 to 2\n\nBumps [extractions/setup-just](https://github.com/extractions/setup-just) from 1 to 2.\n- [Release notes](https://github.com/extractions/setup-just/releases)\n- [Commits](https://github.com/extractions/setup-just/compare/v1...v2)\n\n---\nupdated-dependencies:\n- dependency-name: extractions/setup-just\n  dependency-type: direct:production\n  update-type: version-update:semver-major\n...\n\nSigned-off-by: dependabot[bot] <support@github.com>","shortMessageHtmlLink":"Bump extractions/setup-just from 1 to 2"}},{"before":"06a3a7c1ff14241abd7da581fcde8e75a143209b","after":"525da718ad7e91d3d1dffda6dc2703d153987e20","ref":"refs/heads/main","pushedAt":"2024-03-04T00:47:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Revert the Lean 3 test change.","shortMessageHtmlLink":"Revert the Lean 3 test change."}},{"before":"c3e0893d6255c320e124c0f1a3d6cb62cb5e94c8","after":"06a3a7c1ff14241abd7da581fcde8e75a143209b","ref":"refs/heads/main","pushedAt":"2024-03-04T00:40:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Whoops, vim.iter is 0.10-only.","shortMessageHtmlLink":"Whoops, vim.iter is 0.10-only."}},{"before":"7c8d013045ed730d9488d08feb3292de0d12debe","after":"c3e0893d6255c320e124c0f1a3d6cb62cb5e94c8","ref":"refs/heads/main","pushedAt":"2024-03-04T00:31:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Only show a goal count when there's more than one goal.","shortMessageHtmlLink":"Only show a goal count when there's more than one goal."}},{"before":"3f6a36cfaede4502daa7da51bd08d2c1e2909071","after":"7c8d013045ed730d9488d08feb3292de0d12debe","ref":"refs/heads/main","pushedAt":"2024-03-03T23:55:15.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Point out that we apparently call this differently than we should.","shortMessageHtmlLink":"Point out that we apparently call this differently than we should."}},{"before":"0f4107b5f287fcf6f51410389dc57306c99bf17c","after":"3f6a36cfaede4502daa7da51bd08d2c1e2909071","ref":"refs/heads/main","pushedAt":"2024-03-03T22:22:06.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"May as well align with _meta.protocol even if we don't use it yet.\n\nIt looks like it's new in v0.10.","shortMessageHtmlLink":"May as well align with _meta.protocol even if we don't use it yet."}},{"before":"e73eb7bdac4b40c1134957e8faadf57e60189d6c","after":"0f4107b5f287fcf6f51410389dc57306c99bf17c","ref":"refs/heads/main","pushedAt":"2024-03-03T17:30:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"More closely match the structure of rpcApi from @leanprover/infoview-api","shortMessageHtmlLink":"More closely match the structure of rpcApi from @leanprover/infoview-api"}},{"before":"fbc0dc43643497587dac79f666565111ec71f7f8","after":"e73eb7bdac4b40c1134957e8faadf57e60189d6c","ref":"refs/heads/main","pushedAt":"2024-03-02T22:56:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Add the RPC methods for retrieving some user widget information.\n\nThese aren't rendered or useful anywhere yet clearly.","shortMessageHtmlLink":"Add the RPC methods for retrieving some user widget information."}},{"before":"156e7819cc860512562455642d6991c083f5d2de","after":null,"ref":"refs/heads/lean3-split","pushedAt":"2024-03-02T21:18:48.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"}},{"before":"dd37e1d2e320fb8a0948bf6ca3f7703c98b80ecb","after":"fbc0dc43643497587dac79f666565111ec71f7f8","ref":"refs/heads/main","pushedAt":"2024-02-25T17:04:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Add two apparently existing Mathlib commands to syntax highlighting.","shortMessageHtmlLink":"Add two apparently existing Mathlib commands to syntax highlighting."}},{"before":"1a2a2dfbc7e6775e9ec8b84e5eadaf31fde1894e","after":"dd37e1d2e320fb8a0948bf6ca3f7703c98b80ecb","ref":"refs/heads/main","pushedAt":"2024-02-24T14:00:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Make editDelay=0 the default when starting Lean.\n\neditDelay controls a server-side \"artificial\" delay before it responds\nto changes. Lowering it means removing that delay (which means the\nserver will do more work, albeit be more responsive).\n\nWe wouldn't normally change Lean default behavior, but many users have\nseen cases of 100% CPU usage from neovim, while Lean does nearly\nnothing in the background. #289 has some details. Our best guess has\nbeen somehow the LSP client and server getting somehow out of sync and\nbusy looping, but I have never been able to isolate exactly what's\nhappening. What we *have* seen though is that turning this off on the\nserver side seems to make the problem go away, so let's make it the\ndefault.\n\nIf we ever do find the bug, wherever it lies, we can revisit.\n\nAnyone who wants to override this of course still can do so by\nexplicitly setting a value in your configuration.\n\nCloses: #289","shortMessageHtmlLink":"Make editDelay=0 the default when starting Lean."}},{"before":"4dff4c9d40678d895c8fe8a19b7ad98a196d0921","after":"1a2a2dfbc7e6775e9ec8b84e5eadaf31fde1894e","ref":"refs/heads/main","pushedAt":"2024-02-04T01:31:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Change our Loogle User-Agent (temporarily?)\n\nThe . blows up Loogle, triggering a server restart.\n\n+ seems to not do so.","shortMessageHtmlLink":"Change our Loogle User-Agent (temporarily?)"}},{"before":"2e03e6ada85b256df4243cc727c9238b459a1a00","after":"4dff4c9d40678d895c8fe8a19b7ad98a196d0921","ref":"refs/heads/main","pushedAt":"2024-01-20T16:12:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Julian","name":"Julian Berman","path":"/Julian","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/329822?s=80&v=4"},"commit":{"message":"Simplify window closing callbacks as well.","shortMessageHtmlLink":"Simplify window closing callbacks as well."}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEWbrGzQA","startCursor":null,"endCursor":null}},"title":"Activity · Julian/lean.nvim"}