search

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

chore: bump to nightly-2023-08-19 #48

Closed semorrison closed 1 year ago

semorrison commented 1 year ago

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: genTokens discards its l argument.

semorrison commented 1 year ago

@insightmind would you be able to help me understand the (l : List Token) argument for genTokens in LeanInk/Annotation/Alectryon.lean? It is an unused argument, yet nontrivial values are passed to it, and I'm uncertain if it is a bug.

insightmind commented 1 year ago

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: https://github.com/leanprover/LeanInk/commit/42a98bbfd037e93d13ac9b9770d0d022803b0b4e it seems this was an argument that was used in a previous iteration of this function, which we likely forgot to remove when we simplified it. It also seems that it was previously used as a running list of Tokens due the recursive nature of the function back then, hence it's usually initialized with an empty list.

I'm pretty sure its safe to remove the argument.

semorrison commented 1 year ago

@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 *.leanInk over *.leanInk.expected, thereby "fixing" the tests)?

I'll mark this as a draft so there's no chance we merge with this commit in place, in case it is wrong!