## Stream: general

### Topic: unused argument

#### Kenny Lau (Jun 27 2020 at 17:53):

https://github.com/leanprover-community/mathlib/pull/3198/checks?check_run_id=814314665

#### Kenny Lau (Jun 27 2020 at 17:53):

lint tells me that I have an unused argument

#### Kenny Lau (Jun 27 2020 at 17:53):

but I think I used it

#### Kenny Lau (Jun 27 2020 at 17:53):

@Johan Commelin could you check this? thanks

#### Johan Commelin (Jun 27 2020 at 18:09):

@Kenny Lau What happens if you remove the argument?

#### Kenny Lau (Jun 27 2020 at 18:10):

it's used in the char_p.cast_eq_zero line

#### Kenny Lau (Jun 27 2020 at 18:10):

invalid rewrite tactic, failed to synthesize type class instance

#### Johan Commelin (Jun 27 2020 at 18:11):

That's a different lemma

#### Johan Commelin (Jun 27 2020 at 18:11):

It's complaining about of_irreducible_expand

#### Johan Commelin (Jun 27 2020 at 18:11):

And there I don't see how it's used

#### Johan Commelin (Jun 27 2020 at 18:11):

You seem to be looking at of_separable_expand

oh I'm blind

#### Johan Commelin (Jun 27 2020 at 18:12):

Tip: copy the linter output to the bottom of the file, and ctrl-click on the names

#### Johan Commelin (Jun 27 2020 at 18:12):

@Floris van Doorn Could #lint be "Try this"-ified?

#### Floris van Doorn (Jun 27 2020 at 18:18):

For certain linters it might be possible to get a "Try this" in theory. I think quite some work is needed though, to determine what parts to replace, and how to guess how the source looks from the elaborated expression. In this particular case, it would have to insert an omit HF just before the declaration...

#### Johan Commelin (Jun 27 2020 at 18:19):

No... I didn't mean anything fancy.

#### Johan Commelin (Jun 27 2020 at 18:19):

Just that you can hit Alt-V and have the output of #lint be copied to the main window.

#### Johan Commelin (Jun 27 2020 at 18:20):

I guess it just saves 5 keystrokes...

#### Johan Commelin (Jun 27 2020 at 18:20):

But it will save them a lot of times for a lot of people.

#### Johan Commelin (Jun 27 2020 at 18:20):

Of course you should only do this if it's easy.

#### Floris van Doorn (Jun 27 2020 at 18:24):

I think that should be possible. I don't know if the try this logic to decide what to replace is already compatible with things other than tactics.
Note: there is also a hole command linter option

#### Johan Commelin (Jun 27 2020 at 18:25):

Aaah, I forgot about the hole command

#### Floris van Doorn (Jun 27 2020 at 18:26):

Unfortunately you cannot use hole commands at the top level (would that be possible/desirable to change @Gabriel Ebner?), so you currently have to write #eval _ or something.

#### Bryan Gin-ge Chen (Jun 27 2020 at 18:48):

I opened an issue about better integrating #lint with vscode-lean a while back: leanprover/vscode-lean#149

There aren't any real concrete ideas there yet though.

#### Gabriel Ebner (Jun 27 2020 at 18:57):

In Lean 3.17 we could make the linting output a widget and make the declaration names clickable.

#### Bryan Gin-ge Chen (Jun 27 2020 at 18:58):

Presumably then we could also have the extension add diagnostics at the locations of the linter errors?

#### Gabriel Ebner (Jun 27 2020 at 19:00):

Oh yes, I'm also missing the summer festivals. :sweet_potato: :octopus:

#### Johan Commelin (Jun 27 2020 at 19:11):

I'm really looking forward to the extract_goal widget, paired with the recently discussed name-auto-generator.

#### Gabriel Ebner (Jun 27 2020 at 19:16):

BTW, at least for the current file it is possible to generate diagnostics from Lean, without modifying the vscode extension at all:

def a := 5 --<- blue squiggles here
def b := 4

open tactic widget
#eval do
e ← get_env,
some p ← pure $e.decl_pos a, let w : tc unit string := tc.stateless$ λ _, pure [
h "details" [attr.val "open" "true"] [
h "summary" [] ["unused argument"],
"blah"]],
trace_widget_at p w.to_component "unused argument: blah"


Last updated: May 12 2021 at 23:13 UTC