Bryan Gin-ge Chen
Bryan Gin-ge Chen
This was commented out in https://github.com/leanprover-community/quote4/pull/108/files#diff-d145b90fb729a769adec1dfe0043f229fac2a54f6573370f7b5fa58ecc5ab4ae. Not sure if it's related but I noticed another one of the tests in the file leads to a panic if turned into an...
Weird, looks like one of the runners went offline before the build finished: https://github.com/leanprover-community/mathlib4/actions/runs/10460865400 Let's try again. bors r+
One of the runners ran out of space. Re-running bors r+
While this is unlikely to be fixed before we change to Lean 4, it may be worth leaving this open to serve as a reference for others who run into...
This is great! A few things: - The "sticky" tag selection banner is a bit large and it might be a bit annoying on mobile or narrow screens. Could you...
Thanks, looks like you've addressed all my concerns! Am I correct that there's intentionally no way to view items tagged `historical` now? I'd prefer if they were still accessible somehow,...
> Do we even need an `easy` label? Is it something people specifically filter PRs by? I've often used it when looking for low-hanging fruit to approve.
Some settings (like wordSeparators) could potentially go in the vscode-lean repo instead so that people have access to them by default when working on Lean projects outside mathlib. There's also...
Oh, that's actually a good question. I guess we could write a command in the VS Code extension that copies some convenient settings to the users `settings.json` or a per-project...