Zulip Chat Archive

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