Zulip Chat Archive

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

Kenny Lau (Jun 27 2020 at 18:11):

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"

Martin Dvořák (Aug 25 2022 at 21:17):

Johan Commelin said:

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

Has it been done in the meanwhile?


Last updated: Dec 20 2023 at 11:08 UTC