Zulip Chat Archive

Stream: general

Topic: unused argument


view this post on Zulip Kenny Lau (Jun 27 2020 at 17:53):

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

view this post on Zulip Kenny Lau (Jun 27 2020 at 17:53):

lint tells me that I have an unused argument

view this post on Zulip Kenny Lau (Jun 27 2020 at 17:53):

but I think I used it

view this post on Zulip Kenny Lau (Jun 27 2020 at 17:53):

@Johan Commelin could you check this? thanks

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:09):

@Kenny Lau What happens if you remove the argument?

view this post on Zulip Kenny Lau (Jun 27 2020 at 18:10):

it's used in the char_p.cast_eq_zero line

view this post on Zulip Kenny Lau (Jun 27 2020 at 18:10):

invalid rewrite tactic, failed to synthesize type class instance

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:11):

That's a different lemma

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:11):

It's complaining about of_irreducible_expand

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:11):

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

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:11):

You seem to be looking at of_separable_expand

view this post on Zulip Kenny Lau (Jun 27 2020 at 18:11):

oh I'm blind

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:12):

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:19):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:20):

I guess it just saves 5 keystrokes...

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:20):

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

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:20):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 27 2020 at 18:25):

Aaah, I forgot about the hole command

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Jun 27 2020 at 19:00):

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

view this post on Zulip 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.

view this post on Zulip 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