Zulip Chat Archive

Stream: general

Topic: simp hole command

Johan Commelin (May 02 2020 at 14:25):

I saw that squeeze_simp now has a hole command that allows you to replace it with its output. Could we also add a hole command to regular simp that will say "replace me by squeeze_simp, and after that by the output of squeeze_simp"?

Gabriel Ebner (May 02 2020 at 14:47):

Do you mean "code action" by "hole command"? (Hole commands are {!!}.)

Johan Commelin (May 02 2020 at 14:59):

I guess I mean "code action". The thing that gives you a :bulb: in VScode

Johan Commelin (May 02 2020 at 14:59):

I guess hole commands are a special case?

Johan Commelin (May 02 2020 at 14:59):

Or one is implemented via the other?

Gabriel Ebner (May 02 2020 at 15:04):

There is a code action for hole commands ({!!}).

Gabriel Ebner (May 02 2020 at 15:05):

You could add a code action that checks if the word simp is under the cursor and then prompts to prepend squeeze_.

Johan Commelin (May 02 2020 at 15:06):

But could it do both in one go?

Gabriel Ebner (May 02 2020 at 15:21):

If you're good with javascript, sure.

Steffan (May 02 2020 at 19:53):

thats me

Steffan (May 02 2020 at 19:54):

why do you need JS for that tho?
more like, you don't put JS in Lean, right? x)

Patrick Massot (May 02 2020 at 19:54):

The VS code extension is written in TypeScript

Steffan (May 02 2020 at 19:54):

Patrick Massot (May 02 2020 at 19:54):

https://github.com/leanprover/vscode-lean

Steffan (May 02 2020 at 19:54):

Well I don't do that stuff.

Patrick Massot (May 02 2020 at 19:54):

like all VS code extensions I guess

Steffan (May 02 2020 at 19:55):

yes, I don't know how to do a vscode extension tho.

Bryan Gin-ge Chen (May 02 2020 at 20:47):

@Johan Commelin What you describe sounds possible, though I don't see a non-hacky way to do it. The issue is that I don't know how to get the squeeze_simp output from Lean without modifying the file. It'd be much nicer if we had an interface to have the Lean server evaluate some code without adding it to the file. I guess that's what the hole commands are for, but it's annoying to have to add {!!} whenever we want to use them (and apparently we also can't use them in tactics).

Anyways I won't have time to tackle it in the near future, but if you open an issue at the vscode-lean repo I'll try and circle back to this when I can. I do think we could try and add more code actions (particularly relating to linting).

Johan Commelin (May 02 2020 at 21:00):

@Bryan Gin-ge Chen voila: https://github.com/leanprover/vscode-lean/issues/157

Last updated: Dec 20 2023 at 11:08 UTC