chore: bump to nightly-2023-08-19 #48
Conversation
|
@insightmind would you be able to help me understand the |
|
Hey! I think you can remove the argument there, I can't exactly remember what it was for, but it no longer seems to be used anywhere within the function. Additionally, judging from the commit/blame of this line: 42a98bb I'm pretty sure its safe to remove the argument. |
* Turn on warningAsError in CI * Remove unused arguments flagged by the linter * Note that the unused `l : List Token` argument for `genTokens` was suspicious, as nontrivial values were passed to it. Please see leanprover#48 (comment) for confirmation that removing it is correct.
semorrison
force-pushed
the
bump-nightly-2023-08-19
branch
from
d5449e0
to
39aa884
Compare
|
@insightmind, all the tests were failing, and I'm not certain to what extent it is a problem. Would you be able to have a look at the diff in the last commit (in which I just copied I'll mark this as a draft so there's no chance we merge with this commit in place, in case it is wrong! |
| "semanticType": null, | ||
| "raw": " + 1 => ", | ||
| "raw": "example : Nat → Nat\n | 0 => 0\n | n + 1 => ", |
There was a problem hiding this comment.
It looks like lots of typeinfo is missing, but I haven't followed recent changes to repo. So it might be that something regressed or this is happening because of changes in the compiler. Hard to tell. You might have a look at recent PRs to see when they started failing.
There was a problem hiding this comment.
I deleted the wrong arguments when cleaning up the unused arguments, oops!
This is done properly now on #53
Unfortunately there's still a problem bumping the tool-chain. I'm going to close this PR and do it in smaller steps.
semorrison
force-pushed
the
bump-nightly-2023-08-19
branch
from
616aca4
to
39aa884
Compare
nightly-2023-08-19 is now the first official release candidate, and I would like to see if we can get most major projects to try bumping to it.
In this PR, I've had to address the unused arguments linter in various places. Please feel free to adopt other solutions!
One warning from the linter does seem worrying:
genTokensdiscards itslargument.